論文の概要: Solving VeriContest with a Lean-Backed Rust Verifier
- arxiv url: http://arxiv.org/abs/2610.03994v1
- Date: Fri, 02 Oct 2026 19:56:10 GMT
- ステータス: 情報取得中
- システム内更新日: 2026-10-06 20:41:30.252238
- Title: Solving VeriContest with a Lean-Backed Rust Verifier
- Title（参考訳）: リーンバックのRust検証によるVeriContestの解決
- Abstract要約: 我々は、Lean 4.0が支援するRustの検証ツールであるRust-Proverで、同じ証明生成タスクを解決することを報告します。
すべての1007問題の1325の定理が証明された。
翻訳されたLeanプログラムは、ベンチマークのテストケースの21,413で実行され、すべてのRustプログラムと同じ出力を生成する。
- 参考スコア（独自算出の注目度）: 4.212135305841799
- License:
- Abstract: VeriContest is a benchmark of 1007 competitive-programming problems in Rust, each with a Verus specification, a judge-accepted solution, and a Verus proof. Its authors report that proof generation is the bottleneck for frontier models: given the specification and the code, the best model produces an accepted Verus proof for 13.95% of the problems on the first attempt. We report on solving the same proof-generation task with Rust-Prover, a verifier for Rust backed by Lean 4. The Verus specification and the Rust code are restated and translated into Lean, each specification becomes a theorem, and agents prove the theorems with Lean's kernel as the final check. All 1325 theorems of all 1007 problems were proved. 1259 of them were proved in one run of under 32 hours on Claude Opus 5.5, at a median of 3.2 minutes and $1.17 per proof, and 70% of them on the first iteration. The restated specifications were checked against the benchmark's test suites, and reviewed where no suite applies. None was wrong or weakened. The translated Lean programs were run on 21,413 of the benchmark's test cases and produced the same output as the Rust programs on every one. Across four Claude and four GPT models at five reasoning-effort settings, every current frontier model proves nearly all of a ten-theorem sample at every setting, and more effort raises the cost without raising the number of proofs. The cheapest Claude setting, Sonnet 5.5 at low effort, proves all of the 50 hardest theorems. We also rerun the benchmark's own Verus protocol with Claude Opus 5.5 on the 50 problems with the longest reference proofs. Opus 5.5 alone fails to prove one of them.
- Abstract（参考訳）: VeriContestは、Rustにおける1007の競合プログラミング問題のベンチマークである。
それらの著者は、証明生成はフロンティアモデルのボトルネックであると報告している: 仕様とコードを考えると、最良のモデルは最初の試みにおける問題の13.95%について許容されるVerusの証明を生成する。
我々は、Lean 4.0が支援するRustの検証ツールであるRust-Proverで、同じ証明生成タスクを解決することを報告します。
Verus仕様とRustコードは更新され、Leanに変換され、各仕様は定理となり、エージェントはLeanのカーネルを最終チェックとして定理を証明する。
すべての1007問題の1325の定理が証明された。
そのうち1259人はクロード・オプス5.5で32時間以下で1回、中央値は3.2分、証明1回につき1.17ドル、うち70%は1回目で証明された。
更新された仕様は、ベンチマークのテストスイートに対してチェックされ、スイートが適用されない場所をレビューした。
誤りも弱体化もしなかった。
翻訳されたLeanプログラムは、ベンチマークのテストケースの21,413で実行され、すべてのRustプログラムと同じ出力を生成する。
4つのクロードモデルと4つのGPTモデルを5つの理由付けで比較し、現在のフロンティアモデルは全て、すべての設定で10理論サンプルのほぼ全てを証明し、より多くの労力が証明数を増やすことなくコストを上昇させる。
最も安価なクロード条件であるソンネット5.5は、最も難しい50の定理を証明している。
また、最も長い参照証明を持つ50の問題について、Claude Opus 5.5でベンチマーク独自のVerusプロトコルを再実行します。
オプス5.5だけは、そのうちの1つを証明できない。
関連論文リスト
- Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing [5.8296917468117835]
我々は,Lean 4コンパイラを報奨託書として純粋に扱う3ロールのMonte Carlo Tree Search (MCTS)フレームワークを提案する。
本フレームワークは,証明探索を3つの役割に分解する:証明試行ジェネレータ,サブゴール分解の分解器,サブゴール品質評価の批判器である。
PAB@256 で Goedel-Prover-V2-8B を用いて MiniF2F の87.1% を達成し,PAB@32 で26/659 パットナムベンチ問題を同じ証明試行予算で 18/659 を突破した。
論文 参考訳（メタデータ） (2026-08-11T04:28:22Z) - Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study [0.20415910628419062]
大規模言語モデル(LLM)は数学的証明に類似したテキストを生成することができるが、類似性は正確性を確立しない。
Coqのルールは、システムのどの証明ステップが受け入れられるかを定義する論理的フレームワークであるCalculus of Inductive Constructionsに基づいている。
このパイロット研究は、実際のCoqプロジェクトから派生したベンチマークであるCoqStoqから、同じ100の定理で6つのオープンウェイトLSMを評価した。
論文 参考訳（メタデータ） (2026-08-05T21:29:12Z) - MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving [0.0]
MerLean-Proverは、残念な宣言をカーネルチェック可能な証明に置き換える、エンドツーエンドのLean4定理証明器である。
23のPhD-qualification-exam定理のベンチマークであるFormalQualBenchでは、MerLean-Proverは10/23を解く。
Sonnetは4つのテストされたFormalQualBench問題を全てクローズし、Haikuは2つの短い問題をクローズする。
論文 参考訳（メタデータ） (2026-05-26T12:49:49Z) - OProver: A Unified Framework for Agentic Formal Theorem Proving [33.14658302112269]
OProverは、Lean 4.0で証明された代理的な形式的な反復定理のための統一されたフレームワークである。
エージェント証明を実行し、新たに証明された証明をOProofsと検索メモリにインデックスし、修理軌跡をSFTデータとして使用し、未解決のハードケースをRLに使用する。
OProver-32BはMiniF2F (93.3%)、ProverBench (58.2%)、PutnamBench (11.3%)で最高のパス@32を獲得し、MathOlympiad (22.8%)、ProofNet (33.2%)で上位にランクインしている。
論文 参考訳（メタデータ） (2026-05-17T06:39:05Z) - 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) - Proving the Coding Interview: A Benchmark for Formally Verified Code Generation [3.5319285228327417]
FVAPPS (Formally Verified Automated Programming Progress Standards, FVAPPS) は,プログラムの記述と正確性を証明するための4715サンプルのベンチマークである。
我々は,機械学習とプログラム合成コミュニティに対して,汎用プログラミング問題とその関連した正当性仕様の解決に挑戦する。
論文 参考訳（メタデータ） (2025-02-08T22:54:58Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - Faithful Chain-of-Thought Reasoning [51.21714389639417]
CoT(Chain-of-Thought)は言語モデル(LM)のパフォーマンスを様々な推論タスクで向上させる。
翻訳と問題解決という2つの段階を含む推論フレームワークであるFithful CoTを提案する。
このことは、推論連鎖が最終回答の忠実な説明を提供することを保証している。
論文 参考訳（メタデータ） (2023-01-31T03:04:26Z) - PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。
本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。
我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文 参考訳（メタデータ） (2020-10-06T15:47:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。