論文の概要: Scaling Lean Theorem Proving for Real-World Code Verification
- arxiv url: http://arxiv.org/abs/2610.38174v1
- Date: Wed, 28 Oct 2026 02:23:25 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-11-01 01:32:09.939026
- Title: Scaling Lean Theorem Proving for Real-World Code Verification
- Title（参考訳）: 実世界のコード検証のためのリーン理論のスケーリング
- Abstract要約: EasyProverは、669/672 PutnamBench問題と6つのIMO 2026の形式化を証明している。
Aegisは競合するプログラミング問題を実際の実装よりもはるかに難しい検証タスクに変換する。
2,045の差分検証されたRust-Leanプログラムペアと11,533の候補仕様を生成する。
- 参考スコア（独自算出の注目度）: 2.4869619439800723
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We present EasyProver, a Lean proving system built from recursive agents with isolated contexts, asynchronous search, parallel tactic probing, and an elastic elaboration service. Using an off-the-shelf frontier model with no additional training, it proves 669/672 PutnamBench problems and all six IMO 2026 formalizations and resolves 597/600 NTP4VC verification conditions and all 189 VERINA tasks by proof or refutation. Because these benchmarks are close to saturation, we also introduce Aegis, which converts competitive programming problems into much harder verification tasks over real implementations. The pipeline writes safe Rust solutions, translates them into Lean with Aeneas, generates specifications, and labels each frozen statement with a kernel-checked proof or refutation. It produces 2,045 differentially validated Rust-Lean program pairs and 11,533 candidate specifications. Unlike hand-written benchmarks, these tasks carry implementation-level obligations from fixed-width arithmetic, explicit failure, generated loops, casts, and functionalized mutation. On a stratified sample of 2,000 statements, EasyProver proves 1,054 (52.7%) within a 30-minute budget per statement. The same tasks can also be used to benchmark other provers and as rewards for reinforcement learning.
- Abstract（参考訳）: 我々は、分離されたコンテキスト、非同期検索、並列戦術探索、エラスティックな実験サービスを備えた再帰的エージェントで構築されたリーン証明システムであるEasyProverを紹介します。
669/672 パトナムベンチ問題と6つのIMO 2026の形式化を証明し、597/600 NTP4VCの検証条件と189のVERINAタスクを証明または再利用によって解決する。
これらのベンチマークは飽和に近いため、競合するプログラミング問題を実際の実装よりもはるかに難しい検証タスクに変換するAegisも導入する。
パイプラインは安全なRustソリューションを記述し、それらをLean with Aeneasに翻訳し、仕様を生成し、各フリーズステートメントにカーネルチェックされた証明や反証をラベル付けする。
2,045の差分検証されたRust-Leanプログラムペアと11,533の候補仕様を生成する。
手書きのベンチマークとは異なり、これらのタスクは固定幅演算、明示的な失敗、生成されたループ、キャスト、機能化された突然変異による実装レベルの義務を担っている。
2,000のステートメントの階層化されたサンプルで、EasyProverは1ステートメントあたり30分の予算で1,054 (52.7%)を証明している。
同じタスクは、他のプローバーのベンチマークや強化学習の報酬にも使用できる。
関連論文リスト
- FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification [0.0]
FORALLLEAN-AGENTは、形式数学とソフトウェア検証における監査可能な推論のためのフレームワークである。
独立したワークスペース、リーンツール、ステートメント比較による新たなレビュー、公理監査、独立した証明チェックを組み合わせたものだ。
We evaluate the framework on VeriSoftBench, PutnamBench, and both problems in the Lean Eval softwareverification track。
論文 参考訳（メタデータ） (2026-10-01T01:00:35Z) - SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs? [39.004582663385364]
Benchprooferは、既知の正しいパッチでコーディングタスクを正式に認証されたパイプラインに変換するパイプラインです。
SWE-bench Verified に適用すると SWE-Proof が得られる。
論文 参考訳（メタデータ） (2026-09-18T01:16:53Z) - 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) - Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism [2.215655942741476]
本稿では,機械チェック可能な証明を通じて推論を評価するベンチマークスイートProofGridを紹介する。
ProofGridには、証明記述、証明チェック、証明マスキング、証明ギャップ埋めを含む15のタスクが含まれている。
タスクは最小の形式表記、特に短いプロンプトに適合するコンパクトな自然言語推論言語であるNDLで表現される。
論文 参考訳（メタデータ） (2026-04-07T01:19:41Z) - Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。
その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。
VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
論文 参考訳（メタデータ） (2025-05-17T04:16:36Z) - Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。
まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。
次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。
最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
論文 参考訳（メタデータ） (2025-02-11T15:27:35Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
LLMの複雑な推論には2行のアプローチが採用されている。
1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。
他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。
具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
論文 参考訳（メタデータ） (2023-11-16T11:26:21Z) - PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。
本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。
我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文 参考訳（メタデータ） (2020-10-06T15:47:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。