大規模形式検証を実現するライブラリ自動検索機能付き定理証明器とモデル検査器の融合

• 研究課題/領域番号: 25K14989
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 審査区分: 小区分60010:情報学基礎論関連
• 研究機関: 信州大学
• 研究代表者: 和崎 克己 信州大学, 学術研究院工学系, 教授 (70271492)
• 研究期間 (年度): 2025-04-01 – 2029-03-31
• 研究課題ステータス: 交付 (2025年度)
• 配分額: 4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円); 2028年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2027年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円); 2026年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円); 2025年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
• キーワード: 定理証明系 / モデル検査 / 大規模言語モデル / ハードウェアコンパイラ / 状態空間最適分割

研究開始時の研究の概要

本研究は、定理証明系とモデル検査器を統合し、大規模かつ高並列なハードウェア設計に対する高精度な検証を実現することを目的とする。AIによる定理検索機能を備えたコンパイラとGPUクラスタによる並列検証により、検証効率と信頼性の両立を図る。