LeanPRM: Lean rotulou 152 mil passos de provas sem humanos e elevou a precisão para 74,7%

Verificar as longas provas matemáticas escritas por modelos de linguagem está virando um gargalo. Os autores do LeanPRM propõem obter a rotulagem passo a passo do assistente de provas Lean, sem anotadores. O resultado é um dataset com 10 634 provas e 152 mil passos rotulados. Um verificador baseado em Qwen3-4B, treinado nesses dados, subiu de 48,2 para 74,7 na precisão de acerto do rótulo do passo no conjunto reservado LeanPRM-Bench (200 provas). O mesmo modelo-base, treinado no PRM800K, chegou a 60,3.

De onde vêm os rótulos

Só é possível treinar um verificador de processo (PRM) com dados em que cada passo tem uma avaliação de «correto» ou «incorreto». Para provas abertas, esses rótulos são difíceis de obter. Anotadores humanos são caros. Rótulos derivados da resposta final não ajudam, porque uma prova não tem um número com o qual se possa conferir o resultado. E formalizar cada prova em Lean exige o trabalho de especialistas.

O LeanPRM contorna essas limitações da seguinte forma. O modelo escreve a prova em linguagem natural e, em paralelo, uma prova formal, sem receber feedback do Lean. Depois, o Lean verifica a versão formal e atribui um rótulo a cada passo. Um segundo modelo filtra os casos em que a falha se deve apenas à sintaxe do texto formal. Com isso, os rótulos negativos refletem erros matemáticos de fato, e não deslizes de escrita.

O que os números mostram

Principais resultados do artigo:

• dataset: 10 634 provas, 152 mil passos com rótulos, sem anotação manual;
• LeanPRM-Bench (200 provas reservadas): o Qwen3-4B subiu de 48,2 para 74,7 de correspondência exata por passo;
• baseline PRM800K no mesmo modelo: 60,3;
• em três dos quatro benchmarks externos, o verificador treinado no LeanPRM supera a versão treinada no PRM800K;
• na seleção best-of-N em problemas de nível IMO, ele escolhe provas de melhor qualidade;
• o ganho foi confirmado em modelos de 0,6B a 8B parâmetros no LeanPRM-Bench, no Hard2Verify e no IMO-GradingBench.

A consistência do efeito entre tamanhos importa tanto quanto o número recorde. A melhora aparece tanto no modelo bem pequeno quanto no de oito bilhões de parâmetros. Isso indica que o mérito está na qualidade do sinal, e não na escolha feliz de uma única configuração.

Onde vale olhar com mais atenção

A maior diferença, 48,2 contra 74,7, foi medida em um benchmark montado pelos próprios autores, com os mesmos procedimentos de geração e rotulagem. Para uma amostra assim, o treinamento com LeanPRM leva uma vantagem natural. Por isso os testes externos têm mais valor: neles o ganho aparece em três dos quatro benchmarks, ou seja, não em todos. A descrição disponível do artigo não detalha o resultado no quarto, e vale conferir o texto completo.

Há também uma limitação estrutural. Os rótulos são tão corretos quanto a correspondência entre a prova formal e a prova em linguagem natural. Se o modelo escreveu uma versão formal que diverge do texto, o Lean avalia algo diferente do que o leitor humano lê. O filtro do segundo modelo reduz o risco de ruído causado pela sintaxe, mas não garante a correspondência total entre as duas versões. A cobertura também é limitada: só é possível rotular o que se conseguiu formalizar.

O valor prático está na escala. O volume de dados cresce com o número de enunciados formais disponíveis, e não com o orçamento para especialistas. Para equipes que treinam modelos matemáticos com best-of-N ou RL com recompensas de processo, é uma chance de obter um sinal denso nos passos do raciocínio sem comprar anotação. Para avaliar a abordagem, vale rodar o seu próprio verificador no Hard2Verify e no IMO-GradingBench. Também é útil checar até que ponto o ganho se mantém em provas de áreas distantes das que foram formalizadas em Lean.