Leanabell-Prover: Escalonamento Pós-treinamento em Raciocínio Formal

Leanabell-Prover: Posttraining Scaling in Formal Reasoning

April 8, 2025

Autores: Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, Kun Gai

cs.AI

Resumo

Os avanços recentes na prova automática de teoremas (ATP) por meio de LLMs destacaram o potencial do raciocínio formal com códigos Lean 4. No entanto, a ATP ainda não foi revolucionada pelo recente escalonamento pós-treinamento, como demonstrado pelos modelos Open AI O1/O3 e Deepseek R1. Neste trabalho, investigamos todo o processo de pós-treinamento da ATP, visando alinhá-lo com os avanços nos modelos de raciocínio em linguagens naturais. Para começar, realizamos o treinamento contínuo dos modelos atuais de ATP com um conjunto de dados híbrido, que consiste em diversos pares de enunciado-prova, além de dados adicionais destinados a incorporar comportamentos cognitivos que emulam o raciocínio humano e o refinamento de hipóteses. Em seguida, exploramos o aprendizado por reforço utilizando recompensas de resultado retornadas pelo compilador Lean 4. Por meio de nossos processos projetados de treinamento contínuo e aprendizado por reforço, conseguimos aprimorar os provadores formais existentes, incluindo tanto o DeepSeek-Prover-v1.5 quanto o Goedel-Prover, alcançando desempenho de ponta no campo de geração de provas completas. Por exemplo, obtivemos uma taxa de aprovação de 59,8% (pass@32) no MiniF2F. Este é um projeto em andamento, e atualizaremos progressivamente nossas descobertas, liberando nossos dados e detalhes de treinamento.

English

Recent advances in automated theorem proving (ATP) through LLMs have highlighted the potential of formal reasoning with Lean 4 codes. However, ATP has not yet be revolutionized by the recent posttraining scaling as demonstrated by Open AI O1/O3 and Deepseek R1. In this work, we investigate the entire posttraining of ATP, aiming to align it with breakthroughs in reasoning models in natural languages.To begin, we continual train current ATP models with a hybrid dataset, which consists of numerous statement-proof pairs, and additional data aimed at incorporating cognitive behaviors that emulate human reasoning and hypothesis refinement. Next, we explore reinforcement learning with the use of outcome reward returned by Lean 4 compiler. Through our designed continual training and reinforcement learning processes, we have successfully improved existing formal provers, including both DeepSeek-Prover-v1.5 and Goedel-Prover, achieving state-of-the-art performance in the field of whole-proof generation. For example, we achieve a 59.8% pass rate (pass@32) on MiniF2F. This is an on-going project and we will progressively update our findings, release our data and training details.