論文の概要: ExVerus: Verus Proof Repair via Counterexample Reasoning

• arxiv url: http://arxiv.org/abs/2603.25810v2
• Date: Mon, 30 Mar 2026 05:32:19 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-31 13:48:18.833858
• Title: ExVerus: Verus Proof Repair via Counterexample Reasoning
• Title（参考訳）: ExVerus:反例推論によるVerusの修復の証明
• Authors: Jun Yang, Yuechun Sun, Yi Wu, Rodrigo Caridad, Yongwei Yuan, Jianan Yao, Shan Lu, Kexin Pei,
• Abstract要約: 大規模言語モデル(LLM)のための逆例誘導フレームワークであるEXVERUSを提案する。 証明が失敗すると、EXVERUSは反例を自動生成して検証し、LSMを誘導して誘導不変量に一般化し、これらの障害を阻止する。 評価の結果,EXVERUSは最先端のプロンプトベースのVerus証明生成器よりも証明精度,堅牢性,トークン効率を著しく向上することがわかった。
• 参考スコア（独自算出の注目度）: 8.819482630789217
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large Language Models (LLMs) have shown promising results in automating formal verification. However, existing approaches treat proof generation as a static, end-to-end prediction over source code, relying on limited verifier feedback and lacking access to concrete program behaviors. We present EXVERUS, a counterexample-guided framework that enables LLMs to reason about proofs using behavioral feedback via counterexamples. When a proof fails, EXVERUS automatically generates and validates counterexamples, and then guides the LLM to generalize them into inductive invariants to block these failures. Our evaluation shows that EXVERUS significantly improves proof accuracy, robustness, and token efficiency over the state-of-the-art prompting-based Verus proof generator.
• Abstract（参考訳）: 大規模言語モデル(LLM)は形式的検証を自動化する上で有望な結果を示している。 しかし、既存のアプローチでは、証明生成をソースコード上の静的なエンドツーエンドの予測として扱い、限定された検証者フィードバックに依存し、具体的なプログラム動作へのアクセスを欠いている。 提案するEXVERUSは, 反例による行動フィードバックを用いて, LLMが証明を推論できる, 対例誘導型フレームワークである。 証明が失敗すると、EXVERUSは反例を自動生成して検証し、LSMを誘導して誘導不変量に一般化し、これらの障害を阻止する。 評価の結果,EXVERUSは最先端のプロンプトベースのVerus証明生成器よりも証明精度,堅牢性,トークン効率を著しく向上することがわかった。

関連論文リスト

• Learning to Disprove: Formal Counterexample Generation with Large Language Models [26.262810717227108]
  数学における現在のAIの取り組みは、ほとんど証明構築にのみ焦点をあてている。 我々はこのタスクを形式的な逆例生成として定式化する。 多様なトレーニングデータを合成するシンボリックな突然変異戦略を導入する。
  論文  参考訳（メタデータ） (2026-03-19T22:42:49Z)
• Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought [1.167370706056905]
  VCoT-Liftは低レベルの解法推論を高レベルで可読性のある検証ステップに引き上げる。 VCoT-Benchは、欠落した証明の様々な程度に対する堅牢性、異なる証明タイプに対する能力、証明位置に対する感度の3つの次元で性能を測定する。
  論文  参考訳（メタデータ） (2026-03-18T22:42:20Z)
• Abductive Inference in Retrieval-Augmented Language Models: Generating and Validating Missing Premises [0.0]
  本稿では,帰納的推論をLLMに組み込むフレームワークを提案する。 帰納的推論とマルチホップQAベンチマークの実験結果から,本手法は解答精度と帰納的忠実度の両方を改善することが示された。 この研究は、RAGシステムの堅牢性と説明可能性を高めるための有望な方向として、帰納的推論を強調している。
  論文  参考訳（メタデータ） (2025-11-06T03:37:24Z)
• What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus [2.8003002159083237]
  我々は,2つの言語で作業する8人の専門家から,詳細なソースコードテレメトリの収集と解析を行うユーザスタディを実施している。 その結果、専門家が証明開発プロセスで遭遇した重要な課題や証明についてどのように考えるかについて興味深い傾向とパターンが明らかになった。 我々はこれらの知見を,AI証明アシスタントのための具体的な設計指針に翻訳する。
  論文  参考訳（メタデータ） (2025-08-01T22:16:30Z)
• StepProof: Step-by-step verification of natural language mathematical proofs [16.150265021594088]
  本稿では,ステップ・バイ・ステップ検証のための新しい自動形式化手法であるStepProofを提案する。 StepProofは、完全な証明を複数の検証可能なサブプロテクションに分解し、文レベルの検証を可能にする。 StepProofは従来の手法に比べて証明成功率と効率を著しく改善することを示す。
  論文  参考訳（メタデータ） (2025-06-12T10:31:23Z)
• Faithfulness-Aware Uncertainty Quantification for Fact-Checking the Output of Retrieval Augmented Generation [108.13261761812517]
  本稿では,RAG出力における幻覚検出の新しい手法であるFRANQ(Fithfulness-based Retrieval Augmented Uncertainty Quantification)を紹介する。 本稿では,事実性と忠実性の両方に注釈を付したQAデータセットを提案する。
  論文  参考訳（メタデータ） (2025-05-27T11:56:59Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。