Stepwise: 自動システム検証のためのニューラル-シンボリック証明探索

要約: 対話型定理証明による形式的検証は、重要なシステムの正確性を保証するためにますます広く用いられていますが、大規模な証明スクリプトの作成は依然として高度な手作業を要し、スケーラビリティを制約しています。特に数学的推論における大規模言語モデル（LLM）の進歩は、ソフトウェア検証への統合をますます有望にしています。本論文は、システムレベルの検証プロジェクトの証明探索を自動化するよう設計された神経-シンボリック証明生成フレームワークを紹介します。フレームワークは、証明状態上でベストファースト（優先度付き）ツリー探索を実行し、次の候補証明手順を繰り返しLLMに問い合わせます。ニューラル側では、証明状態と手順のペアのデータセットを用いてLLMsをファインチューニングします。シンボリック側では、却下された手順を修正するための幅広いITPツールを組み込み、証明状態をフィルタリング・ランク付けし、探索の進捗が停滞したときにはサブゴールを自動的に解消します。この相乗効果により、データ効率の高いLLM適応と意味情報に基づく探索空間の絞り込みが可能になります。新しいIsabelle REPL上にフレームワークを実装し、細粒度の証明状態と自動化ツールを公開し、FVEL seL4ベンチマークおよび追加のIsabelle開発で評価します。seL4では、システムは定理の最大77.6\%を証明し、従来のLLMベースのアプローチおよび単独のSledgehammerを大幅に凌駕し、より多くの多段証明を解決します。他のベンチマークにおける結果は、強い一般化を示しており、スケーラブルな自動ソフトウェア検証への有効な道を示唆しています。