GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving
Author
- Haebom
Category
Empty
저자
Ruida Wang, Jiarui Yao, Rui Pan, Shizhe Diao, Tong Zhang
개요
본 논문은 검증 가능한 언어를 활용하여 수학 문제를 해결하는 모델의 효율성을 높이기 위해, 문제 생성기와 해결사를 적대적 방식으로 함께 학습시키는 GAR (Generative Adversarial Reinforcement learning) 프레임워크를 제안합니다. 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 패러다임을 제시합니다.
시사점, 한계점
•
시사점:
◦
문제 생성기와 해결사의 적대적 학습을 통해 수학 문제 해결 모델의 효율성을 향상시킴.
◦
암묵적 교육 과정 학습을 통해 모델 훈련 효율성을 높임.
◦
MiniF2F-Test 및 ProofNet-Test 벤치마크에서 성능 향상을 입증.
◦
검증 가능한 환경에서 문제 생성과 해결의 공동 진화를 위한 일반적인 RL 패러다임을 제시.
•
한계점:
◦
논문에 구체적인 한계점에 대한 언급은 없음.
