Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data

저자: Huajian Xin, Daya Guo, Zhihong Shao, Z. Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, Xiaodan Liang | 날짜: 2024 | DOI: 미공개 📄 PDF

⚠️ 이 페이지의 요약·평가·해설은 생성형 AI(Claude)가 자동 생성한 2차적 분석물입니다. 논문 원문의 저작권은 원저작자에게 있으며, 정확한 내용은 원문(위 DOI·arXiv 등 출처)을 확인하세요.

Essence

Figure 1

그림 1: 접근 방법의 개요. 비형식 수학 문제에서 형식적 증명 데이터를 생성하는 반복적 파이프라인

이 논문은 비형식적 수학 문제에서 자동으로 대규모 형식 증명 데이터(Lean 4)를 합성하는 방법을 제시하고, 이를 통해 미세조정된 LLM이 GPT-4를 능가하는 정리 증명 성능을 달성했다. 특히 800만 개의 정형화된 명제-증명 쌍을 생성하여 훈련 데이터 부족 문제를 해결했다.

Motivation

Achievement

  1. 데이터셋 규모: 869,659개의 비형식 수학 문제에서 800만 개의 고품질 형식 명제-증명 쌍 생성 (기존 자동형식화 연구의 수십~수백배 규모)
  2. 벤치마크 성능:
    • miniF2F-test: 64 샘플 기준 46.3% 전체 증명 정확도 (GPT-4: 23.0%, RL 방법: 41.0%)
    • miniF2F 누적: 52% 정확도
    • FIMO 벤치마크: 100 샘플로 4/148, 4096 샘플로 5/148 증명 성공 (GPT-4: 0/148)
  3. 반복 학습의 유효성: 애블레이션 실험으로 각 반복마다 miniF2F 해결 문제 수가 점진적으로 증가함을 입증

How

![Figure 1 참조]

4단계 반복 파이프라인:

  1. 자동형식화 (Autoformalization)
    • DeepSeekMath-Base 7B를 MMA 데이터셋(Lean 4 mathlib 기반)으로 미세조정
    • 구조화된 프롬프트를 통해 비형식 문제를 Lean 4 형식 명제로 변환
    • 웹 스크래핑으로 수집한 869,659개 고등학교~학부 수준 경시 문제 활용
  2. 품질 보증 (Quality Assurance)
    • 모델 스코링: 단순 명제 필터링으로 증명 난이도 높은 문제 선별
    • 가설 거부 전략 (Hypothesis Rejection): 비형식적으로 부정확한 명제 제거
    • 형식 검증자로 생성된 명제 유효성 검사
  3. 증명 생성 및 검증 (Statements Proving)
    • DS-Prover가 형식 명제의 증명 코드 생성
    • Lean 4 형식 검증자로 증명 정확성 자동 확인
    • 병렬 증명 최적화: 원래 명제와 부정 명제를 동시에 증명하여 탐색 공간 축소 (unprovable 명제는 부정 증명으로 빠르게 배제)
  4. 반복 훈련 (Iterative Fine-tuning)
    • 검증된 명제-증명 쌍으로 DS-Prover 재훈련
    • 모델 성능 향상 → 더 나은 형식화 및 증명 생성 → 고품질 데이터 증가
    • 성능 개선이 수렴할 때까지 반복

Originality

Limitation & Further Study

한계점:

후속 연구 방향:

Evaluation

Novelty: 4.5/5 Technical Soundness: 4/5 Significance: 4.5/5 Clarity: 4/5 Overall: 4.25/5

총평: 이 논문은 정형식 증명의 오래된 데이터 부족 문제를 대규모 자동 합성과 반복 검증을 통해 실용적으로 해결한 견고한 연구로, 특히 800만 규모 오픈소스 데이터셋의 공개는 자동정리증명 분야에 상당한 인프라 기여를 할 것으로 예상된다. 다만 정리 증명의 절대 성능은 여전히 제한적이며, 고급 수학으로의 확장 가능성 검증이 필요하다.

같이 보면 좋은 논문

Minif2f: a cross-system benchmark for formal olympiad-level mathematics
기반 연구대규모 형식 증명 데이터 합성의 방법론적 기초를 제공한다.
A survey on deep learning for theorem proving
기반 연구정리 증명을 위한 심층학습 기법을 유사하게 종합 조사하며 확장함
다른 접근정리 증명을 위한 다른 형식 데이터 합성 방법을 제시한다.
Lean-star: Learning to interleave thinking and proving
기반 연구형식 검증 방법론이 자동 증명 데이터 합성의 기초를 이룬다.
후속 연구형식 증명과 자연어 추론 결합의 이론적 기반을 제공
Mustard: Mastering uniform synthesis of theorem and proof data
기반 연구MUSTARD의 정리-증명 데이터 합성 방식을 확장한 후속 연구
Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness
기반 연구correctness를 넘어선 평가 척도를 확장하여 다루는 관련 연구이다.
OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving
기반 연구수학적 추론 모델을 다른 응용 도메인으로 확장하는 유사한 시도로 보임
P1-VL: Bridging Visual Perception and Scientific Reasoning in Physics Olympiads
기반 연구과학 문제 해결에 특화된 추론 모델 응용 사례로 관련됨
The Two-Hump Problem: Bridging the Difficulty Gap in Mathematical Reinforcement Learning
다른 접근수학 문제 난이도 분포를 다루는 다른 RL 접근 방식을 제시한다.
Mixture of Graders: Adaptive Strategy Routing for LLM-Based Mathematical Evaluation
후속 연구SPECTER2 유사도 0.93로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
Nemotron-Math: Efficient Long-Context Distillation of Mathematical Reasoning from Multi-Mode Supervision
후속 연구long-context distillation 기법의 이론적 기반을 제공한다.
On Compositional Learning Behaviours in Formal Mathematics
후속 연구SPECTER2 유사도 0.93로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
PWW-Bench: Probing Visual Mathematical Reasoning with Proofs Without Words
후속 연구SPECTER2 유사도 0.93로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
QEDBench: Quantifying the Alignment Gap in Automated Evaluation of University-Level Mathematical Proofs
후속 연구SPECTER2 유사도 0.92로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
Scaling Generative Verifiers For Natural Language Mathematical Proof Verification And Selection
후속 연구SPECTER2 유사도 0.94로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
SorryDB: Can AI Provers Complete Real-World Lean Theorems?
후속 연구SPECTER2 유사도 0.94로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
The Self-Verification Cliff: Generation Outpaces Self-Selection in Frontier LLMs, and It Widens With Capability
후속 연구SPECTER2 유사도 0.93로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
The Signal-Coverage Matrix: Stratifying Type and Semantic Errors in Statement Autoformalization
후속 연구SPECTER2 유사도 0.94로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
Token-Level Verification under Controlled Evaluation: Protocol Sensitivity Shapes Apparent Performance
후속 연구SPECTER2 유사도 0.92로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
When RL Suppresses Its Own Vocabulary: Recovering Reasoning Diversity in Puzzle-to-Math Transfer
후속 연구SPECTER2 유사도 0.93로 LLM Agent Reasoning Training와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
Achieving Gold-Medal-Level Olympiad Reasoning via Simple and Unified Scaling
후속 연구Lean 4 기반 증명 데이터를 확장하여 정리 증명 성능을 향상시킨다.
Awakening the Sleeping Agent: Lean-Specific Agentic Data Reactivates General Tool Use in Goedel Prover
후속 연구SPECTER2 유사도 0.93로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs
후속 연구SPECTER2 유사도 0.93로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
BrokenMath: A Benchmark for Sycophancy in Theorem Proving with LLMs
후속 연구SPECTER2 유사도 0.94로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
FactorLibrary: From Polynomials to Circuits via Recursive Subgoals
후속 연구SPECTER2 유사도 0.93로 LLM Agent Reasoning Training와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings
후속 연구SPECTER2 유사도 0.93로 LLM Agent Reasoning Training와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
Hard or Just Unreached? Diagnosing the Sampling Blind Spot in Math-Reasoning Difficulty Estimation
후속 연구SPECTER2 유사도 0.91로 Computational Molecular Design와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study
후속 연구SPECTER2 유사도 0.94로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
Learn Hard Problems During RL with Reference Guided Fine-tuning
후속 연구SPECTER2 유사도 0.94로 LLM Agent Reasoning Training와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
응용 사례자동정형화 기법을 실제 수학 문제에 적용한 사례이다.
LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics
후속 연구SPECTER2 유사도 0.94로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.
← 목록으로 돌아가기

🎧 Audio Overview

이 논문 리뷰를 팟캐스트형 오디오로 생성합니다. (Gemini · 키는 브라우저에만 저장 · 완성본은 이메일로도 전송)
▸ 고급: 구성 방향(대본 작성 지침) 직접 수정
속도 1.0x
⬇ MP3 다운로드