Novo modelo de IA resolve 92% dos problemas de matemática formal com busca autônoma por lemmas

A Hugging Face e a equipe da Kimi anunciaram o Kimina-Prover-72B, um modelo de inteligência artificial treinado especificamente para criar provas matemáticas formais na linguagem Lean 4 (um sistema usado por matemáticos para verificar se demonstrações estão corretas). O modelo alcançou uma taxa de sucesso de 92,2% no miniF2F, um conjunto de problemas de matemática usado como referência na área — superando o DeepSeek-Prover-V2-671B, que ficou em 86,6%. Junto com a versão de 72 bilhões de parâmetros (números que definem o comportamento de um modelo de IA), a equipe também lançou duas versões menores, com 8 bilhões e 1,7 bilhão de parâmetros, voltadas para quem tem hardware mais modesto.

A principal inovação do Kimina-Prover é o que os pesquisadores chamam de busca por aprendizado por reforço em tempo de teste (TTRL, na sigla em inglês — uma técnica em que o modelo aprende a tomar decisões melhores explorando estratégias diferentes durante o uso). Na prática, isso significa que o modelo consegue descobrir, combinar e reutilizar lemmas intermediários (pequenos resultados matemáticos que servem como degraus para chegar à prova final) de forma autônoma, em vez de simplesmente gerar uma resposta direta. Esse método permite que ele resolva problemas que exigem raciocínio longo e estruturado, decompondo desafios difíceis em partes menores e reutilizáveis — algo que se aproxima mais da forma como matemáticos humanos trabalham.

Durante o treinamento com aprendizado por reforço (RL, uma técnica em que o modelo recebe recompensas quando acerta e ajusta seu comportamento), a equipe introduziu um padrão que incentiva o uso estratégico de lemmas. O modelo recebe entre um e três lemmas formais gerados por outro sistema de IA, e aprende a identificar quais são úteis para cada problema. Inicialmente, a taxa de aproveitamento era baixa, mas depois de ajustar as recompensas para favorecer soluções que usassem lemmas relevantes — e penalizar as que não usassem quando deveriam —, o modelo passou a incorporar lemmas em 30% a 40% dos casos, ignorando os irrelevantes. Essa seletividade é um avanço importante: mostra que o sistema não aplica lemmas cegamente, mas sim de forma inteligente.

Outro diferencial do Kimina-Prover é sua capacidade de corrigir erros: ele consegue ler e interpretar mensagens de erro geradas pelo Lean 4 (avisos que indicam onde uma prova falhou) e propor correções direcionadas, em vez de simplesmente começar do zero. Essa habilidade aumenta muito a eficiência, reduzindo o número de tentativas necessárias para chegar à solução certa. Segundo os pesquisadores, com apenas 32 tentativas (pass@32, uma métrica que indica quantas vezes o modelo tenta resolver o problema), o Kimina-Prover-72B alcançou 84% de acerto; com 1.024 tentativas, chegou a 87,7%. A taxa de 92,2% foi obtida com a busca TTRL completa, embora os autores reconheçam que grande parte do orçamento de tentativas ainda é gasto provando lemmas redundantes — algo que pretendem otimizar em versões futuras.

Os resultados indicam uma mudança no comportamento de escala desses sistemas. Versões anteriores de modelos de prova formal melhoravam de forma aproximadamente linear conforme se aumentava o número de tentativas; agora, os ganhos diminuem depois de cerca de mil tentativas, sugerindo que simplesmente tentar mais vezes não resolve — é preciso buscar de forma mais esperta, justamente o que o TTRL propõe. Todos os modelos — incluindo as versões menores, que obtiveram 78,3% (8B) e 73,4% (1,7B) de acerto com 32 tentativas — estão disponíveis para download na Hugging Face, permitindo que pesquisadores e desenvolvedores experimentem com provas matemáticas formais sem depender de infraestrutura de grande escala.