OProver: Lean 4 증명 에이전트를 학습에 통합 — MiniF2F Pass@32 93.3%

OProver는 Lean 4에서 실패한 증명 시도를 컴파일러 피드백과 검증된 증명 검색으로 반복 수정하는 에이전틱 증명 프레임워크입니다. 사전 학습과 반복 후학습(증명 실행, SFT, RL)을 통해 훈련되며, 1.77M Lean 문장과 6.86M 검증된 증명을 포함한 OProofs 데이터셋을 구축했습니다. OProver-32B는 MiniF2F(93.3%), ProverBench(58.2%), PutnamBench(11.3%)에서 최고 Pass@32를 달성했으나, MathOlympiad와 ProofNet에서는 2위에 그쳐 일부 벤치마크에서 한계를 보입니다.

• #theorem-proving
• #lean4
• #agentic
• #oprover
• #deepseek