AIを含むソフトウェアのための形式検証手法

2025 年度 審査結果の所見

• 研究課題/領域番号: 25H01113
• 研究種目: 基盤研究(A)
• 配分区分: 補助金
• 応募区分: 一般
• 審査区分: 中区分60:情報科学、情報工学およびその関連分野
• 研究機関: 京都大学
• 研究代表者: 末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
• 研究分担者: 和賀 正樹 京都大学, 情報学研究科, 助教 (00899007) ; 五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456) ; 池渕 未来 京都大学, 情報学研究科, 助教 (70961796) ; 関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (80828476) ; Hsieh Chiao (謝橋) 北陸先端科学技術大学院大学, 先端科学技術研究科, 特任助教 (71006426)
• 研究期間 (年度): 2025-04-01 – 2030-03-31

学術的意義、期待される成果

機械学習技術に基づき構築されたソフトウェアがブラックボックス化している昨今の課題解決に向けて、AIの形式的仕様を学習する手法や、仕様の正確性を前提としない検証手法といった独創的なアイデアを基に具体的な計画が提案されており、大きな波及効果が期待される。AIの信頼性担保のための理論的側面からのアプローチは将来のソフトウェア品質の向上だけでなく、学術的な新規性、重要性も高い。