論文の概要: Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning
- arxiv url: http://arxiv.org/abs/2507.08649v1
- Date: Fri, 11 Jul 2025 14:53:14 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-07-14 18:03:54.393302
- Title: Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning
- Title（参考訳）: Leanabell-Prover-V2:強化学習による形式的定理証明のための検証器積分推論
- Authors: Xingguang Ji, Yahui Liu, Qi Wang, Jingyuan Zhang, Yang Yue, Rui Shi, Chenxi Sun, Fuzheng Zhang, Guorui Zhou, Kun Gai,
- Abstract要約: われわれはLean 4で公式な定理を証明できる7Bの大規模言語モデル(LLM)であるLeanabell-Prover-V2を紹介します。
主に、Lean 4検証者からのフィードバックで強化学習(RL)をアップグレードしています。
実験の結果、Leanabell-Prover-V2はKimina-Previewer-Distill-7Bで3.2%改善し、DeepSeek-Prover-V2-7Bで2.0%改善した。
- 参考スコア（独自算出の注目度）: 26.794050801484346
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We introduce our Leanabell-Prover-V2, a 7B large language models (LLMs) that can produce formal theorem proofs in Lean 4, with verifier-integrated Long Chain-of-Thoughts (CoT). Following our previous work Leanabell-Prover-V1, we continual to choose to posttrain existing strong prover models for further performance improvement. In our V2 version, we mainly upgrade the Reinforcement Learning (RL) with feedback provided by the Lean 4 verifier. Crucially, verifier feedback, such as indicating success or detailing specific errors, allows the LLM to become ``self-aware'' of the correctness of its own reasoning process and learn to reflexively correct errors. Leanabell-Prover-V2 directly optimizes LLM reasoning trajectories with multi-turn verifier interactions, together with feedback token masking for stable RL training and a simple reward strategy. Experiments show that Leanabell-Prover-V2 improves performance by 3.2% (pass@128) with Kimina-Prover-Preview-Distill-7B and 2.0% (pass@128) with DeepSeek-Prover-V2-7B on the MiniF2F test set. The source codes, curated data and models are available at: https://github.com/Leanabell-LM/Leanabell-Prover-V2.
- Abstract（参考訳）: 私たちはLeanabell-Prover-V2を紹介します。これは7Bの大規模言語モデル(LLM)で、検証器統合のLong Chain-of-Thoughts(CoT)を使ってLean 4で公式な定理の証明を作成できます。
前回のLeanabell-Prover-V1に続いて、パフォーマンス改善のために、既存の強力な証明モデルを延期することを選択しました。
V2バージョンでは、主にLean 4検証者からのフィードバックで強化学習(RL)をアップグレードしています。
重要なことは、検証者からのフィードバック、例えば成功を示すか、特定のエラーの詳細を示すことは、LSMが自身の推論プロセスの正しさを‘self-aware’(自己認識)’し、エラーを反射的に修正することを学ぶことを可能にする。
Leanabell-Prover-V2は、LLM推論トラジェクトリとマルチターン検証器の相互作用を直接最適化し、フィードバックトークンマスキングにより安定したRLトレーニングと単純な報酬戦略を実現する。
実験の結果、Leanabell-Prover-V2はKimina-Prover-Preview-Distill-7Bで3.2%(pass@128)、DeepSeek-Prover-V2-7Bで2.0%(pass@128)、MiniF2Fテストセットでパフォーマンスが改善された。
ソースコード、キュレートされたデータ、モデルは、https://github.com/Leanabell-LM/Leanabell-Prover-V2.comで入手できる。
関連論文リスト
- Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction [95.91743732150233]
一連のオープンソースの言語モデルであるGoedel-Prover-V2は、自動定理の新たな最先端を証明した。
我々は、より複雑な定理をマスターするためにモデルを訓練することの困難さを増す合成タスクを生成する。
Goedel-Prover-V2-32Bは、標準モードのpass@32でMiniF2Fの88.1%、自己補正モードの90.4%を達成する。
論文 参考訳（メタデータ） (2025-08-05T16:28:22Z) - VerIF: Verification Engineering for Reinforcement Learning in Instruction Following [55.60192044049083]
検証可能な報酬(RLVR)による強化学習は、大規模言語モデル(LLM)の強化の鍵となる技術となっている。
ルールベースのコード検証とLLMベースの大規模な推論モデルによる検証を組み合わせた検証手法であるVerIFを提案する。
我々はVerIFを用いたRLトレーニングを2つのモデルに適用し、いくつかの代表的な命令追従ベンチマークで大幅に改善した。
論文 参考訳（メタデータ） (2025-06-11T17:10:36Z) - GuardReasoner-VL: Safeguarding VLMs via Reinforced Reasoning [43.89818154399979]
本稿では,GardReasoner-VLと呼ばれる推論に基づく新しいVLMガードモデルを提案する。
123Kサンプルと631K推論ステップを備えた推論コーパスであるGuardReasoner-VLTrainを構築する。
性能とトークン効率のバランスをとるために,精度,フォーマット,トークンコストを一体化して,長さ認識型安全報酬を設計する。
論文 参考訳（メタデータ） (2025-05-16T09:46:10Z) - Leanabell-Prover: Posttraining Scaling in Formal Reasoning [26.534511088861446]
本稿では, 自然言語の推論モデルにおけるブレークスルーと整合性を持たせることを目的として, ATPのポストトレーニング全体について検討する。
我々は,DeepSeek-Prover-v1.5やGoedel-Proverなど,既存のフォーマルプロバーの改良に成功した。
論文 参考訳（メタデータ） (2025-04-08T15:15:26Z) - LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
証明の進捗を予測する手法であるLeanProgressを紹介します。
実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
論文 参考訳（メタデータ） (2025-02-25T07:46: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) - LLM2: Let Large Language Models Harness System 2 Reasoning [65.89293674479907]
大規模言語モデル(LLM)は、無数のタスクにまたがって印象的な機能を示してきたが、時には望ましくない出力が得られる。
本稿では LLM とプロセスベースの検証器を組み合わせた新しいフレームワーク LLM2 を紹介する。
LLMs2は妥当な候補を生成するのに責任を持ち、検証者は望ましい出力と望ましくない出力を区別するためにタイムリーなプロセスベースのフィードバックを提供する。
論文 参考訳（メタデータ） (2024-12-29T06:32:36Z) - Language Models are Hidden Reasoners: Unlocking Latent Reasoning Capabilities via Self-Rewarding [74.31981011985681]
大きな言語モデル(LLM)は印象的な機能を示しているが、それでも複数のステップを必要とする複雑な推論タスクに苦戦している。
LaTRO(LaTent Reasoning Optimization)は、潜在分布からのサンプリングとして推論を定式化するためのフレームワークである。
複数のモデルアーキテクチャを用いて、GSM8KおよびARC-Challengeデータセットの実験を通してLaTROを検証する。
論文 参考訳（メタデータ） (2024-11-06T22:02:30Z) - Coarse-Tuning Models of Code with Reinforcement Learning Feedback [0.0]
コード上で事前訓練されたLarge Language Models (LLM) が、プログラム合成の主流のアプローチとして登場した。
コードの品質を評価する接地関数からのフィードバックを用いて、強化学習により事前学習したLLMをさらに訓練するRCCFを提案する。
論文 参考訳（メタデータ） (2023-05-25T22:09:08Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。