Formal verification methods for trustworthy statistics

• 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: ¥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

観察研究・実験研究における統計の誤りは，科学的結論や政策判断の誤りにつながるため，社会的に注目を集めている．しかし，統計の誤りを防ぎ，統計の信頼性を保証する手段は確立されていない．そこで，本研究では，ソフトウェアの動作を数理論理学に基づいて厳密に記述し検証するための「形式手法」を用いて，統計の誤りを防ぐための仕様記述言語と自動検証技術を開発し，その有効性を評価する．