GAR: 형식적 정리 증명을 위한 생성적 적대 강화 학습

GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

October 13, 2025

저자: Ruida Wang, Jiarui Yao, Rui Pan, Shizhe Diao, Tong Zhang

cs.AI

초록

Lean과 같은 검증 가능한 언어를 통해 수학 문제를 해결하는 것은 수학 및 컴퓨터 과학 커뮤니티에 상당한 영향을 미쳤습니다. 현재 최첨단 모델들은 종종 비용이 많이 드는 온라인 강화 학습(Reinforcement Learning, 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.