(논문 요약) DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data (paper)
핵심 내용
- 중등, 고등, 대학부 수학 문제를 Lean4 로 formalize
- Autoformalization: generate formal mathematical statements from informal math problems
- Model scoring and hypothesis rejection: drop overly simplistic statements (using a model) or meaningless statements (by proving False conclusion - if solved, it means hypothesis is False)
- Statement proving: 모델이 생성한 statement 는 False 인 것들이 있을수 있어, original statement 와 negation 에 대해서, DeepSeek-Prover 로 proof 를 생성하여, 풀리는 것을 데이터에 추가
- Autoformalization: generate formal mathematical statements from informal math problems
데이터
- 869,659 high-quality natural language math problems (web scraping 후, data cleaning)
- 최초 data 생성시, DeepSeekMath-Base 7B (120 billion math-related tokens 로 학습) 을 MMA dataset (LEAN4 mathlib 을 natural language 로 변환한 것) 에 train 한 모델 사용
실험 결과
- effect of iteration
- 데이터 사이즈에 따른 성능 차이