2024 Fiscal Year Research-status Report
Formal verification methods for trustworthy statistics
| Project/Area Number |
24K02924
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
川本 裕輔 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究グループ長 (60760006)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
佐藤 哲也 東京科学大学, 情報理工学院, 助教 (40761797)
田中 哲 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (10357452)
|
|---|
| Project Period (FY) |
2024-04-01 – 2027-03-31
|
| Keywords | 形式手法 / プログラム検証 / 自動検証 / 統計の信頼性 / 仮説検定 |
|---|
| Outline of Annual Research Achievements |
本研究は、ソフトウェアの動作を数理論理学に基づいて厳密に記述し検証するための「形式手法」を用いて、統計の誤りを防ぐための仕様記述言語と自動検証技術を開発することを目的としている。
本年度は、統計の誤りを防ぐための仕様記述言語・自動検証技術及びこれらの基礎となる理論について、以下の研究に取り組んだ。
(1) 統計の誤りを防ぐための形式検証ツールStatWhyの開発を実施した。具体的には、仕様記述言語に関して、統計プログラムにおける繰り返しの記述を簡潔にするための略記法を導入し実装した。自動検証技術に関しては、統計プログラムの検証に失敗した場合に統計の前提や解釈の誤りの箇所を分かりやすく指摘できるように、形式検証ツールStatWhyの利便性を高めた。また、形式検証ツールStatWhyによる自動検証を高速化するために、統計プログラムの特徴に基づいて証明のゴールを簡略化するためのタクティクスを導入した。さらに、形式検証ツールStatWhyにおいてさまざまな仮説検定手法のモジュールを整備した。これらの研究成果をまとめた論文が査読付国際会議CAV2025に採択された。また、形式検証ツールStatWhyとそのユーザドキュメントを公開した。
(2) 統計の誤りを防ぐための形式検証技術の基礎となる理論の研究に取り組んだ。具体的には、形式検証ツールStatWhyの基礎となる論理体系BHLの枠組みとデフォルト推論との間の比較と分析を行った。研究成果について日本科学哲学会において発表した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
統計の誤りを防ぐための形式検証ツールStatWhyの開発を進め、本ツールを公開することができた。また、研究成果をまとめた論文が査読付国際会議CAV 2025に採択されており、おおむね順調に進展していると言える。
|
| Strategy for Future Research Activity |
2024年度に引き続き、形式検証ツールStatWhyの機能の拡張を目指す。このために、統計プログラムの正しさを検証できる論理体系について研究を行い、その性質を明らかにする。また、現状では、検証対象がOCamlで書かれたプログラムにとどまっているが、他の言語で書かれたプログラムの検証の実現を目指す。
|
| Causes of Carryover |
本研究の遂行に必要な情報収集のための海外出張を本年度に実施できず、次年度に実施することにしたため、次年度使用額が生じた。
|
