| Project/Area Number |
24K02924
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| 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
|
| Project Status |
Granted (Fiscal Year 2024)
|
| Budget Amount *help |
¥18,590,000 (Direct Cost: ¥14,300,000、Indirect Cost: ¥4,290,000)
Fiscal Year 2026: ¥6,370,000 (Direct Cost: ¥4,900,000、Indirect Cost: ¥1,470,000)
Fiscal Year 2025: ¥5,720,000 (Direct Cost: ¥4,400,000、Indirect Cost: ¥1,320,000)
Fiscal Year 2024: ¥6,500,000 (Direct Cost: ¥5,000,000、Indirect Cost: ¥1,500,000)
|
|---|
| Keywords | 形式手法 / プログラム検証 / 自動検証 / 統計の信頼性 / 仮説検定 / 統計 |
|---|
| Outline of Research at the Start |
観察研究・実験研究における統計の誤りは，科学的結論や政策判断の誤りにつながるため，社会的に注目を集めている．しかし，統計の誤りを防ぎ，統計の信頼性を保証する手段は確立されていない．そこで，本研究では，ソフトウェアの動作を数理論理学に基づいて厳密に記述し検証するための「形式手法」を用いて，統計の誤りを防ぐための仕様記述言語と自動検証技術を開発し，その有効性を評価する．
|
| 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で書かれたプログラムにとどまっているが、他の言語で書かれたプログラムの検証の実現を目指す。
|
