| 研究課題/領域番号 |
24K02924
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 国立研究開発法人産業技術総合研究所 |
|---|
研究代表者 |
川本 裕輔 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 研究グループ長 (60760006)
|
|---|
| 研究分担者 |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
佐藤 哲也 東京科学大学, 情報理工学院, 助教 (40761797)
田中 哲 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (10357452)
|
|---|
| 研究期間 (年度) |
2024-04-01 – 2027-03-31
|
| 研究課題ステータス |
交付 (2024年度)
|
| 配分額 *注記 |
18,590千円 (直接経費: 14,300千円、間接経費: 4,290千円)
2026年度: 6,370千円 (直接経費: 4,900千円、間接経費: 1,470千円)
2025年度: 5,720千円 (直接経費: 4,400千円、間接経費: 1,320千円)
2024年度: 6,500千円 (直接経費: 5,000千円、間接経費: 1,500千円)
|
|---|
| キーワード | 形式手法 / プログラム検証 / 自動検証 / 統計の信頼性 / 仮説検定 / 統計 |
|---|
| 研究開始時の研究の概要 |
観察研究・実験研究における統計の誤りは，科学的結論や政策判断の誤りにつながるため，社会的に注目を集めている．しかし，統計の誤りを防ぎ，統計の信頼性を保証する手段は確立されていない．そこで，本研究では，ソフトウェアの動作を数理論理学に基づいて厳密に記述し検証するための「形式手法」を用いて，統計の誤りを防ぐための仕様記述言語と自動検証技術を開発し，その有効性を評価する．
|
| 研究実績の概要 |
本研究は、ソフトウェアの動作を数理論理学に基づいて厳密に記述し検証するための「形式手法」を用いて、統計の誤りを防ぐための仕様記述言語と自動検証技術を開発することを目的としている。
本年度は、統計の誤りを防ぐための仕様記述言語・自動検証技術及びこれらの基礎となる理論について、以下の研究に取り組んだ。
(1) 統計の誤りを防ぐための形式検証ツールStatWhyの開発を実施した。具体的には、仕様記述言語に関して、統計プログラムにおける繰り返しの記述を簡潔にするための略記法を導入し実装した。自動検証技術に関しては、統計プログラムの検証に失敗した場合に統計の前提や解釈の誤りの箇所を分かりやすく指摘できるように、形式検証ツールStatWhyの利便性を高めた。また、形式検証ツールStatWhyによる自動検証を高速化するために、統計プログラムの特徴に基づいて証明のゴールを簡略化するためのタクティクスを導入した。さらに、形式検証ツールStatWhyにおいてさまざまな仮説検定手法のモジュールを整備した。これらの研究成果をまとめた論文が査読付国際会議CAV2025に採択された。また、形式検証ツールStatWhyとそのユーザドキュメントを公開した。
(2) 統計の誤りを防ぐための形式検証技術の基礎となる理論の研究に取り組んだ。具体的には、形式検証ツールStatWhyの基礎となる論理体系BHLの枠組みとデフォルト推論との間の比較と分析を行った。研究成果について日本科学哲学会において発表した。
|
| 現在までの達成度 |
現在までの達成度
2: おおむね順調に進展している
理由
統計の誤りを防ぐための形式検証ツールStatWhyの開発を進め、本ツールを公開することができた。また、研究成果をまとめた論文が査読付国際会議CAV 2025に採択されており、おおむね順調に進展していると言える。
|
| 今後の研究の推進方策 |
2024年度に引き続き、形式検証ツールStatWhyの機能の拡張を目指す。このために、統計プログラムの正しさを検証できる論理体系について研究を行い、その性質を明らかにする。また、現状では、検証対象がOCamlで書かれたプログラムにとどまっているが、他の言語で書かれたプログラムの検証の実現を目指す。
|
