論文の概要: GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

• arxiv url: http://arxiv.org/abs/2510.11769v1
• Date: Mon, 13 Oct 2025 17:56:25 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-15 19:02:32.041137
• Title: GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving
• Title（参考訳）: GAR:形式的定理証明のための生成的対向強化学習
• Authors: Ruida Wang, Jiarui Yao, Rui Pan, Shizhe Diao, Tong Zhang,
• Abstract要約: 本稿では,GAR:Generative Adversarial Reinforcement Learningを提案する。 GARは暗黙のカリキュラム学習機構を導入し、課題の難易度を証明者の進化能力と整合させる。 GARトレーニングでは、Goedel-Prover-V2-8BとDeepSeek-Prover-V2-7Bが、MiniF2F-Testベンチマークで平均4.20%のパス@32の平均相対的な改善を実現している。
• 参考スコア（独自算出の注目度）: 23.743060792178067
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Solving math problems through verifiable languages such as Lean has significantly impacted both the mathematics and computer science communities. Current state-of-the-art models are often trained with expensive online Reinforcement Learning (RL) or expert iteration. However, these approaches rely on fixed problem sets, which causes inefficient training and limits the model to tackle complex problems. To overcome these limitations, we propose GAR: Generative Adversarial Reinforcement learning, a comprehensive RL training framework that jointly trains the problem composer and solver in an adversarial loop. GAR introduces an implicit curriculum learning mechanism, which aligns task difficulty with the prover's evolving capability. It thereby improves the training efficiency and enables stronger performance of proving advanced theorems. Experiments show that with GAR training, Goedel-Prover-V2-8B and DeepSeek-Prover-V2-7B achieve an average relative improvement in pass@32 of 4.20% on MiniF2F-Test benchmark, while DeepSeek-Prover-V2's pass@32 on ProofNet-Test increases from 22.58% to 25.81%. Beyond formal proving, GAR establishes a general RL paradigm for co-evolution of problem generation and solving under verifiable environments.
• Abstract（参考訳）: リーンのような検証可能な言語による数学問題の解決は、数学とコンピュータサイエンスのコミュニティに大きな影響を与えている。 現在の最先端モデルは、高価なオンライン強化学習(RL)やエキスパートのイテレーションでトレーニングされることが多い。 しかし、これらのアプローチは固定された問題集合に依存しており、これは非効率なトレーニングを引き起こし、複雑な問題に取り組むためにモデルに制限を与える。 これらの制約を克服するために、GAR: Generative Adversarial Reinforcement Learning, 総合的なRLトレーニングフレームワークを提案する。 GARは暗黙のカリキュラム学習機構を導入し、課題の難易度を証明者の進化能力と整合させる。 これにより、訓練効率が向上し、高度な定理の証明性能が向上する。 GARトレーニングでは、Goedel-Prover-V2-8BとDeepSeek-Prover-V2-7Bが、MiniF2F-Testベンチマークで平均4.20%のパス@32、ProofNet-TestでDeepSeek-Prover-V2のパス@32が22.58%から25.81%に向上した。 形式的証明の他に、GARは、検証可能な環境下での問題解決と問題生成の共進化のための一般的なRLパラダイムを確立している。

関連論文リスト

• Staying in the Sweet Spot: Responsive Reasoning Evolution via Capability-Adaptive Hint Scaffolding [59.60915947702282]
  検証可能な報酬(RLVR)による強化学習は,大規模言語モデル(LLM)の推論能力の向上に成功している。 既存のRLVR手法は、訓練データの困難さとモデルの能力のミスマッチにより、探索の非効率に悩まされることが多い。 本稿では,高効率領域に留まることの難易度を動的に調整する新しい監視支援RLVRフレームワークであるSEELEを提案する。
  論文  参考訳（メタデータ） (2025-09-08T17:36:21Z)
• UR$^2$: Unify RAG and Reasoning through Reinforcement Learning [17.319590573147565]
  大規模言語モデル(LLM)は2つの相補的パラダイムを通じて顕著な能力を示してきた: 検索-拡張生成(RAG)と、検証リワード(RLVR)からの強化学習(Reinforcement Learning)である。 我々は、強化学習による検索と推論を統一する一般的なフレームワークUR2(Unified RAG and Reasoning)を提案する。 オープンドメインQA、MMLU-Pro、医学、数学的推論タスクにわたる実験は、UR$2$が既存のRAG法とRL法を大幅に上回ることを示した。
  論文  参考訳（メタデータ） (2025-08-08T09:33:20Z)
• Beyond Accuracy: Dissecting Mathematical Reasoning for LLMs Under Reinforcement Learning [82.43575191712726]
  本稿では,強化学習が推論に与える影響を明らかにするための,きめ細かい分析フレームワークを提案する。 本フレームワークは,RLトレーニングの恩恵を受けると仮定された重要な要素を具体的に調査する。
  論文  参考訳（メタデータ） (2025-06-05T07:53:59Z)
• Maximizing Confidence Alone Improves Reasoning [48.83927980325788]
  RENT: エントロピー最小化による強化学習(Reinforcement Learning via Entropy Minimization)は、完全な教師なしのRL手法であり、外部の報酬や地道的な回答を必要としない。 得られた回答に高いモデル信頼をもたらす思考の連鎖を強化することで、モデルは推論能力を向上させる。
  論文  参考訳（メタデータ） (2025-05-28T17:59:37Z)
• LoRanPAC: Low-rank Random Features and Pre-trained Models for Bridging Theory and Practice in Continual Learning [103.45785408116146]
  連続学習(CL)は、連続的に提示される複数のタスクを解決できるモデルを訓練することを目的としている。 最近のCLアプローチは、ダウンストリームタスクをうまく一般化する大規模な事前学習モデルを活用することで、強力なパフォーマンスを実現している。 しかし、これらの手法には理論的保証がなく、予期せぬ失敗をしがちである。 理論的に健全で高性能な単純なCL法を設計することで,このギャップを埋めることを目指している。
  論文  参考訳（メタデータ） (2024-10-01T12:58:37Z)

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

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