Pythagoras-Prover: Продвижение эффективного формального доказательства посредством дополненной формализации Lean

Аннотация

Современные Lean-доказатели теорем достигают высокой производительности лишь при значительных вычислительных затратах на обучение и инференс, что отчасти обусловлено дефицитом верифицированных данных доказательств и длинными цепочками рассуждений при формальном поиске доказательств, что делает как контролируемую тонкую настройку (SFT), так и сэмплирование затратными. Мы представляем Pythagoras-Prover — семейство вычислительно эффективных Lean-доказателей теорем с открытым исходным кодом, созданных для практических вычислительных бюджетов. Семейство охватывает две парадигмы генерации: авторегрессионные модели с 4B и 32B параметрами, а также первую концептуальную диффузионную модель доказателя (4B), которая итеративно уточняет Lean-доказательства во время инференса. Для эффективности обучения мы построили верифицированный на Lean корпус, стратифицированный по задачам лёгкой, средней и сложной сложности для учебной SFT, благодаря чему модели постепенно овладевают навыками доказательства — от более коротких и простых к более длинным и сложным. В ходе SFT динамический фильтр рассуждений о доказательствах сохраняет информативные цепочки, удерживая каждый экземпляр в пределах контекстного бюджета в 8k токенов. Мы также вводим Augmented Lean Formalisation (ALF), который расширяет скудные верифицированные корпуса за счёт вариантов формальных утверждений, пополняемых с помощью самодистилляции для получения дополнительного обучающего сигнала без полной формальной верификации каждой мутированной части. Возмущая известные задачи с сохранением их формального характера, ALF снижает зависимость от поверхностной формы любого утверждения. Эмпирически Pythagoras-Prover-4B превосходит DeepSeek-Prover-V2-671B по показателю pass@32 на MiniF2F-Test (86,1% против 82,4%) при примерно в 167 раз меньшем числе параметров, а Pythagoras-Prover-32B устанавливает открытый рекорд с результатом 93,0% на MiniF2F-Test и решает 93 из 672 задач PutnamBench. Мы выпускаем MiniF2F-ALF — бенчмарк, чувствительный к контаминации, мутированный с помощью ALF, на котором все протестированные модели теряют точность; здесь наша 32B модель остаётся сильнейшей, а 4B модель сравнивается с предыдущим рекордсменом Goedel-Prover-V2-32B.

English

Modern Lean theorem provers achieve strong performance only with substantial training and inference compute, driven in part by scarce verified proof data and the long reasoning traces of formal proof search, making both supervised fine-tuning (SFT) and sampling expensive. We introduce Pythagoras-Prover, a compute-efficient open-source family of Lean theorem provers built for practical compute budgets. The family spans two generation paradigms: autoregressive models at 4B and 32B parameters, and a first proof-of-concept diffusion-based prover (4B) that iteratively refines Lean proofs at inference time. For training efficiency, we build a Lean-verified corpus stratified into easy, medium, and hard problems for curriculum SFT, so models acquire proof skills progressively from shorter, simpler proofs to longer, harder ones. During SFT, a dynamic proof-reasoning filtering scheme preserves informative proof traces while keeping each instance within an 8k-token context budget. We also introduce Augmented Lean Formalisation (ALF), which expands scarce verified corpora into variants of formal statements, populated via self-distillation for extra training signal without formally verifying every mutated instance. By perturbing known problems while preserving their formal character, ALF reduces reliance on any statement's surface form. Empirically, Pythagoras-Prover-4B surpasses DeepSeek-Prover-V2-671B at pass@32 on MiniF2F-Test (86.1% vs 82.4%) with ~167x fewer parameters, while Pythagoras-Prover-32B sets the open-source state of the art at 93.0% on MiniF2F-Test and solves 93 of 672 PutnamBench problems. We release MiniF2F-ALF, an ALF-mutated contamination-sensitive benchmark on which every evaluated model loses accuracy; here our 32B remains strongest and our 4B matches the prior state of the art, Goedel-Prover-V2-32B.