機械学習の論理推論を援用したスケーラブルな形式検証並列化手法の研究

• Project/Area Number: 25K15065
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60050:Software-related
• Research Institution: Waseda University
• Principal Investigator: 岸 知二 早稲田大学, 理工学術院, 教授 (30422661)
• Project Period (FY): 2025-04-01 – 2028-03-31
• Project Status: Granted (Fiscal Year 2025)
• Budget Amount: ¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000); Fiscal Year 2027: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2026: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2025: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
• Keywords: ソフトウェア / ソフトウェア工学 / 形式検証 / 機械学習 / 可変性管理

Outline of Research at the Start

形式検証は論理に基づきシステムの正しさを厳密に確認する技術として，特に信頼性や安全性の求められる分野で使われているが，スケーラビリティに課題がある．一方，近年発達した機械学習による論理推論はスケーラブルだが統計的な手法であるため厳密解を得ることは困難である．本研究では機械学習による論理推論を，形式手法の厳密解に影響しないように援用することで，形式手法のスケーラビリティ改善を狙う．具体的には，形式検証を並列化する際に，機械学習により高速に得られる解の予測を活用し，システム記述の効果的な分割，効率的な並行検証の実行戦略の決定，最も適切な分割数の決定などを行う手法を提案しツールとして具現化する．