ExVerus：反例推論によるVerus証明の修復

arXiv cs.LG / 2026/3/30

📰 ニュースIdeas & Deep AnalysisModels & Research

共有:

要点

EXVERUSは、失敗したVerusの証明に対して反例（counterexample）を自動生成・検証し、その行動的フィードバックをLLMの推論に取り込む反例ガイド型フレームワークを提案している。
従来のようにソースコード全体から静的に推論するのではなく、反例を一般化して帰納的不変条件（inductive invariants）を作り、同種の失敗を再発させないことを狙っている。
評価では、既存のプロンプトベースのVerus証明生成手法と比べて、証明の正確性・頑健性が向上し、さらにトークン効率も改善したと報告している。
この研究は、形式検証におけるLLM利用において、検証器のフィードバックを単なるエラー情報としてでなく“具体的なプログラム挙動（反例）”として活用する方向性を示している。

要旨: 大規模言語モデル（LLM）は、形式的検証の自動化において有望な結果を示しています。しかし、既存の手法は、証明生成をソースコードに対する静的なエンドツーエンド予測として扱い、限定的な検証器からのフィードバックに依存するとともに、具体的なプログラム挙動にアクセスできていません。私たちは、反例を通じた挙動フィードバックにより、LLMが証明について推論できるようにする反例ガイド付きフレームワークであるEXVERUSを提示します。証明が失敗した場合、EXVERUSは自動的に反例を生成して検証し、その後それらを帰納的不変量へと一般化するようLLMを導き、これらの失敗を阻止します。評価の結果、EXVERUSは、最先端のプロンプトベースのVerus証明生成器に比べて、証明精度、頑健性、トークン効率を大幅に向上させることが分かりました。