GAR: 形式的定理証明のための生成的敵対的強化学習

要旨

Leanなどの検証可能な言語を用いた数学問題の解決は、数学とコンピュータサイエンスの両コミュニティに大きな影響を与えてきた。現在の最先端モデルは、高コストなオンライン強化学習（RL）や専門家反復法を用いて訓練されることが多い。しかし、これらのアプローチは固定された問題セットに依存しており、訓練の非効率性を引き起こし、複雑な問題に対処する能力を制限している。これらの制限を克服するため、我々はGAR（Generative Adversarial Reinforcement learning）を提案する。GARは、問題作成者と解決者を敵対的ループで共同訓練する包括的なRL訓練フレームワークである。GARは暗黙的なカリキュラム学習メカニズムを導入し、タスクの難易度を証明者の進化する能力に合わせることで、訓練効率を向上させ、高度な定理の証明においてより強力な性能を発揮することを可能にする。実験結果によると、GAR訓練により、Goedel-Prover-V2-8BとDeepSeek-Prover-V2-7BはMiniF2F-Testベンチマークにおいてpass@32で平均4.20%の相対的改善を達成し、DeepSeek-Prover-V2のProofNet-Testにおけるpass@32は22.58%から25.81%に増加した。形式的証明を超えて、GARは検証可能な環境下での問題生成と解決の共進化のための一般的なRLパラダイムを確立する。

English

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.

GAR: 形式的定理証明のための生成的敵対的強化学習

GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

要旨

Support