OProver: Единый фреймворк для агентного формального доказательства теорем

Аннотация

Недавний прогресс в формальном доказательстве теорем выиграл от крупномасштабной генерации доказательств и обучения с учётом верификатора, однако агентное доказательство редко интегрируется в обучение доказателю, появляясь лишь на этапе вывода. Мы представляем OProver — единую среду для агентного формального доказательства теорем в Lean 4, в которой неудачные попытки доказательства итеративно пересматриваются с использованием извлечённых проверенных компилятором доказательств и обратной связи компилятора Lean. OProver обучается с помощью продолженного предварительного обучения с последующим итеративным пост-обучением: каждая итерация запускает агентное доказательство, индексирует недавно проверенные доказательства в OProofs и память поиска, использует траектории исправления как данные SFT и использует нерешённые сложные случаи для RL. OProofs построен на основе общедоступных ресурсов Lean, крупномасштабного синтеза доказательств и следов агентного доказательства, содержащих 1,77 млн утверждений Lean, 6,86 млн проверенных компилятором доказательств и сериализованные траектории с извлечённым контекстом, неудачными попытками, обратной связью и исправлениями. На пяти бенчмарках OProver-32B достигает лучшего показателя Pass@32 на MiniF2F (93,3%), ProverBench (58,2%) и PutnamBench (11,3%) и занимает второе место на MathOlympiad (22,8%) и ProofNet (33,2%) — больше лучших позиций, чем любой предыдущий доказатель целых теорем с открытым весом.

English

Recent progress in formal theorem proving has benefited from large-scale proof generation and verifier-aware training, but agentic proving is rarely integrated into prover training, appearing only at inference time. We present OProver, a unified framework for agentic formal theorem proving in Lean 4, in which failed proof attempts are iteratively revised using retrieved compiler verified proofs and Lean compiler feedback. OProver is trained through continued pretraining followed by iterative post-training: each iteration runs agentic proving, indexes newly verified proofs into OProofs and the retrieval memory, uses repair trajectories as SFT data, and uses unresolved hard cases for RL. OProofs is built from public Lean resources, large-scale proof synthesis, and agentic proving traces, containing 1.77M Lean statements, 6.86M compiler-verified proofs, and serialized trajectories with retrieved context, failed attempts, feedback, and repairs. Across five benchmarks, OProver-32B attains the best Pass@32 on MiniF2F (93.3%), ProverBench (58.2%), and PutnamBench (11.3%), and ranks second on MathOlympiad (22.8%) and ProofNet (33.2%) more top placements than any prior open-weight whole-proof prover.