論文の概要: Automating Formal Verification with Reinforcement Learning and Recursive Inference

• arxiv url: http://arxiv.org/abs/2605.30914v1
• Date: Fri, 29 May 2026 06:59:28 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-01 20:56:50.435512
• Title: Automating Formal Verification with Reinforcement Learning and Recursive Inference
• Title（参考訳）: 強化学習と再帰推論による形式検証の自動化
• Abstract要約: 我々はダフニーで検証可能な報酬(RLVR)と検証者誘導推論時間探索を用いてオープンソースモデルを訓練する。 固定ベースモデルでは、証明修正器を備えた完全な足場は、直接修理中の初期VeriCodingパイロットセットのパスレートを46.2%から69.2%に改善する。 Rust $texttcurve25519-dalek$検証プロジェクトから派生した,レポジトリスケールのLeanベンチマークであるDalek-Benchについても紹介します。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automated formal verification remains challenging for large language models because data for proof assistants and verification-aware languages is scarce, and correctness depends on satisfying precise machine-checkable specifications rather than producing plausible code. This thesis studies how verifier environments can improve LLM generation of verified programs and proofs through reinforcement learning from verifiable rewards (RLVR) and verifier-guided inference-time search. First, we train open-source models in Dafny with RLVR using Group Relative Policy Optimization (GRPO) and related variants, assembling generated candidates into complete programs and scoring them with compiler and verifier outcomes. Initial experiments on an APPS-derived Dafny dataset increased verified reward from 2.2% to 58.1%, but revealed specification hacking, where models exploit weak formal specifications instead of implementing the intended solutions. After filtering underspecified and vulnerable tasks, multi-turn RLVR on the refined benchmark improves the verified pass rate from 9.7% to 31.1%. Second, we develop a verifier-guided inference scaffold in Lean that treats proof generation as structured search over decomposed subgoals, verifier feedback, diagnostics, and repair. With a fixed base model, the full scaffold with proof reviser improves pass rate on an initial VeriCoding pilot set from 46.2% under direct repair to 69.2%. On the larger VERINA dataset, whole-task decomposition plus proof reviser solves 7 of 42 previously unsolved tasks. We also introduce Dalek-Bench, a repository-scale Lean benchmark derived from the Rust $\texttt{curve25519-dalek}$ verification project; preliminary results remain weak, indicating that stronger progress evaluation and task-specific tool-use policies are still needed.
• Abstract（参考訳）: 証明アシスタントや検証対応言語のデータが少ないため、大規模な言語モデルでは、自動的な形式検証は依然として困難であり、正確性は、プラウシブルコードを生成するのではなく、正確なマシンチェック可能な仕様を満たすことに依存する。 本論文は,検証済み報酬(RLVR)と検証対象推論時間探索からの強化学習を通じて,検証対象環境が検証対象プログラムと証明のLLM生成を改善する方法について検討する。 まず、グループ相対ポリシー最適化(GRPO)と関連する変種を用いて、DafnyのオープンソースモデルをRLVRでトレーニングし、生成した候補を完全なプログラムに組み立て、コンパイラと検証結果で評価する。 APPSから派生したDafnyデータセットの初期実験では、証明された報酬が2.2%から58.1%に増加したが、仕様のハッキングが明らかになった。 未特定で脆弱なタスクをフィルタリングした後、改良されたベンチマークでのマルチターンRLVRは、検証されたパスレートを9.7%から31.1%に改善する。 第2に,分解されたサブゴール,検証者フィードバック,診断,修復よりも,証明生成を構造化された検索として扱う検証者誘導推論足場をLeanで開発する。 固定ベースモデルでは、証明修正器を備えた完全な足場は、直接修理中の初期VeriCodingパイロットセットのパスレートを46.2%から69.2%に改善する。 より大きなVERINAデータセットでは、全タスク分解プラス証明修正器が、未解決タスク42の7を解決している。 Rust $\texttt{curve25519-dalek}$検証プロジェクトに由来する,リポジトリスケールのLeanベンチマークであるDalek-Benchについても紹介した。

関連論文リスト

• SEVA: Self-Evolving Verification Agent with Process Reward for Fact Attribution [6.908637308550535]
  SEVAは、エビデンスアライメント、ステップバイステップの推論チェーン、キャリブレーションされた信頼度、6カテゴリのエラー診断を発行する構造化検証エージェントである。 ClearFacts では、SEVA-3B は GPT-4o-mini (69.0 vs. 69.8 F1) と一致し、よりリッチで監査可能な出力を生成する。
  論文  参考訳（メタデータ） (2026-06-29T02:37:13Z)
• Verifier-First Evaluation of Agentic LLMs for Infrastructure-as-Code Generation [0.0]
  自然言語からインフラストラクチャ・アズ・コード(IaC)を生成するには、プロバイダのスキーマ、依存関係の計画、組織的なポリシの制約を満たす必要がある。 Rego v1ポリシを備えた186タスクのAWS/TerraformベンチマークであるIaC-Eval v2で評価されたTerraform生成のための7つのエージェント戦略に関する検証初の実験的研究を示す。
  論文  参考訳（メタデータ） (2026-05-29T12:43:27Z)
• Agentic Proving for Program Verification [44.663012714194025]
  エージェントシステムは、形式数学における自動定理証明のための最先端のアプローチとして登場した。 検証可能なコード生成のためのLean 4ベンチマークであるCLEVERのエージェント証明フレームワークでClaude Codeを評価した。
  論文  参考訳（メタデータ） (2026-05-22T15:41:27Z)
• Rewarding the Scientific Process: Process-Level Reward Modeling for Agentic Data Analysis [68.28714988482703]
  プロセス・リワード・モデル(PRM)は、LLM(Large Language Models)の推論能力を増強することに成功した。 本稿では,一般ドメインのPRMがデータ分析エージェントの監督に苦慮していることを示す。 本稿では,新しい環境対応生成プロセス報酬モデルであるDataPRMを紹介する。
  論文  参考訳（メタデータ） (2026-04-27T09:00:30Z)
• From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification [0.30915521808748864]
  大規模な言語モデルは、自動化されたソフトウェア工学における約束を示すが、その正しさの保証は、誤ったコードや幻覚的なコードによってしばしば損なわれる。 NaturalLanguage2VerifiedCodeデータセット:60の複雑なアルゴリズム問題の集合を提供する。 7個のオープンウェイト LLM でランダムに選択された11個の問題集合をタイレッドプロンプト戦略を用いて評価した。 以上の結果から,コンテキストレスなプロンプトがほぼユニバーサルの失敗につながる一方で,構造的アンカーと反復的自己修復が劇的なパフォーマンスの転換を促進することが示唆された。
  論文  参考訳（メタデータ） (2026-04-24T14:28:10Z)
• Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification [34.98335927187393]
  大規模言語モデル(LLM)は可塑性コードを生成することができるが、正確性には限界がある。 本稿では,Lean4における自動コード検証のための階層的証明検索フレームワークを提案する。 Goedel-Code-Prover-8Bは、分解と完了の両方のための単一の統一ポリシーです。
  論文  参考訳（メタデータ） (2026-03-18T18:42:04Z)
• HLE-Verified: A Systematic Verification and Structured Revision of Humanity's Last Exam [63.84155758655084]
  HumanityのLast Exam (HLE)は、フロンティアの大規模言語モデルを評価するために広く使われているベンチマークである。 HLE-Verifiedは,透過的検証プロトコルときめ細かい誤り分類法を備えたHLEの検証および改訂版である。 我々は,HLEとHLE-Verifiedの7つの最先端言語モデルを評価し,平均7～10ポイントの絶対精度を観測した。
  論文  参考訳（メタデータ） (2026-02-15T02:50:15Z)
• PRIME: A Process-Outcome Alignment Benchmark for Verifiable Reasoning in Mathematics and Engineering [71.15346406323827]
  本稿では,プロセス・アウトカム・アライメント・アライメント・検証における検証結果を評価するベンチマークであるPRIMEを紹介する。 現在の検証器は、しばしば導出欠陥を検出するのに失敗する。 本稿では,PRIMEで選択した検証手法を利用したプロセス認識型RLVRトレーニングパラダイムを提案する。
  論文  参考訳（メタデータ） (2026-02-12T04:45:01Z)
• CVeDRL: An Efficient Code Verifier via Difficulty-aware Reinforcement Learning [57.24524263804788]
  コード検証は、LLMベースのコード生成の検証後において重要な役割を果たす。 既存の教師付き微調整手法は、データの不足、高い失敗率、推論効率の低下に悩まされている。 機能的な報酬しか持たない単純RLは、難しいブランチやサンプルに対して効果的な単体テストを生成することができないことを示す。
  論文  参考訳（メタデータ） (2026-01-30T10:33:29Z)
• Continuous Self-Improvement of Large Language Models by Test-time Training with Verifier-Driven Sample Selection [6.471199527741301]
  VDS-TTT(Verifier-Driven Sample Selection for Test-Time Training)と呼ばれる新しいフレームワークを導入する。 学習した検証器を用いて、生成された応答のプールをスコアし、高いランクの擬似ラベル付き例からのみ選び、微調整を施す。 低ランクなLoRAアダプタパラメータのみを微調整し、適応効率と高速収束を確保する。
  論文  参考訳（メタデータ） (2025-05-26T03:54:47Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。 SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。 我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• TACRED Revisited: A Thorough Evaluation of the TACRED Relation Extraction Task [80.38130122127882]
  TACREDはリレーショナル抽出(RE)において最も大きく、最も広く使われているクラウドソースデータセットの1つである パフォーマンスの天井に到達したのか、改善の余地はあるのか? ラベルエラーは絶対F1テストエラーの8%を占めており、例の50%以上を可逆化する必要がある。
  論文  参考訳（メタデータ） (2020-04-30T15:07:37Z)

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

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