Leanstral 1.5: o modelo da Mistral que prova teoremas — e achou bugs que ninguém tinha visto

Há uma diferença fundamental entre um modelo de linguagem que diz que uma resposta está certa e um sistema que prova isso matematicamente. A primeira categoria domina as manchetes; a segunda, até pouco tempo atrás, vivia confinada a nichos acadêmicos. O Leanstral 1.5, lançado pela Mistral na quinta-feira sob licença Apache 2.0, é o esforço mais sério até agora de tirar a prova formal do nicho — e os números que o acompanham merecem atenção.

O modelo escreve provas em Lean 4, uma linguagem em que cada teorema precisa ser verificado por um compilador que não aceita retórica: ou a prova fecha, ou não fecha. Não há espaço para a alucinação convincente que assombra os LLMs convencionais. E é justamente por isso que os resultados impressionam.

Os números: da competição universitária ao estado da arte

No PutnamBench — coleção formalizada de problemas da Putnam, a mais difícil competição de matemática universitária dos Estados Unidos —, o Leanstral 1.5 resolve 587 dos 672 problemas. No miniF2F, benchmark clássico de matemática olímpica formalizada, o modelo simplesmente saturou: 100%. Nos benchmarks FATE, mais recentes e mais duros, marca 87% no FATE-H e 34% no FATE-X — estado da arte em ambos.

Tão interessante quanto os placares é a curva que os produz. Com orçamento de 50 mil tokens por problema, o modelo resolve 44 questões do PutnamBench; com 4 milhões de tokens, chega às 587. É o test-time scaling — a capacidade de converter mais tempo de computação em mais capacidade — funcionando de forma quase linear num domínio onde cada acerto é verificável por máquina.

Como um provador vira um agente

A novidade técnica do Leanstral 1.5 está menos na arquitetura — um MoE (mistura de especialistas) de 119 bilhões de parâmetros com apenas 6 bilhões ativos por token — e mais no modo de operação. O modelo trabalha em dois ambientes. No primeiro, mais tradicional, ele dialoga com o compilador de Lean: propõe uma prova, recebe os erros, refina, repete.

No segundo, ele age como um desenvolvedor: edita arquivos, roda comandos de terminal e consulta o servidor de linguagem do Lean para inspecionar o estado das metas de prova em tempo real. Num estudo de caso, o modelo provou que a inserção em árvores AVL tem complexidade O(log n) — uma prova que exigiu 2,7 milhões de tokens e 22 compactações de contexto. Não é um chatbot respondendo perguntas; é um agente executando um projeto de engenharia de provas do começo ao fim.

Bugs de verdade, encontrados por prova

O detalhe mais persuasivo do anúncio não é benchmark — é arqueologia de software. Ao tentar verificar formalmente propriedades de 57 repositórios de código aberto, o Leanstral encontrou 5 bugs até então desconhecidos. O exemplo destacado: um estouro na função de sinal da biblioteca de decodificação zigzag datrs/varinteger, que trava o programa em modo debug e corrompe dados silenciosamente em modo release quando recebe valores máximos.

É o tipo de defeito que testes convencionais raramente pegam — o caso extremo que ninguém escreveu no conjunto de testes. A verificação formal, por definição, não deixa caso extremo de fora: ou a propriedade vale para todas as entradas, ou a prova não fecha. Se essa abordagem escalar, muda o cálculo econômico de auditar software crítico.

O ceticismo necessário

Antes de decretar a era da verificação formal em massa, três ressalvas. Primeiro, o custo de US$ 4 por problema vale para a Putnam formalizada — verificar propriedades de software real, como no caso da árvore AVL, consumiu milhões de tokens para uma única prova. Segundo, o gargalo histórico da área continua de pé: alguém precisa formalizar a especificação antes de o modelo prová-la, e traduzir intenção humana em enunciado matemático segue sendo trabalho especializado.

Terceiro, um detalhe curioso da disponibilização: a API gratuita do modelo tem aposentadoria marcada para 30 de setembro de 2026 — uma janela experimental, não um compromisso de longo prazo. Os pesos, esses sim, são definitivos: Apache 2.0 no Hugging Face, para quem quiser rodar por conta própria.

Por que isso importa além da matemática

A aposta da Mistral é que "engenharia de provas" vire uma disciplina prática, não um luxo acadêmico. Compiladores, criptografia, sistemas financeiros, firmware de dispositivos médicos — há uma lista longa de domínios onde "quase certo" não basta e onde a verificação formal sempre foi cara demais para ser rotina. Um agente aberto que derruba o custo em duas ordens de grandeza mexe nessa equação.

O Leanstral 1.5 não escreve o software do futuro — mas pode ser a ferramenta que finalmente torna viável provar que o software do presente faz o que promete.

Perguntas Frequentes

O que é Lean 4 e o que significa "prova formal"?

Lean 4 é uma linguagem de programação e assistente de provas em que teoremas matemáticos e propriedades de software são escritos de forma que um compilador possa verificar cada passo lógico. Uma prova formal aceita pelo compilador é garantidamente correta — não há espaço para erro de raciocínio disfarçado de prosa convincente.

O Leanstral 1.5 é gratuito?

Os pesos estão no Hugging Face sob licença Apache 2.0, livres para uso comercial. A Mistral também oferece uma API gratuita (leanstral-1-5), mas com aposentadoria já anunciada para 30 de setembro de 2026 — sinal de implantação experimental.

Isso substitui testes de software?

Não. A verificação formal complementa testes: prova propriedades específicas (ausência de estouro, complexidade, correção de algoritmo) para todas as entradas possíveis, mas exige que alguém formalize o que se quer provar. O custo por propriedade ainda é alto — o caso da árvore AVL consumiu 2,7 milhões de tokens — e a formalização da especificação continua sendo trabalho humano especializado.