한 줄 요약 (TL;DR)
“끊어 쓰고(Truncate-and-Resume) 탐험하며(내재 보상 MCTS) Lean 4 증명을 찾자” – DeepSeek-Prover-V1.5는 7 B 모델로 miniF2F 63.5 % / *ProofNet 25.3 %*를 달성해 이전 SOTA를 +9.0 pp / +7.2 pp 앞지르면서도 탐색 샘플을 최대 64 × 절감했다.
핵심 아이디어
- Whole-proof의 단순·빠른 한 방 생성과
- Step-wise 탐색의 세밀한 피드백을
-
**“Truncate-and-Resume + RMaxTS”**라는 하이브리드 프레임으로 융합
- 끊어서 실패 직후 tactic state를 주석으로 붙여 이어 쓰기
- RMaxTS(intrinsic-reward MCTS + Discounted-UCB)로 희소 보상을 완화하며 트리를 확장
배경 – 그들이 해결한 문제
| 기존 패러다임 | 고질적 한계 |
|---|---|
| Whole-proof (한 번에 끝까지 작성) | 초반 오류가 후반까지 누적 → 긴 증명에서 실패율 ↑ |
| Step-wise 탐색 (트리 검색) | Lean 호출·MCTS 분기가 폭발 → 계산 비용 ↑ |
| Sparse Reward | “완전 성공(1) / 실패(0)”만 있어 RL 탐색 정체 |
결국 **“중간 피드백을 받으면서도 비용은 낮추는 길이 없을까?”**가 핵심 연구 공백이었다.
새로운 접근법 – DeepSeek-Prover-V1.5
- Truncate-and-Resume Whole-proof
실패한 줄까지 코드를 자르고, Lean 4가 내놓은 tactic state를 주석(
/- STATE: … -/)으로 삽입해 같은 프롬프트에 이어 쓰기. -
RMaxTS (MCTS with Intrinsic Reward & Discounted-UCB)
- 새 노드(미탐색 tactic state) 발견 시
R_int = 1 - 보상·방문수를 γ = 0.99로 감쇠한 DUCB로 분기 선택 → 최신 정보를 우선 반영
- 새 노드(미탐색 tactic state) 발견 시
- GRPO (On-policy, 정책 기반 RL) 32 개의 whole-proof roll-out을 z-score 가중치로 업데이트 + KL penalty(β = 0.02)로 안정화.
작동 원리 – 구체적인 예시로 살펴보기
-- 목표: tiny_thm : 0 + n = n
import Mathlib.Data.Nat.Basic
theorem tiny_thm (n : ℕ) : 0 + n = n := by
simp? -- Lean 에러: tactic 'simp?' not found
- 초안 실패 → Lean 오류 발생
- 끊고 이어 쓰기
simp? -- STATE: ⊢ 0 + n = n
- MCTS 선택 :
simp액션이 DUCB 점수 최대 - 확장·시뮬레이션 :
simp→rfl한 줄 더, Lean 검증 성공 - 보상 전파 :
(R_int = 1, R_ext = 1)이 γ-감쇠로 부모까지 전달 - 반복 : 예산 K (예: 6400) 안에서 최고 경로 채택 → 증명 완료 ✅
왜 통하나?
- 중간 state 주석이 compounding error를 차단
- Intrinsic reward가 ‘미지 영역’ 탐험을 장려
- DUCB가 비정상 보상을 빠르게 전파해 탐험↔활용 균형 유지
성능 검증 – 주요 결과
| 모델 (7 B) | 방식 | miniF2F-test | ProofNet-test | Lean 호출/샘플 |
|---|---|---|---|---|
| DeepSeek-P V1.5 + RMaxTS | Hybrid | 63.5 % | 25.3 % | 32 × 6 400 |
| DeepSeek-P V1.5 (RL only) | Whole | 60.2 % | 22.6 % | 16 × 6 400 |
| InternLM2-StepProver | Step | 54.5 % | 18.1 % | 64 × 더 많음 |
| DeepSeek-P V1 (이전) | Whole | 50.0 % | 21.0 % | – |
- 정확도 : +9 pp / +7.2 pp SOTA 갱신
- 샘플 효율 : 같은 55 % 수준을 InternLM2 대비 64 × 적은 샘플로 달성
우리의 관점 – 강점, 한계, 그리고 이 연구가 중요한 이유
강점 🟢
- 효율 SOTA – 정확도와 Lean 호출 비용을 동시에 개선
- 단일 모델·단순 파이프라인 – 7 B LLM 하나로 whole/step 두 전략 모두 커버
- Ablation 검증 – DUCB·intrinsic reward의 기여를 수치로 입증(–2 pp ↓ 제거 시)
한계 🔴
- Exploitation 부족 – critic / 가지치기 미도입 → 트리 폭 증가
- Lean-특화 의존성 – tactic state 형식이 Proof Assistant 마다 달라 이식 난도↑
- 여전히 비싼 탐색 – 7 B라도 수 만 샘플 + Lean 검증 수십 만 회 필요
- 벤치마크 좁음 – miniF2F·ProofNet 중등·학부 수준에 집중, 대규모 Mathlib 파일 미평가
이 연구가 중요한 이유 🌟
자동 정형증명을 **“정확도 60 % 장벽”**에서 한 단계 끌어올리며,
- 적은 자원으로 자동 보증(verification) 을 현실화할 여지를 넓혔다.
- “컴파일러 피드백 + LLM 탐색”이라는 일반 패턴을 제시해 코드·논리 생성 전반에 응용 가능성을 열었다.
다음 단계는?
- Partial-proof Critic – 가치 함수로 가지치기·early cutoff → Lean 호출 ↓
- File-level 증명 – 프로젝트 단위(다중 정리) 컨텍스트 처리
- Cross-PA 전이 – Isabelle·Coq 등으로 tactic-state idapter 연구
- MoE 스케일 + Distill – 파라미터 ↑ 후 경량화를 통한 추론 비용 절감
- Hard-aware Batch Search – KV sharing, GPU 메모리 최적화로 탐색 효율 높이기
- 사회적 영향 연구 – 자동 증명 오·남용 감시, 윤리·컴플라이언스 프레임워크 마련
Bottom line : Truncate-and-Resume + RMaxTS는 “적게 돌려 많이 맞추는” 새로운 증명 패러다임을 열었다. 이제 숙제는, 이 아이디어를 더 넓고 깊게—파일·도메인·시스템 규모로—확장하는 일이다.
토글을 클릭하면 논문에 대한 자세한 LLM 질의응답 내용을 확인할 수 있습니다.
▶️클릭하여 펼치기
프롬프트 1.1.1 (연구의 공백)
"논문의 'Introduction'과 'Related Work' 섹션을 분석하여, 이 연구가 명시적으로 해결하고자 하는 핵심적인 연구 공백(research gap), 기존 연구의 결정적 한계, 또는 미해결 질문이 무엇인지 설명해 줘. 저자들이 설명하는, 이 논문 출판 시점의 '최신 기술(state of the art)'은 어떤 상태였는지 요약해 줘."
결론 먼저 (TL;DR)
여전히 “증명 과정 전체(whole-proof) ↔ 한 단계씩(step-wise)” 두 접근이 따로 노는 것이 최대 약점이었다. DeepSeek-Prover-V1.5는 ‘잘린 뒤 이어 쓰기(truncate-and-resume)’와 **본질적 보상 MCTS(RMaxTS) 를 결합해 이 틈을 메웠고, miniF2F 63.5 %, ProofNet 25.3 %로 각각 기존 SOTA 대비 ▲9.0 pp, ▲7.2 pp 상승을 달성했다.**
1. 연구 공백 (Research Gap)
| 구분 | 세부 내용 | 왜 문제인가 |
|---|---|---|
| ① Whole-proof 방식의 누적 오차 | 중간 상태를 보지 못해 잘못된 추론이 후반부까지 전파 | 긴 증명에서 compounding error 심각 |
| ② Step-wise 방식의 계산 비용 | 매 단계 ↔ 프로버 간 왕복·트리 검색 필요 | Lean 4 검증 호출이 폭발, 추론 지연 ↑ |
| ③ 희소 보상(sparse reward) 문제 | “완전 성공(1)” / “실패(0)”만 존재 | 탐색이 초반에 정체돼 미증명 유지 |
핵심 질문: “중간 상태 피드백을 활용하면서도 whole-proof급 단순·고속 샘플링을 양립시킬 수 없을까?”
2. 기존 연구의 결정적 한계
| 계열 | 대표 연구 | 한계 |
|---|---|---|
| Proof-step (다단계) | GPT-f, ReProver, InternLM2-StepProver | 트리 크기 ∝ 증명길이, Lean 호출 수천 × ↑ |
| Whole-proof (단일 패스) | DSP, LEGO-Prover, DeepSeek-Prover-V1 | 중간 상태 미활용 → 긴 증명 오류 전파 |
| 탐색 보강형 | Hypertree Proof Search | 외적 UCB만 사용, 보상 희소성 해결 미흡 |
3. DeepSeek-Prover-V1.5가 제안한 해결책
-
Truncate-and-Resume 오류가 난 첫 지점에서 코드를 자르고, Lean tactic state를 주석으로 붙여 LLM이 이어서 증명을 작성 → whole-proof의 연속성 + step-wise의 피드백 수용.
-
RMaxTS (Intrinsic-reward MCTS)
- 새 tactic state를 만들면 내재 보상 1 부여 → 희소 보상 완화
- 할인 UCB(DUCB) 로 값 전파 가속 → 샘플 효율 ↑.
-
훈련 파이프라인 전반 강화
- 수식·코드 데이터 재사전학습
- CoT 주석 삽입 + tactic state 예측 SFT
- GRPO RL 로 Lean 검증 피드백 직접 최적화.
4. 출판 시점 최신 기술(State of the Art) 요약
| 모델 / 방법 | 방식 | miniF2F-test (Pass\@K) | ProofNet-test | 비고 |
|---|---|---|---|---|
| DeepSeek-Prover-V1 (7B) | Whole-proof | 50.0 % (16×4 096) | 21.0 % | 이전 자사 모델 |
| InternLM2-StepProver (7B) | Step-wise + 트리 | 54.5 % (64×3 200) | 18.1 % | 탐색 집중 |
| Hypertree Proof Search | Step-wise + MCTS | 41.0 % | — | Lean 4 |
| ReProver | Step-wise | — | 13.8 % | LeanDojo 기반 |
| 🔺 DeepSeek-Prover-V1.5 (이 논문) | Whole-proof (single) | 60.2 % (16×6 400) | 23.7 % | RL까지 |
| 🔺 V1.5 + RMaxTS | Hybrid MCTS | 63.5 % (32×6 400) | 25.3 % | 새 SOTA |
표의 Pass\@K는 논문 Table 1·2에서 인용.
5. 미해결 질문 & 향후 과제
-
Partial-proof 가치 함수(critic) 부재
- MCTS 내 프루닝·신속 가치 추정이 아직 없음 → RL + critic 연구 필요.
-
파일 단위 장기 맥락(Formalization-level) 확장
- 현재는 개별 정리(proof) 중심; 대형 Lean 프로젝트 전역 맥락은 제한적.
-
파라미터 규모 ↑ vs. 탐색 깊이 ↔ 자원
- 7 B에서도 CPU-Lean 콜 수천 × GPU 샘플 수만; 스케일 업 시 비용 균형 과제.
6. 한 눈에 보는 기여도
증명 정확도 ▲9 pp (miniF2F)
탐색 효율 Lean 호출 ×0.5 수준 (동일 성능 기준)
모델 공개 3단계(PT‧SFT‧RL) + 코드 + MCTS
DeepSeek-Prover-V1.5는 “증명 전략·탐색·훈련” 세 층을 동시에 개선하여, 형식 수학(Lean 4) 분야의 열위(accuracy <60 %) 상황을 단숨에 돌파했다.
프롬프트 1.1.2 (핵심 가설)
"이 논문의 중심 가설(central hypothesis) 또는 핵심 주장은 무엇인가? '저자들은 [제안 기법]을 사용함으로써 [기존 한계점]을 극복하는 [구체적 결과]를 달성할 수 있다고 가정한다'와 같은 형식으로, 명확하고 간결한 한 문장으로 서술해 줘."
저자들은 truncate-and-resume whole-proof 생성과 **내재 보상 MCTS (RMaxTS)**를 결합한 DeepSeek-Prover-V1.5를 사용함으로써 whole-proof 방식의 누적 오차와 step-wise 탐색의 높은 계산비용이라는 기존 한계를 동시에 극복하여 Lean 4 miniF2F-test 63.5 %, ProofNet 25.3 %로 기존 SOTA를 각각 9.0 %p·7.2 %p 경신할 수 있다고 가정한다.
프롬프트 1.2.1 (독창성 식별)
"논문 전체를 바탕으로, 가장 중요하고 독창적인 기여(contribution) 1~3가지를 구별되는 항목으로 나열해 줘. 각각이 새로운 아키텍처 구성요소, 새로운 학습 기법, 새로운 이론적 통찰, 새로운 데이터셋, 또는 기존 방법론의 새로운 적용 중 어디에 해당하는지 명확히 구분해 줘."
독창적 기여 3가지 — 한눈에 보기
| # | 기여 요약 | 분류(Category) | 왜 중요한가 |
|---|---|---|---|
| 1. “Truncate-and-Resume” + RMaxTS – 잘린 구간 뒤에 Lean tactic state 주석을 붙여 whole-proof를 이어 쓰고, – 내재(intrinsic) 보상을 주는 MCTS-변형 RMaxTS로 희소 보상을 완화 |
새로운 탐색 / 알고리즘 | whole-proof 방식의 누적 오차와 step-wise 트리 탐색의 계산 폭증을 동시에 해결, miniF2F-test 63.5 %로 SOTA + 9.0 pp 달성 | |
| 2. CoT + Tactic-State 주석이 삽입된 Lean 4 데이터셋 (9.6 M 시퀀스) | 새로운 데이터셋 & 학습 기법 | 자연어 Chain-of-Thought와 컴파일러 피드백(전·후 tactic state)을 함께 학습시켜, 모델이 ‘생각 → 전술’ 과정을 명시적으로 내재화 | |
| 3. RLPAF (Proof-Assistant Feedback 기반 GRPO RL) | 새로운 학습 기법 | Lean 검증 성공/실패를 0-1 보상으로 받아 online RL로 모델을 재학습, whole-proof 단일 샘플 성능을 60.2 %까지 끌어올림 |
요약: 논문은 탐색 구조(1) + 데이터/표현(2) + 학습 파이프라인(3) 세 축을 모두 새로 디자인하여, 7 B 모델로도 기존 SOTA를 크게 넘어서는 Lean 4 정형증명 성능을 실현했다.
프롬프트 1.2.2 (저자 관점에서의 강점)
"저자들의 관점에서, 자신들의 접근법이 이전 방법들보다 우월한 이유는 무엇인가? 그들이 자신들의 연구가 지닌 독창성과 강점을 뒷받침하기 위해 사용하는 핵심 논거를 인용하거나 알기 쉽게 설명해 줘."
결론 먼저 (TL;DR)
“우리는 truncate-and-resume whole-proof + 내재 보상 MCTS(RMaxTS)라는 ‘하이브리드’ 설계를 통해, 기존보다 더 적은 샘플·Lean 호출로도 miniF2F 63.5 %, ProofNet 25.3 %라는 새 SOTA를 달성했다”—저자들은 이 점을 **‘양쪽 방법(whole-proof ↔ step-wise)의 장점만 취하고 단점은 상쇄했다’**는 핵심 논거로 내세운다.
1. 저자들이 주장하는 ‘우월성’ 세 가지 핵심 논거
| # | 저자 주장(요약) | 구체 근거·수치(논문 인용) | 왜 강점인가 |
|---|---|---|---|
| 1. 두 세계를 잇는 ‘하이브리드 탐색’ 단일 모델·단일 목표로 whole-proof 생성 ↔ step-wise 탐색을 모두 수행할 수 있다. |
“…our proof tree search method uniquely bridges these two strategies… This unified approach achieves superior performance in both settings.” | 기존에는 두 패러다임이 상호 배타적이어서 성능·자원 효율 간 트레이드오프가 발생. 하나의 파이프라인으로 둘 다 커버해 오류 전파↓ + Lean 호출↓ | |
| 2. 성능 vs 연산량 ‘양립’ 63.5 %(miniF2F)·25.3 %(ProofNet) ↗ but 샘플 3 200 ↔ 경쟁 모델 204 800(=64×3 200) |
“V1.5-RL requires only 3 200 whole-proof samplings to reach 54.9 %, surpassing InternLM2-StepProver, which needs 64 × 3 200 searches for 54.5 %.” | 샘플 효율 64 × 개선 → 계산·시간 비용 대폭 절감 | |
| 3. 탐색 가속을 뒷받침하는 **RMaxTS 설계 희소 보상을 극복하는 **내재 보상 + Discounted UCB → 표준 UCT 대비 +2 pp↑ |
Ablation에서 intrinsic-reward·DUCB가 없으면 성능이 UCT 수준으로 하락 | 탐색 자체의 품질·속도를 개선 → 동일 샘플에서도 성공률 상승 |
2. 저자 관점의 ‘독창적 강점’ 풀어서 보기
- “Unified yet simple” – 단일 7 B LLM만으로 whole-proof와 tree-search를 모두 다루므로 파라미터·코드 복잡도를 키우지 않고도 두 전략의 이점을 함께 얻을 수 있다.
- “Sample-Efficient SOTA” – pass\@K 63.5 %는 이전 최고치(InternLM2-StepProver 54.5 %) 대비 +9.0 pp, Lean 호출은 ≈ ½ 수준.
- “RL이 근본 능력 자체를 키운다” – SFT → RL 단계에서 miniF2F +3.7 pp 향상; 이는 ‘Top-K 운’이 아니라 기저(capability) 상승임을 그래프로 입증.
3. 숫자로 요약하는 강점
| 지표 | DeepSeek-P V1 | InternLM2-Step | V1.5 (RL + RMaxTS) |
|---|---|---|---|
| miniF2F-test Pass\@K | 50.0 % | 54.5 % | 63.5 % |
| ProofNet-test Pass\@K | 21.0 % | 18.1 % | 25.3 % |
| Lean 호출(동일 K) | 1.0 × | 64 × | 1.0 × |
| Whole-proof 샘플 | 16 ×4 096 | — | 1 ×3 200 |
표는 Table 1·2 및 저자 비교 서술에서 발췌·정리.
4. 한 줄 평
“우리는 ‘중간 상태 피드백을 먹는 whole-proof’라는 제3의 길을 제시했고, 그 결과 더 빨리·더 많이 증명해냈다.”
이처럼 저자들은 하이브리드 설계 + 본질적 탐색 보상 + 온라인 RL의 삼위일체가 기존 방법의 구조적 한계를 깔끔히 해결했다고 강하게 주장한다.
프롬프트 1.3.1 (알고리즘 단계별 설명)
"핵심 알고리즘, 모델 아키텍처, 또는 주요 방법론을 단계별(step-by-step)로 설명해 줘. 독자는 AI 분야의 대학원생 수준이라고 가정해. 특히, 간단한 문장, 3x3 픽셀 이미지, 작은 상태 공간(state space) 등 아주 간단하고 구체적인 예시(toy example)와 샘플 입력을 만들어서, 이 예시를 통해 각 단계를 거치며 입력이 최종 출력으로 어떻게 변환되는지 전체 과정을 보여줘. 등장하는 모든 핵심 용어와 변수는 그 즉시 정의해 줘."
TL;DR — 한눈에 보는 파이프라인
입력 정리 → (0) Whole-proof 초안 → Lean 에러 → (1) truncate-and-resume → (2) RMaxTS 선택·확장·시뮬레이션 → (3) Lean 검증 보상 → (4) DUCB 역전파 → (5) K 회 반복 후 최종 증명. 핵심은 “중간 tactic state를 끊어 주석으로 넘겨 whole-proof를 이어 쓰고, 내재 보상 MCTS(RMaxTS) 로 탐색 효율을 극대화한다”는 점이다.
1. 핵심 용어·변수 (요약표)
| 기호 | 의미 | 최초 등장 섹션 |
|---|---|---|
| s | 트리 노드 = (partial Lean proof, tactic state) | §3.2 Algorithm |
| a | tactic 코드 한 줄(모델이 생성) | §3.2 |
| N(s,a) | (s,a) 방문 횟수 | Eq.(6) |
| W(s,a) | 누적 보상 합 | Eq.(5) |
| 𝑅_extrinsic | Lean 검증 성공 = 1 / 실패 = 0 | Fig. 2 |
| 𝑅_intrinsic | 새 tactic state 생성 시 1, 아니면 0 | Eq.(3) |
| DUCB | Discounted UCB 선택 점수 | Eq.(7) |
모두 논문( turn6file6 , turn6file7 , turn6file15 )에서 인용.
2. 장난감 예시 — 3 줄짜리 Lean 증명
-- 목표: tiny_thm : 0 + n = n
import Mathlib.Data.Nat.Basic
theorem tiny_thm (n : ℕ) : 0 + n = n := by
simp? -- (❌ Lean 에러: tactic 'simp?' not found)
상태 공간 축소
- state s₀ = 코드 4 줄 전체 + Lean goal
⊢ 0 + n = n - 액션 후보 {
simp,rw [Nat.zero_add], …} 3 개 → 트리 branching ≤ 3.
아래 단계에서 이 예시가 어떻게 흘러가는지 추적한다.
3. 단계별 알고리즘 흐름
| 단계 | 처리 내용 | toy 예시에서의 변화 |
|---|---|---|
| 0. Whole-proof 초안 | 7 B LLM이 s₀에 대해 단일 패스 완성 시도 | 위 코드 그대로 출력 → Lean 실패 |
| 1. Truncate-and-Resume | 실패한 줄까지만 남기고 -- STATE: … 주석으로 tactic state 삽입, 재프롬프트 |
lean … by\n simp? -- STATE: ⊢ 0 + n = n |
| 2. 선택(Selection) | 현재 노드 s₀의 액션 a 중 DUCB(s,a) 최대인 것 선택 | 초기엔 방문 0 → 임의로 simp 선택 |
| 3. 확장(Expansion) | LLM이 simp 한 줄 생성 → Lean 검증 → 새 tactic state 얻으면 새로운 노드 s₁ 생성, 𝑅_intrinsic = 1 |
Lean이 성공적으로 simp 수행 → 새 goal ⊢ n = n, 노드 추가 |
| 4. 시뮬레이션 / 증명 완성 | (옵션) 남은 예산으로 roll-out; 완성되면 𝑅_extrinsic = 1 | LLM이 바로 rfl 생성, Lean 성공 |
| 5. 역전파(Back-prop) | (s,a) ∈ trajectory마다 W, N 갱신 후 𝑄_DUCB 재계산 | (s₀,simp), (s₁,rfl) 모두 𝑅 = 1 |
| 6. 반복 | 예산 K(예: 6400)까지 단계 2‒5 반복 → 최종 최고 scoring 경로 반환 | 단 2 스텝 만에 증명 완료 |
이 toy 예시는 노드 2 개로 끝나지만, 실제 miniF2F 난제는 평균 노드 수 천 개에 달한다. RMaxTS의 내재 보상 + DUCB 덕분에 64× 적은 샘플로도 탐색이 수렴한다 .
4. 왜 잘 작동하나? (직관)
- 끊고 이어 쓰기 → whole-proof의 단순성은 유지하면서도, 실제 Lean tactic state를 LLM에 피드백하여 누적 오차를 꺾어 버린다.
- RMaxTS → “새 상태일 때만 1점”이라는 보상 덕에 트리 폭을 넓히는 방향으로 유도, sparse-reward 문제 완화.
- Discounted UCB → intrinsic reward가 시간이 갈수록 희소해지는 비정상(non-stationary) 상황에 맞춤형으로 값 전파를 가속한다.
5. 마무리 — 한 문장 요약
“Lean tactic state 주석으로 ‘끊어 쓰는’ whole-proof와, 새 노드에만 점수 주는 RMaxTS 탐색이 합쳐져, 7 B 모델로도 miniF2F 63.5 %의 새 SOTA를 거뜬히 달성한다.”
프롬프트 1.3.2 (‘비밀 병기’ 식별)
"이 논문의 핵심 기여를 가능하게 하는 가장 결정적인 단일 수학 공식, 알고리즘 단계, 또는 아키텍처 구성요소를 식별해 줘. 그것의 기능과, 그것이 이 방법론의 성공에 왜 필수적인지 설명해 줘."
결론 먼저 (Secret Weapon TL;DR)
할 일 리스트는 하나—
Q_{DUCB}만 잘 써라. 이 논문의 승부수는 내재 보상 RMaxTS 탐색에서Discounted UCB (Eq. 7)를 선택 점수로 채택한 것이다. γ-가중 누적값으로 최근 보상을 더 크게 반영해 희소·비정상(intrinsic) 보상을 즉시 전파하며, 이를 뺀 모든 변형(UCT·UCB1)보다 miniF2F-test가 최대 ▲2.4 pp 낮게 나온다.
1. ‘비밀 병기’ 공식
Q_{\text{DUCB}}(s,a)=
\underbrace{\frac{W_\gamma(s,a)}{N_\gamma(s,a)}}_{\text{가치 추정}}
\;+\;
\underbrace{\sqrt{\frac{2\ln\!\bigl(\sum_{a'} N_\gamma(s,a')\bigr)}
{N_\gamma(s,a)}}}_{\text{탐색 보너스}}
\tag{7}
- $s$: (partial proof, tactic state) 노드
- $a$: 다음 tactic 코드
- $\gamma$: 할인因子(논문 0.99)
- $W_\gamma,N_\gamma$: 과거 $t$-번째 방문 보상을 $\gamma^{,\Delta t}$ 으로 감쇠한 가중 합
즉, 최근에 새 상태를 만들며 받은 보상은 크게, 오래된 보상은 작게 본다.
2. 왜 필수적인가? — 3-단 논리
| 단계 | 논리·효과 | 증거 |
|---|---|---|
| A. 보상 신호는 ‘새 노드 생성’(1/0)뿐 → 비정상 | 탐색이 진행될수록 새 노드 발견 확률 ↓ → 기대보상 감소 | 논문 §3.3 설명 |
| B. 표준 UCB1는 과거 보상을 등가 취급 | 오래된 “한때 새로웠던” 보상이 과대평가 → 트리 분기 선택이 왜곡 | Ablation: UCB1으로 교체 시 성능이 UCT 수준으로 급락 |
| C. DUCB는 γ-감쇠로 ‘현재형 보상’만 강조 | 보상값·카운트를 동시에 discount → 값 전파 빠름, 최신 노드 우선 | Figure 5: RMaxTS-DUCB가 동일 샘플 6 400개에서 +1.4 ~ +2.4 pp 우세 |
결국 증명 성공률을 올리는 유일한 레버가 이 식이라는 점을 Ablation이 직설적으로 보여 준다.
3. 직관적 작동 메커니즘 (한 줄 요약)
“새 tactic state를 발견한 직후의 ‘신선한’ 보상만 크게 본다 → 트리가 넓고 얕게 퍼지며 Lean 호출 대비 성공률이 극대화된다.”
덕분에 DeepSeek-Prover-V1.5는 64 × 적은 탐색 예산으로도 step-wise 프로버보다 높은 63.5 % SOTA를 달성했다.
참고: 관련 변수 정의
| 기호 | 정의 |
|---|---|
| $R_{\text{intrinsic}}=1$ | 새 노드 추가 시 보상 Eq.(3) |
| $W_\gamma(s,a)$ | 최근 보상일수록 가중치 ↑ (Eq. 8) |
| $N_\gamma(s,a)$ | 할인 방문 횟수 (Eq. 9) |
4. 한 문장 평
DUCB는 “희소·비정상 보상”이라는 정형증명 탐색의 고질병을 한 식으로 눌러 버린, DeepSeek-Prover-V1.5의 결정적 한 방이다.
프롬프트 1.4.1 (핵심 결과 분석)
"'Experiments' 또는 'Results' 섹션의 표와 그림을 포함한 주요 결과를 분석해 줘. 사용된 핵심 성능 지표(performance metrics)는 무엇인가? 어떤 벤치마크 데이터셋에서 결과가 보고되었는가? 저자들이 자신들의 방법론의 성공 증거로 가장 강조하는 주요 결과를 요약해 줘."
결론 먼저 (TL;DR)
- miniF2F-test 63.5 %, ProofNet 25.3 % — DeepSeek-Prover-V1.5 (RL + RMaxTS) ↗ 기존 최고(InternLM2-StepProver 54.5 % / 18.1 %) 대비 +9.0 pp / +7.2 pp
- 같은 54 %대 성능을 내려면 우리 모델 3 200 샘플이면 충분하지만, 이전 SOTA는 64 × 3 200 탐색이 필요 → 샘플 효율 64 ×
- 비밀 병기 Discounted-UCB + Intrinsic Reward가 없으면 성능이 ▲2 pp 이상 급락하여 tree-search 효과가 사라짐
1. 핵심 성능 지표
| 지표 | 정의 | 왜 사용? |
|---|---|---|
| pass\@K | K 번의 증명 시도 중 하나라도 Lean 검증에 통과하면 1, 아니면 0 → 정확도 평균 | 비일관적 길이·탐색예산을 공통 잣대로 비교하기 위해 |
논문은 single-pass, best-first, tree-search 각 방식의 K 계산법을 명시해 공정성을 확보한다.
2. 사용된 벤치마크 데이터셋
| 데이터셋 | 난이도 | 규모 | 설명 |
|---|---|---|---|
| miniF2F-test | 고교 수준 | 488문제 | Lean 4 공식 고등학교 수학 벤치마크 |
| ProofNet | 학부 수준 | 5 018문제 | Lean 4 대수·해석 등 광범위 전공 수학 |
3. SOTA 비교 — 숫자로 한눈에
| 방법 | 패러다임 | 샘플 예산 (K) | miniF2F-test | ProofNet-test |
|---|---|---|---|---|
| DeepSeek-Prover-V1 (이전) | whole | 16 × 4 096 | 50.0 % | 21.0 % |
| InternLM2-StepProver | step + tree | 64 × 32 × 100 | 54.5 % | 18.1 % |
| V1.5-RL (single-pass) | whole | 16 × 6 400 | 60.2 % | 22.6 % |
| V1.5-RL + RMaxTS | hybrid tree | 32 × 6 400 | 63.5 % | 25.3 % |
모든 수치는 Table 1·2에서 발췌
4. 저자들이 강조한 성공 증거
-
절대 성능 우위
- 63.5 %는 7 B 계열 모델 중 최초로 60 %+ 벽 돌파, 이전 기록 대비 9 pp↑.
-
샘플-효율적 SOTA
- 54.9 % 달성에 3 200 샘플 → 동일 성능의 InternLM2는 64 배 더 많은 모델 × Lean 호출 필요.
-
RMaxTS의 필수성 (Ablation)
- Discounted-UCB + Intrinsic Reward 둘 중 하나라도 제거 시 16 × 6 400 샘플에서 **≃ 61 %**로 하락; tree-search 이점 거의 소멸.
-
훈련 단계별 기여
- SFT → RL 전환만으로도 단일-패스 성능이 +3.7 pp(56.5→60.2) 상승, tree-search와 직교적으로 합산됨.
5. 요약 — 왜 이 결과가 중요한가?
**“하이브리드 탐색 + 맞춤 보상 설계”**로 정확도·연산비용 두 마리 토끼를 동시에 잡았다. 숫자가 말한다: +9 pp 정확도 상승과 ×64 샘플 절감. 이는 7 B LLM으로 Lean 4 정형증명에서 첫 60 %대 SOTA를 달성하며, 프루버 설계의 새로운 효율 프런티어를 제시한다.
프롬프트 1.4.2 (비판적 비교)
"제안된 방법론은 논문에서 언급된 주요 베이스라인 및 SOTA(State-of-the-Art) 모델들과 비교하여 어떤 성능을 보이는가? 저자들의 우월성 주장을 가장 강력하게 뒷받침하는 특정 결과나 비교 지점을 식별해 줘. 반대로, 제안된 방법론이 경쟁 모델을 능가하지 못했거나 개선 효과가 미미했던 결과는 없는지 찾아봐. 만약 있다면, 저자들은 이러한 경우에 대해 어떤 이유를 제시하는가?"
📝 한 줄 결론
DeepSeek-Prover-V1.5 (+ RMaxTS) 는 miniF2F 63.5 % / ProofNet 25.3 %로 기존 최고치보다 각각 +9.0 pp · +7.2 pp 우수하며, 같은 55 %대 정확도를 얻는 데 필요한 샘플 수는 InternLM2-StepProver의 1/64에 불과하다.
1. 숫자로 보는 성능 비교
| 방법 (7 B 계열) | 탐색 방식 | 샘플 예산 $K$ | miniF2F-test | ProofNet-test | 강점/약점 포인트 |
|---|---|---|---|---|---|
| V1.5-RL + RMaxTS | Hybrid MCTS | 32 × 6400 | 63.5 % | 25.3 % | 새 SOTA 📈 |
| InternLM2-StepProver | Step BFS | 64 × 32 × 100 | 54.5 % | 18.1 % | 샘플 폭증(×64) |
| V1.5-RL (single-pass) | Whole | 16 × 6400 | 60.2 % | 22.6 % | 탐색 없이도 SOTA 근접 |
| DeepSeek-Prover-V1 | Whole | 16 × 4096 | 50.0 % | 21.0 % | 이전 자사 모델 |
| ReProver | Step | – | – | 13.8 % | ProofNet 열세 |
샘플 효율: V1.5-RL은 *54.9 %*를 3200회 샘플로 달성, StepProver가 같은 성능을 내려면 64 × 3200 탐색이 필요.
2. 저자 주장 — ‘왜 우리 방법이 우위인가?’
- 하이브리드 탐색 truncate-and-resume whole-proof + RMaxTS 덕분에 누적 오차와 트리 비용을 동시에 완화해 정확도↑·Lean 호출↓.
- 샘플-효율 SOTA 동일 정확도 대비 계산량을 최대 64 × 절감.
-
RMaxTS 핵심 구성요소 검증
- 내재 보상·Discounted-UCB 중 하나라도 빼면 성능이 2 pp 이상 하락해 탐색 효과 상실.
3. ‘가장 강력한’ 증거 지점
- miniF2F 63.5 % — 7 B 범주 최초 60 % 돌파. SFT나 RL 없이도 60 %대에 안착해 step 계열 대비 +9 pp 격차.
- 3200 샘플 vs 204 800 — 같은 55 % 근방 성능에서 샘플 효율 64 × 개선으로 계산/시간 비용이 급감.
4. 못 이기거나 미미했던 부분 & 저자 해석
| 관찰 | 상세 수치 | 저자 설명 or 추정 |
|---|---|---|
| 저샘플(≤128) 구간 이득 ↓ | 128 샘플에서 V1.5-RL 51.6 % vs SFT 50.4 % → +1.2 pp 뿐 | RL 보상(Lean 피드백)이 누적되기엔 탐색·샘플 수가 부족 |
| ProofNet SFT↔RL 차이 작음 | 22.6 %(RL) - 21.9 %(SFT) = +0.7 pp | “학부 수준 문제는 짧아 compounding-error가 덜해 RL 이득 제한” (암시적) |
| 탐색 없이는 여전히 60 % 미만 | single-pass 60.2 % → 트리 병합 뒤 63.5 % | 희소 보상 극복용 RMaxTS 없으면 성능 상한 존재 |
| 장기 맥락·파일 단위 증명은 미해결 | 한 파일 다중 정리에선 평가 안 됨 | critic 모델 등 exploitation 연구 과제로 제시 |
5. 요약 & 시사점
DeepSeek-Prover-V1.5는 **“적게 돌리고 더 맞힌다”**라는 명확한 우위(정확도 + 샘플 효율)를 실측 데이터로 입증했다. 다만 샘플이 매우 적은 상황·ProofNet 같이 짧은 증명에서는 향상이 제한적이며, 파일-레벨 대증명·critic 도입 등 exploitation 측면은 여전히 열려 있다.
연구·산업 적용 시 ➜ RMaxTS 탑재 + 충분한 샘플 예산이 있을 때 최대 효과. 샘플 예산이 극도로 제한된 환경이라면 SFT 모델만으로도 비용-성능 균형을 다시 따져볼 필요가 있다.
프롬프트 1.5.1 (언급된 한계와 잠재적 한계)
"저자들이 논문에서 명시적으로 인정한 한계점, 약점, 또는 실패 사례(failure modes)는 무엇인가? 다음으로, 방법론과 결과에 대한 당신의 분석을 바탕으로, 저자들이 언급하지 않았을 수 있는 잠재적인 한계나 약점은 무엇이라고 생각하는가? (예: 강력한 가정에 대한 의존성, 확장성 문제, 높은 연산 비용, 일반화의 한계, 잠재적인 부정적 사회 영향 등)"
결론 먼저 (TL;DR)
저자 인정 한계는 (i) 탐색-후-활용(exploitation) 미흡, (ii) 파일(Level)-단위 맥락 부족, (iii) Lean tactic-state 의존성 등 세 가지다. 추가로 보이는 잠재 한계는 높은 계산‧메모리 비용, 보상 설계의 민감성, 데이터·벤치마크 편향, 타 Proof Assistant 일반화 미확인, 잠재적 사회적 영향 등이다. 아래 표에 상세·근거를 정리했다.
1. 저자가 명시적으로 인정한 한계
| # | 한계(저자 서술) | 근거 문구·구간 | 영향 |
|---|---|---|---|
| A1. ‘Exploitation(평가·가지치기)’ 부재 | “…the exploitation aspect, specifically the problem of proof search, remains unexplored. A promising future direction is training a critic model to assess incomplete proofs and prune search branches.” | 트리 폭은 넓히지만 불필요한 분기를 제거 못 해 탐색 비용 ↑ | |
| A2. 파일-단위(다중 정리) 증명 미지원 | “…recent work has progressed beyond proving individual theorems to addressing real-world theory proving within complex, multi-theorem Lean files… Moving forward, we will focus on enhancing this aspect.” | 실제 Lean 프로젝트(예: Mathlib) 적용 시 컨텍스트 길이 한계 | |
| A3. Lean tactic state 의존 | RMaxTS-without-state 실험에서 성능이 **62.7 → 61.1 %(-1.6 pp)**로 하락, “compiler information is an essential component of the tree search algorithm” | 다른 Proof Assistant(Isabelle, Coq)로 이식 시 재설계 필요 |
2. 저자가 언급하지 않은 잠재적 한계 (비판적 분석)
| 잠재 한계 | 구체 설명 / 왜 문제인가? | 정량·정성 근거 |
|---|---|---|
| P1. 계산·메모리 비용 여전히 高 | 7 B 모델이라도 32 × 6 400 샘플 → Lean 검증 수십 만 회. A100-40G 1대 기준 Pass\@63.5 %에 ≈6.5 GPU·시 / 문제 추정 → 대규모 배치·온라인 시스템엔 부담 | 샘플·GPU 설정 표/Table 3 |
| P2. 보상 설계 민감성 | DUCB·intrinsic reward 파라미터(γ = 0.99, R=1/0) 변경 시 성능 급락(▲2 pp) → 하이퍼 튜닝 비용 | Ablation에서 DUCB→UCB1 시 62.7 → 60.7 % |
| P3. 벤치마크 편향·일반화 불확실 | 학습·평가 모두 Lean-3→4 변환된 miniF2F, ProofNet에 집중 → 새 정리·대수기하 등 미리 보기 어려운 영역에서 과적합 위험 | 벤치마크 범위 정의 |
| P4. 모델 크기 한계 | 7 B로 60 %대는 뛰어나지만, 미증명 36 %(miniF2F)·75 %(ProofNet) 남음 → 매스 스케일-업 시 파라미터·메모리 병목 | 최고 성능 63.5 %, 25.3 % 표 |
| P5. 사회적 영향 평가 부재 | 대규모 자동 증명은 암호·스마트컨트랙트 검증을 가속하는 반면, 악의적 증명 위조·특허 남용 등 위험도 증가 → 책임 있는 공개·감사 체계 필요 | 논문에서 관련 논의 부재(직접 인용 없음) |
3. 정리
DeepSeek-Prover-V1.5는 “탐색(Exploration) 혁신”으로 SOTA를 경신했지만, “활용(Exploitation)·확장(Scalability)·일반화(Generality)” 세 축에서 여전히 과제가 남아 있다. 생산 환경 적용 시 연산 자원과 도메인 전이 비용을 충분히 감안해야 하며, 연구 측면에선 critic 모델·파일-레벨 컨텍스트·다른 Proof Assistant로의 확장이 핵심 후속 과제다.
프롬프트 1.5.2 (미래 연구 궤적)
"저자들이 제안하는 구체적인 향후 연구 방향은 무엇인가? 이 논문의 한계점을 바탕으로, 이 연구를 발전시키거나 약점을 극복하기 위해 추구할 수 있는 다른 논리적인 다음 단계나 대안적인 연구 방향은 무엇이 있을까?"
결론 먼저 (TL;DR)
저자 제시: (1) partial-proof critic 도입으로 탐색 이후의 ‘가지치기(Exploitation)’ 문제 해결, (2) 파일(다중 정리) 레벨 증명 지원 강화를 두 축으로 제안한다. 추가 아이디어: critic을 가치 함수로 확장·MoE 스케일업·다른 Proof Assistant 전이·계산비용 절감 등 여섯 가지 논리적 다음 단계를 제안한다.
1. 저자가 명시적으로 제안한 향후 연구 방향
| 구분 | 제안 내용 | 기대 효과 | 근거 |
|---|---|---|---|
| F-A1 Exploitation Critic | “train a critic model to assess incomplete proofs and prune search branches” | ✔ 탐색 폭 줄여 Lean 호출 ↓ ✔ 보상 분해‧값 전파 → RL 샘플 효율 ↑ |
|
| F-A2 File-level Context | 복잡한 multi-theorem Lean files까지 처리 ↗ | ✔ 실제 Mathlib 프로젝트 적용성 ↑ |
2. 추가로 고려할 만한 연구 궤적 (필자 제안)
| ID | 방향 | 구체 아이디어 | 왜 필요한가 |
|---|---|---|---|
| N-B1 Critic+Actor 공동학습 | Tree node 가치 $V(s)$ 예측 critic ↔ LLM actor 공동 GRPO | DUCB가 방문수 기반이라 깊은 트리선 한계; $V$로 미리 가지치기 | |
| N-B2 MoE 스케일 & Distill | 7 B → 30 B MoE로 탐색 깊이 ↗, 완성 모델은 LoRA distill | 파라미터 ↑ 시 miniF2F 잔여 36 % 공략, 단 추론 비용 억제 | |
| N-B3 Cross-PA Generalization | Lean → Isabelle/Coq로 tactic-state adapter 교체 | Lean 특화 의존성(P1) 완화, 생태계 확장 | |
| N-B4 Proof-Sketch Pre-planner | LLM이 먼저 natural-lang outline 생성 → proof fill-in | Whole-proof 오차를 사전 구조화로 감쇠 | |
| N-B5 Hardware-Aware Batch Search | KV 공유 prefix 가속(예: Hydragen 기법)과 RMaxTS 결합 | 대규모 탐색 시 GPU 메모리·FLOPS 절감 | |
| N-B6 사회·안전 연구 | 자동 증명의 오·남용 탐지·감사 파이프라인 설계 | 악의적 증명 위조·특허 분쟁 등 잠재 리스크 대응 |
3. 정리
DeepSeek-Prover-V1.5는 탐색(Exploration) 혁신으로 새 SOTA를 세웠다. 다음 목표는
- critic 도입으로 Exploitation 효율 극대화,
- 파일·도메인·스케일 확장으로 현실 적용성을 높이는 것이다. 위 표의 B-series 제안은 이 두 축을 구체화하여 성능·자원·범용성 세 마리 토끼를 잡기 위한 실질적 로드맵이 될 수 있다.
모델 아키텍처/알고리즘
"상태 공간(State Space), 행동 공간(Action Space), 보상 함수(Reward Function)를 정의해 줘. 모델은 온-폴리시(on-policy)인가 오프-폴리시(off-policy)인가? 가치 기반(예: DQN), 정책 기반(예: REINFORCE), 또는 액터-크리틱(예: A2C, PPO) 중 어느 유형인가? 정책 및/또는 가치 함수에 대한 핵심 업데이트 규칙을 설명해 줘."
한눈에 요약 — DeepSeek-Prover V1.5의 RL 정의
| 구성요소 | 정의 | 핵심 수치/식 |
|---|---|---|
| 상태 공간 S | ⟨ theorem statement, 현재까지 생성한 Lean proof 토큰들, (선택) 최신 tactic state ⟩토큰 길이 ≤ 2 048(훈련) / 4 096(추론) |
Lean tactic state를 주석으로 삽입하여 모델이 “컴파일러 피드백”을 안에 보관 |
| 행동 공간 A | LLM 토큰 단위(≈ 32 K vocab) — 즉 다음 토큰을 확률적으로 출력. Tree-search 단계(RMaxTS)에서는 “다음 tactic 한 줄”이 실질적 action |
후보 32 개/정리(훈련)·6400 개/샘플(추론) |
| 보상 함수 R | Extrinsic R=1 (Lean 검증 성공) / 0 (실패) Intrinsic (RMaxTS) R_int=1 |
새 tactic-state 노드 최초 방문, else 0 (식 3) |
| 알고리즘 | GRPO (Group-Relative Policy Optimization) — 32 개의 proof 샘플을 동일 정책에서 뽑아 상대 보상 기반으로 갱신 | |
| On/Off-policy? | On-policy (샘플은 현행 π θ 로부터 즉시 수집) | |
| 유형 | 정책-기반 (REINFORCE 계열). Critic을 없애 PPO 대신 “relative weights” 사용 → Actor-Critic 아님. | |
| 정책 업데이트 | <div>\[ | |
| L(θ)=\sum_{i=1}^{32} w_i;\log π_θ(y_i\mid x) ;-;β\,\mathrm{KL}[π_θ;|;π_{SFT}] | ||
| \] </div> 여기서 • w_i = (r_i - \overline r)/σ_r (그룹 내 z-score) • β = 0.02 (KL penalty) |
||
| 가치 업데이트(RMaxTS) | <div>\[ | |
| Q_{DUCB}(s,a)=\frac{W_γ(s,a)}{N_γ(s,a)} + \sqrt{\frac{2\ln!\sum_{a’}N_γ(s,a’)}{N_γ(s,a)}};,\ γ=0.99 | ||
| \] </div> |
자세한 설명
-
상태 S
- 모델은 정리 문장과 지금까지 작성한 증명 코드를 토큰 시퀀스로 본다.
- 증명 중 Lean 4 REPL이 반환한 tactic state를
/- tactic state: … -/형태로 주석 삽입해 관찰‧학습 신호로 활용 . - 이렇게 하면 환경(Lean 컴파일러)의 내부 상태까지 텍스트로 노출되어 (i) Supervised FT 의 부가 목표, (ii) RL과 tree-search 양쪽에서 모두 사용된다.
-
행동 A
- RL 학습 단계에서는 “다음 토큰”을 예측해 전체 증명 시퀀스를 완성한다(episode = 한 proof).
- RMaxTS 추론 단계에선 truncate-and-resume 메커니즘으로 증명을 잘라 tactic 단위 노드를 탐색 .
-
보상 R
- Extrinsic : Lean 4가 ‘QED’를 반환하면 1, 아니면 0. 보상 희소성을 줄이기 위해 “SFT에서 50 % 내외 성공” 정리만 4.5 k 개 선별 .
- Intrinsic (RMaxTS) : 새 tactic-state를 처음 확장할 때 1 부여(식 3) → 탐험-보장 .
-
알고리즘 특성
-
GRPO ≈ PPO–critic + relative weights
- 32 개 샘플에서
w_i를 z-score로 정규화 → 높은 보상을 받은 샘플에 강한 gradient. - KL penalty(0.02)로 학습 안정성 유지 .
- 32 개 샘플에서
-
On-policy, 정책-기반 : critic 없이 직접 policy log-prob을 최적화 → 메모리· compute 효율 ↑ .
-
-
Tree-Search 업데이트
- MCTS 노드는 DUCB(γ=0.99)로 선택값을 계산해 non-stationary intrinsic reward를 빠르게 전파 .
- back-prop 시 최근 rollout 보상으로
W_γ, N_γ누적치를 갱신한다.
이 정의만 기억해 두면, DeepSeek-Prover V1.5의 RL 훈련·추론 로직을 다른 증명 환경이나 LLM에도 손쉽게 이식할 수 있습니다.
학습 및 최적화
"탐험(exploration)과 활용(exploitation)의 트레이드오프는 어떻게 관리되는가(예: epsilon-greedy, entropy regularization)? 리플레이 버퍼(replay buffer)가 사용되었는가? 학습에 사용된 시뮬레이션 환경이나 실제 환경 설정을 설명해 줘."
결론 요약 (1-줄)
새 노드를 발견하면
R=1(탐험)·최근 보상만 강조하는DUCB(γ = 0.99)로 분기 선택(탐험/활용 균형) → 온-폴리시 GRPO 정책-기반 학습이며, 리플레이 버퍼는 없고 Lean 4 프로버 자체가 RL 환경이다.
1. 핵심 정의
| 항목 | 구체 내용 | 근거 |
|---|---|---|
| State S | ⟨정리 문장, 현재까지 작성한 Lean 코드, 최근 tactic state 주석⟩ | Lean state 삽입 설명 |
| Action A | LLM이 출력하는 다음 토큰 (트리 탐색 단계에서는 “다음 tactic 한 줄”) | |
| Reward R | Extrinsic: Lean 검증 성공 1 / 실패 0 Intrinsic: 새 tactic-state 노드 생성 시 1, 아니면 0 (RMaxTS) |
Eq.(3) |
| Policy πθ | 7 B Llama 기반 LLM, GRPO로 온라인 업데이트 |
2. 탐험 vs 활용 제어
| 메커니즘 | 역할 | 수식·세부 | ||
|---|---|---|---|---|
Intrinsic reward (R_int) |
새로운 상태 공간을 넓게 탐색 (탐험) | R_int=1 if new node |
||
Discounted-UCB (Q_DUCB) |
최근 보상을 크게 반영해 탐험 보너스 조절 (탐험↔활용 균형) | DUCB 식 (7) with γ=0.99 | ||
| GRPO KL penalty (β = 0.02) | 정책 폭발 방지·활용 촉진 | 학습 세팅 | ||
샘플 그룹 정규화 (w_i z-score) |
동일 배치(32개) 내 상대 성과에 따라 gradient 가중 | GRPO 설명 |
별도 ε-greedy·entropy reg는 사용하지 않으며, DUCB + KL 조합이 탐험/활용 트레이드오프의 핵심이다.
3. 학습 패러다임 요약
| 구분 | 설명 | |
|---|---|---|
| On-/Off-policy | 온-폴리시 — 매 스텝 현행 πθ로 32 개 proof를 새로 roll-out | |
| 알고리즘 유형 | 정책-기반 (REINFORCE 계열) · critic 없이 GRPO로 업데이트 | |
| 핵심 업데이트 | <div>\(L(θ)=\sum_i w_i \log π_θ(y_i | x) - β,\text{KL}[π_θ‖π_\text{SFT}]\)</div> where w_i는 그룹 z-score |
| Replay buffer | 사용하지 않음 — on-policy & sparse reward 구조상 즉시 폐기 |
4. 환경 및 실행 설정
| 항목 | 세부 사항 | 근거 |
|---|---|---|
| 환경 | Lean 4 프로버 + Mathlib4/Aesop; 각 증명 시도 후 Lean이 성공/실패 반환 → 보상 신호 | |
| 하드웨어 | A100-40G GPU 1장; vLLM으로 샘플링, 증명 길이 ≤ 2 048 토큰, Lean 검증 제한 300 s | |
| RL 배치 | 32 샘플 × 16 그룹 ⇒ batch 512, lr 5e-6 |
🔑 이해 포인트
- 탐험은 _새로운 tactic state_에 즉시 1점을 주는 RMaxTS와 γ-감쇠 UCB로 달성.
- 활용은 DUCB의 평균 가치 항(term 1) + GRPO의 KL 규제로 자연스럽게 확보.
- On-policy이므로 리플레이 버퍼는 불필요하며 Lean 4가 곧 시뮬레이션 환경 역할을 한다.
평가 및 지표
"성능은 어떻게 측정되는가(예: 누적 보상, 에피소드 길이, 성공률)? 평가에 얼마나 많은 에피소드나 타임스텝이 사용되었는가? 시간에 따른 성능을 보여주는 학습 곡선(learning curves)이 있는가?"
결론 한 줄 — 정확도는 pass@K (성공률)로, 에피소드는 “문제 수=244 + 186”, 학습‧탐색 스텝은 샘플 예산 K로 표시하며, 논문 Figure 3·5에 pass@K vs. K 학습 곡선이 존재한다.
1. 측정 지표 (Metrics)
| 지표 | 정의 | 쓰인 이유·특징 |
|---|---|---|
| pass\@K | K 회 생성 중 Lean 검증을 1 번이라도 통과하면 1, 아니면 0 → 평균 | 증명은 “성공/실패”만 있으므로 누적 보상·길이보다 성공률이 직관적 |
| K 산정 규칙 | Single-pass = 생성 Proof 수 Best-first = N × S × T Tree-search = N × T |
서로 다른 탐색 방식의 연산량을 맞추기 위해 통일 규칙 제시 |
| 추가 통계 | 평균 ± 표준편차(표·그래프) | 3회 반복 후 $\mu!\pm!\sigma$ 표기 |
2. 평가 프로토콜
| 항목 | miniF2F-test | ProofNet-test | 근거 |
|---|---|---|---|
| 에피소드 수 | 244 문제 | 186 문제 | Lean 3→4 전환 버전 사용 |
| 한 에피소드 길이 | 증명 길이 (토큰) ≤ 2 048 (평가), Lean 타임아웃 300 s | 동일 | 샘플 파라미터·검증 제한 |
| K 값 (대표) | 32, 64, 128, 3 200, 4 × 6 400, 16 × 6 400, 32 × 6 400 | 128, 3 200, (16 ×) 6 400 등 | Table 1·2·3 전반 |
| 하드웨어 | A100-40G × 1, vLLM 샘플링 | 동일 | 설정 설명 |
Episode = 문제 하나이므로 총 430 에피소드(244+186)를 반복 없이 전량 평가한다.
3. 시간(샘플 예산) 대 성능 곡선
| 그림 | 내용 | 관찰 포인트 |
|---|---|---|
| Figure 3 | Pass\@K (K ≤ 128) — Base → SFT → RL 단계별 성능 곡선 | RL이 초기 작은 K 구간부터 SFT 대비 +1.2 pp↑ (miniF2F) |
| Figure 5 | RMaxTS 변형별 Pass\@K (K ≤ 6 400) 곡선 + 대용량 결과 | DUCB+Intrinsic 조합 없으면 최대 ▲2 pp 하락; tactic-state 제거도 성능↓ |
두 그래프 모두 X-축은 ‘샘플 예산 K’, Y-축은 pass\@K 정확도를 사용해 “탐색/샘플이 늘수록 성능이 얼마나 개선되는가”를 시각화한다.
4. 왜 다른 지표는 없는가?
- 누적 보상·에피소드 길이는 Lean 검증이 “성공 1 / 실패 0” 이므로 정보량이 적어 사용하지 않음.
- RL 학습 중 time-step reward 곡선은 제시되지 않았지만, Figure 3·5가 사실상 학습·탐색 효율을 대변한다.
5. 정리 한 줄
DeepSeek-Prover V1.5는 430 에피소드 전체를 pass\@K로 평가하고, Figure 3·5 학습 곡선으로 “샘플 예산 → 성능” 상관관계를 명확히 드러낸다—덕분에 정확도·샘플 효율을 동일 축에서 비교할 수 있다.