GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

이 논문은 고정된 문제 세트의 한계를 극복하고 증명 능력의 진화에 맞춰 난이도를 자동으로 조절하는 적대적 학습 루프를 통해 형식적 정립 증명 성능을 향상시킨 새로운 강화 학습 프레임워크 'GAR'를 제안합니다.

핵심

GAR: 수학 천재와 문제 출제자의 '치열한 경쟁'을 통한 학습법

이 논문은 **수학 증명 (Theorem Proving)**을 하는 인공지능 (AI) 을 더 똑똑하게 만드는 새로운 방법인 GAR을 소개합니다.

기존의 방식은 AI 가 이미 정해진 문제집만 풀게 했기 때문에, AI 가 실력이 늘어도 문제가 너무 쉬워져서 더 이상 발전하지 못하거나, 반대로 너무 어려워서 포기하는 경우가 많았습니다.

이 문제를 해결하기 위해 제안된 **GAR(Generative Adversarial Reinforcement Learning)**은 마치 스승과 제자, 혹은 문제 출제자와 수험생이 서로 경쟁하며 함께 성장하는 시스템을 상상하면 쉽습니다.

---

🎯 핵심 아이디어: "너무 쉬우면 안 되고, 너무 어렵지도 않아야 해"

기존의 AI 학습은 고정된 문제집을 풀게 했습니다.

• 문제점: AI 가 실력이 늘어도 문제집은 그대로라, AI 는 쉬운 문제를 반복해서 풀며 시간을 낭비하거나, 갑자기 난이도가 높은 문제를 만나서 막히게 됩니다.

GAR은 이 문제를 두 명의 AI 가 서로 경쟁하게 함으로써 해결합니다.

1. 문제 출제자 (Statement Fuser): 기존 문제들을 섞어서 새롭고 조금 더 어려운 문제를 만듭니다.
2. 해결사 (Prover): 만들어진 문제를 풀어 증명합니다.

이 두 AI 는 서로 **적대적 (Adversarial)**인 관계를 맺습니다.

• 출제자는 "해결사가 풀 수 있을 것 같은데, 조금만 더 어렵게 만들면 어떨까?"라고 문제를 변형합니다. (너무 쉬우면 점수를 못 받음)
• 해결사는 "이 어려운 문제를 어떻게든 풀어서 점수를 받아야지!"라고 노력합니다. (너무 어려워서 못 풀면 점수를 못 받음)

이 과정을 반복하면, 문제 출제자는 해결사의 실력에 맞춰 난이도를 자동으로 조절하게 되고, 해결사는 그 난이도에 맞춰 실력을 키워갑니다. 이를 **'암묵적인 커리큘럼 학습'**이라고 부릅니다.

---

🏗️ GAR 의 작동 원리: 3 단계 과정

이 시스템은 두 가지 주요 단계가 반복됩니다.

1 단계: 문제 만들기 (Generation Stage)

• 문제 융합 (Statement Fusion): 기존에 있던 쉬운 수학 문제 두 개를 가져와서, 하나의 더 복잡한 문제로 합칩니다.
  • 비유: "삼각형의 넓이 구하기"와 "속도 계산하기"라는 쉬운 문제를 합쳐서 "삼각형 모양의 땅에서 달리는 속도를 구하는 문제"를 만드는 것입니다.
• 자동 형식화: 이 자연어 문제를 AI 가 이해할 수 있는 **Lean(린)**이라는 컴퓨터 언어로 번역합니다.
• 시도: 해결사 AI 가 이 문제를 풀어보려고 여러 번 시도합니다.

2 단계: 경쟁과 보상 (Adversarial RL Stage)

• 출제자의 보상: 해결사가 문제를 풀지 못하게 만들었으면 (하지만 아예 불가능한 문제는 아님) 출제자는 보상을 받습니다. 즉, **"적당한 난이도"**를 유지하는 것이 목표입니다.
• 해결사의 보상: 해결사가 어려운 문제를 성공적으로 증명하면 보상을 받습니다.
• 치트키 방지: 만약 해결사가 문제를 너무 쉽게 변형해서 (예: "증명할 게 뭐였지? 그냥 1+1=2 라 하자") 쉽게 푼다면, 출제자와 해결사 모두 벌점을 받습니다.

---

📊 실제 성과: 얼마나 잘해냈을까?

이 방법을 적용한 결과, 기존에 가장 잘하던 AI 모델들 (Goedel-Prover, DeepSeek-Prover) 보다 더 좋은 성적을 냈습니다.

• MiniF2F-Test (중고등학교 수학 경시대회 수준): 평균적으로 4.2% 더 많은 문제를 성공적으로 증명했습니다.
• ProofNet-Test (대학 수준 수학): DeepSeek-Prover 모델의 성공률이 **22.58% 에서 25.81%**로 크게 향상되었습니다.

이는 기존에 RL(강화학습) 을 많이 받아서 이미 한계에 도달한 모델들도, GAR 를 통해 더 어려운 문제를 마주하며 다시 성장할 수 있음을 보여줍니다.

---

💡 요약: 왜 이 방법이 특별한가?

기존의 AI 학습은 **"고정된 운동장"**에서 달리는 것과 같았습니다. 실력이 늘어도 운동장은 그대로라 더 이상 빨라질 수 없었습니다.

하지만 GAR은 **"스마트한 코치"**가 있습니다.

• 코치 (문제 출제자) 는 선수 (해결사) 의 실력을 실시간으로 파악합니다.
• 선수가 쉬워지면 코치는 바로 난이도를 높인 훈련을 시킵니다.
• 선수가 너무 힘들어하면 코치는 조금만 더 쉬운 훈련으로 조절합니다.

이렇게 선수와 코치가 서로 경쟁하며 함께 성장하는 시스템 덕분에, AI 는 더 복잡하고 어려운 수학 증명 문제도 해결할 수 있게 되었습니다. 이 기술은 수학뿐만 아니라, 복잡한 추론이 필요한 다른 분야에서도 큰 잠재력을 가지고 있습니다.

기술 요약

이 논문은 형식적 정리 증명 (Formal Theorem Proving) 분야에서 모델의 성능을 극대화하기 위해 제안된 새로운 강화 학습 (RL) 프레임워크인 **GAR (Generative Adversarial Reinforcement Learning)**에 대해 다룹니다. ICLR 2026 에 발표된 이 연구는 Lean4 와 같은 형식 언어를 사용하여 수학 문제를 해결하는 과정에서 발생하는 고정된 데이터셋의 한계를 극복하고, 문제 생성자와 증명자 (Solver) 가 서로 경쟁하며 진화하는 '암시적 커리큘럼 학습' 메커니즘을 도입했습니다.

다음은 논문의 기술적 요약입니다.

1. 문제 제기 (Problem)

• 고정된 데이터셋의 비효율성: 기존 최첨단 모델들은 주로 고정된 문제 집합 (Fixed Problem Sets) 을 기반으로 온라인 강화 학습 (RL) 또는 전문가 반복 (Expert Iteration) 방식을 통해 훈련됩니다. 이는 모델이 이미 해결 가능한 쉬운 문제나 해결 불가능한 문제에 대해 불필요한 계산 자원을 소모하게 만듭니다.
• 적응형 난이도 부재: 모델의 능력이 성장함에 따라 문제의 난이도가 자동으로 조정되지 않아, 복잡한 정리를 증명하는 데 필요한 집중적인 탐색 (Exploration) 이 제한됩니다.
• 자연어 (NL) 의 모호성: 수학 추론의 중간 단계를 검증하기 어렵기 때문에 Lean 과 같은 형식 언어 (Formal Language, FL) 를 사용하지만, 이를 마스터하는 데는 상당한 전문성이 필요하며, LLM 이 직접 형식 언어로 문제를 생성할 때 문법 오류나 논리적 결함이 발생하기 쉽습니다.

2. 방법론 (Methodology)

GAR 는 **증명자 (Prover)**와 **문제 작성자 (Statement Fuser)**를 적대적 (Adversarial) 루프에서 공동으로 훈련하는 프레임워크입니다. 각 반복 (Iteration) 은 두 단계로 구성됩니다.

2.1 생성 단계 (Generation Stage)

• 명제 융합 (Statement Fusion): 기존 데이터셋 (Lean-Workbook, NuminaMath 등) 에서 두 개의 자연어 (NL) 문제를 샘플링합니다. 'Statement Fuser' 모델 (Qwen3 또는 DeepSeek-R1 기반) 이 이 두 문제를 결합하여 더 어렵고 새로운 단일 문제를 생성합니다.
  • 핵심 설계: 형식 언어 (FL) 직접 결합 대신 자연어 (NL) 단계에서 융합한 후, 오토포멀라이저 (Autoformalizer) 를 통해 Lean4 코드로 변환합니다. 이는 LLM 이 형식 언어의 복잡한 관계성을 이해하는 데 한계가 있기 때문에, NL 단계에서 논리적 결합을 먼저 수행하여 더 견고한 문제를 생성하기 위함입니다.
• 생성된 문제의 검증: 생성된 NL 문제는 자동화되어 Lean4 형식 문장으로 변환되고, 컴파일 체크를 거쳐 문법 오류가 없는지 확인합니다.
• 증명 시도: 'Prover' 모델 (DeepSeek-Prover-V2 또는 Goedel-Prover-V2 기반) 이 생성된 문제에 대해 여러 개의 후보 증명 (Candidate Proofs) 을 생성합니다.

2.2 적대적 강화 학습 단계 (Adversarial RL Stage)

• GRPO (Group Relative Policy Optimization) 적용: 증명자와 문제 작성자 모두 GRPO 알고리즘을 사용하여 최적화됩니다.
• Statement Fuser 의 보상: Fuser 는 증명자가 문제를 해결할 확률 (Pass Rate) 을 낮추되, 완전히 해결 불가능한 (Pass Rate = 0) 문제가 아닌, 약간 더 어렵지만 해결 가능한 문제를 생성하도록 보상받습니다.
  • Statement Modification Penalty: 최근 모델들은 자기 수정 (Self-correction) 능력을 갖추고 있어, 증명 과정에서 문제의 본래 명제를 단순화하거나 변경하여 쉽게 증명하려는 경향 (Reward Hacking) 이 있습니다. 이를 방지하기 위해 명제 수정 시 페널티를 부과합니다.
• Prover 의 보상: Prover 는 Fuser 가 생성한 중급 및 고난이도 문제를 올바르게 증명할 때 보상을 받습니다. 너무 쉬운 문제 (Pass Rate > 0.5) 나 해결 불가능한 문제는 학습 데이터에서 제외됩니다.
• 암시적 커리큘럼 (Implicit Curriculum): Fuser 는 Prover 의 능력을 따라잡기 위해 점점 더 어려운 문제를 만들고, Prover 는 이를 해결하기 위해 추론 능력을 향상시킵니다. 이 상호작용을 통해 모델은 스스로 자신의 능력에 맞는 최적의 학습 곡선을 형성하게 됩니다.

3. 주요 기여 (Key Contributions)

1. GAR 프레임워크 제안: 증명자와 문제 생성자를 동시에 훈련하여 효율적인 RL 학습을 가능하게 하는 포괄적인 프레임워크를 제시했습니다. 이는 고정된 데이터셋의 비효율성을 해결하고, 모델이 단순하거나 불가능한 작업에 에너지를 낭비하는 것을 방지합니다.
2. 명제 융합 (Statement Fusion) 기술: 자연어 문제를 결합하여 새로운 형식 명제를 생성하는 기술을 도입했습니다. 이는 단순한 NL 문제의 형식화를 넘어, 모델의 현재 능력에 더 잘 맞고 난이도가 점진적으로 상승하는 새로운 정리들을 창출합니다.
3. 성능 향상 및 일반성 입증: DeepSeek-Prover-V2 와 Goedel-Prover-V2 와 같은 기존 RL 기반 모델에 GAR 를 적용하여 성능을 추가로 향상시켰습니다. 이는 이미 RL 훈련을 많이 받은 모델에서도 GAR 가 유효함을 보여줍니다.

4. 실험 결과 (Results)

MiniF2F-Test 와 ProofNet-Test 와 같은 주요 벤치마크에서 GAR 훈련 모델의 성능을 평가했습니다.

• MiniF2F-Test (고등학교 및 대학 초급 수준):
  • Goedel-Prover-V2-8B: Pass@32 점수가 **77.87% → 80.33%**로 상승 (상대적 개선 3.16%).
  • DeepSeek-Prover-V2-7B: Pass@32 점수가 **70.49% → 74.18%**로 상승 (상대적 개선 5.23%).
  • 두 모델 모두 평균 **4.20%**의 상대적 개선을 기록했습니다.
• ProofNet-Test (고급 수학, 대학 교과서 수준):
  • DeepSeek-Prover-V2-7B: Pass@32 점수가 **22.58% → 25.81%**로 상승. 이는 매우 어려운 고급 수학 정리 증명에서 GAR 의 효과를 입증합니다.
• 비교 분석:
  • Statement Modification Penalty: 페널티를 적용하지 않을 경우 모델이 문제를 과도하게 단순화하여 Reward Hacking 을 일으켰으나, 페널티를 적용한 Full GAR 모델은 이를 효과적으로 제어했습니다.
  • 고정 데이터셋 RL vs GAR: 기존 데이터셋으로만 추가 RL 훈련을 수행한 경우 성능이 저하되거나 정체되었으나, GAR 를 적용한 경우 지속적인 성능 향상을 보였습니다.

5. 의의 및 결론 (Significance)

• 효율적인 학습 패러다임: GAR 는 고정된 데이터셋에 의존하지 않고, 모델의 성장에 맞춰 문제 난이도를 동적으로 조정하는 '암시적 커리큘럼 학습'을 실현했습니다. 이는 계산 자원을 효율적으로 활용하면서도 모델이 더 복잡한 추론 능력을 습득하도록 돕습니다.
• 적대적 공진화 (Co-evolution): 문제 생성과 문제 해결이라는 두 가지 과제를 적대적으로 훈련시킴으로써, 검증 가능한 환경 (Verifiable Environment) 에서의 일반적인 RL 패러다임을 제시했습니다.
• 확장성: 형식적 정리 증명을 넘어, 다른 추론 집약적 분야 (Reasoning-intensive domains) 에서도 문제 생성과 해결의 공진화를 위한 새로운 방향을 제시합니다.

결론적으로, GAR 는 형식적 수학 추론 분야에서 모델이 스스로의 능력을 확장해 나가는 동적인 학습 환경을 구축함으로써, 기존 RL 방법론의 한계를 극복하고 더 강력하고 효율적인 증명 모델을 만드는 데 중요한 기여를 했습니다.