Fugu-MT 論文翻訳(概要): GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

論文の概要: 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パラダイムを確立している。

関連論文リスト

Actor-Curator: Co-adaptive Curriculum Learning via Policy-Improvement Bandits for RL Post-Training [63.34044358216334]
ACTOR-CURATORは、大規模言語モデルの強化学習のためのスケーラブルで完全に自動化されたカリキュラム学習フレームワークである。経験的に、ACTOR-CURATORは一貫して一様サンプリングと強力なカリキュラムベースラインを上回っている。
論文参考訳（メタデータ） (2026-02-24T04:19:48Z)
CVeDRL: An Efficient Code Verifier via Difficulty-aware Reinforcement Learning [57.24524263804788]
コード検証は、LLMベースのコード生成の検証後において重要な役割を果たす。既存の教師付き微調整手法は、データの不足、高い失敗率、推論効率の低下に悩まされている。機能的な報酬しか持たない単純RLは、難しいブランチやサンプルに対して効果的な単体テストを生成することができないことを示す。
論文参考訳（メタデータ） (2026-01-30T10:33:29Z)
ProRAG: Process-Supervised Reinforcement Learning for Retrieval-Augmented Generation [54.071574153853994]
ProRAGは、学習段階の監視をオンライン最適化ループに統合するために設計されたプロセス教師付き強化学習フレームワークである。本フレームワークは,(1)構造化推論形式でモデルを初期化するための監視されたポリシーワームアップ,(2)中間推論品質を定量化するためのMCTSベースのプロセスリワードモデル(PRM)の構築,(3)細粒度プロセスの好みに合わせてポリシーを調整するためのPRM誘導推論リファインメント,(4)プロセススーパービジョン強化学習と2つのグラニュラリティー・アドバンテージ・メカニズムの4段階から構成される。
論文参考訳（メタデータ） (2026-01-29T16:04:59Z)
DRIVE: Data Curation Best Practices for Reinforcement Learning with Verifiable Reward in Competitive Code Generation [5.496363733566038]
我々は、RLVR(すなわち、RLプロンプト)を構築し、競争プログラミングコード生成に強力なパフォーマンスをもたらすトレーニング技術を示す。本手法はQwen2.5-32B上で実装され,LeetCodeとCodeforcesの毎週のコンテストでデータ漏洩を回避する。結果として得られたモデルは、同様のスケールのモデル間で最先端のパフォーマンスを実現し、DeepSeek v3.1 や Doubao-1.5-Thinking のような主要なシステムに匹敵する。
論文参考訳（メタデータ） (2025-11-09T10:11:28Z)
ATGen: Adversarial Reinforcement Learning for Test Case Generation [78.48498301767079]
大きな言語モデル(LLM)はコード生成に優れていますが、その出力には微妙なバグが伴います。既存のテスト生成方法は静的データセットに依存している。我々は,対戦型強化学習を通じてテストケースジェネレータを訓練するフレームワークであるATGenを紹介する。
論文参考訳（メタデータ） (2025-10-16T12:49:25Z)
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)
Zero-Sum Positional Differential Games as a Framework for Robust Reinforcement Learning: Deep Q-Learning Approach [2.3020018305241337]
本稿では、位置微分ゲーム理論におけるRRL問題を考慮した最初の提案である。すなわち、イザックの条件の下では、同じQ-函数をミニマックス方程式とマクシミン・ベルマン方程式の近似解として利用することができる。本稿ではIssas Deep Q-Networkアルゴリズムについて,他のベースラインRRLやMulti-Agent RLアルゴリズムと比較して,その優位性を示す。
論文参考訳（メタデータ） (2024-05-03T12:21:43Z)

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

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