OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving

Motivation

• Known: 기존 LLM 기반 formal theorem prover들은 MiniF2F와 같은 Olympiad-level 벤치마크에서 whole-proof generation과 step-level proving 패러다임을 통해 인상적인 성과를 보였으며, expert iteration과 DPO 같은 기법들이 이러한 모델 학습에 널리 사용되어 왔다.
• Gap: Optimization은 convexity, optimality condition, 알고리즘 수렴성 분석 등 고유한 formalism에 의존하기 때문에 기존 Olympiad 중심 prover를 naive하게 domain transfer하면 심각한 distribution shift와 catastrophic forgetting이 발생하며, 이를 완화할 체계적인 방법과 평가 벤치마크가 부재했다.
• Why: Optimization은 머신러닝, operations research, 과학계산의 근간이 되는 분야임에도 불구하고 formal verification 도구의 지원이 부족했으며, Olympiad에서 undergraduate 전문 도메인으로의 효과적인 domain transfer 방법론은 formal theorem proving을 실용적 수학 전반으로 확장하는 데 중요한 선결 과제이다.
• Approach: 강력한 Olympiad-level prover를 시작점으로 하여, 대규모 optimization 특화 data curation(expert iteration 기반)과, perplexity-weighted 최적화 및 유효하지만 진전 없는 증명 단계(non-progressing tactic)에 페널티를 부여하는 preference learning objective를 결합한 continual training 파이프라인을 도입한다.

Achievement

Figure 4. Performance of OptProver across expert iteration (EI)

1. OptProver 모델 개발: Olympiad-level prover로부터 continual training을 통해 undergraduate optimization 도메인으로 강건하게 transfer된 모델을 구축했다.
2. OptBench 벤치마크 구축: Optlib 기반의 Lean 4 optimization 문제 400개로 구성된 새로운 벤치마크를 제시하여 엄밀한 평가를 가능하게 했다.
3. State-of-the-art 성능 달성: OptBench에서 Pass@1, Pass@32 기준 comparable size 모델 중 최고 성능(55% 이상 성공률)을 달성하면서도 ProofNet, MiniF2F 등 일반 Olympiad 벤치마크에서 catastrophic forgetting 없이 경쟁력 있는 성능을 유지했다.

How

Figure 2. Performance degradation of OptBench under naive SFT.

• Step-level proving을 tree-search 과정으로 형식화하고, expert iteration(EI)을 통해 검증된 state-tactic pair (s,a)로 구성된 Dsucc를 반복적으로 구축하여 negative log-likelihood 손실(LSFT)로 정책을 학습.
• Optimization-focused data curation과 self-play 기반 curation 메커니즘을 결합해 도메인 특화 학습 데이터를 확보.
• Preference-based learning(DPO 계열)에서 영감을 받아, verifier-driven, utility-aware preference optimization을 도입: base 모델과 target 모델 간 log-probability ratio를 이용한 perplexity-weighted DPO objective를 설계해, 유효하지만 진전 없는(correct-but-unhelpful) tactic을 명시적으로 penalize.
• naive SFT 대비 OptBench 및 일반 벤치마크(ProofNet, MiniF2F)에서의 성능 저하(catastrophic forgetting)를 실험적으로 분석(Figure 1, 2)하고, EI 반복에 따른 성능 변화를 추적(Figure 4).

Originality

• Formal theorem proving 분야에서 Olympiad에서 undergraduate 전문 도메인(optimization)으로의 continual training을 domain shift 문제로 명시적으로 정식화한 최초의 시도 중 하나이다.
• Perplexity-weighted preference optimization과 "valid but non-progressing" tactic penalization을 결합한 verifier-driven utility-aware preference learning objective는 formal proving의 binary feedback 특성을 반영한 새로운 방식이다.
• Optlib 기반 400문항의 Lean 4 optimization 전용 벤치마크(OptBench)를 새롭게 구축하여 이 분야 평가 인프라의 공백을 메웠다.

Limitation & Further Study

• OptBench이 400문제로 규모가 제한적이며, undergraduate optimization의 넓은 스펙트럼(예: 비볼록 최적화, 확률적 최적화 등)을 충분히 대표하는지에 대한 검증이 더 필요하다.
• 본 발췌에서는 다른 전문 수학 도메인(예: 확률론, 해석학 등)으로의 일반화 가능성에 대한 논의가 부족해 보이며, 후속 연구에서 다양한 도메인으로의 확장성을 검증할 필요가 있다.
• Perplexity-weighted DPO의 하이퍼파라미터(예: perplexity 가중치, β 등) 민감도에 대한 분석이 충분히 제시되지 않아 재현성과 안정성 검증이 추가로 요구된다.
• Catastrophic forgetting 완화가 완전한지, 혹은 일부 성능 저하가 여전히 존재하는지에 대한 정량적 trade-off 분석이 더 필요하다.

Evaluation

총평: Formal theorem proving을 Olympiad를 넘어 실용적인 undergraduate optimization 도메인으로 확장한 실질적이고 시의적절한 연구로, domain shift 문제를 정교하게 다룬 preference learning 기법과 새로운 벤치마크 제시가 돋보인다. 다만 벤치마크 규모와 일반화 가능성에 대한 추가 검증이 향후 연구에서 보완되어야 할 것으로 보인다.