Mistral AI Lança Leanstral 1.5: Modelo Open-Source Resolve 587 de 672 Problemas do PutnamBench

A Mistral AI lançou nesta quinta-feira (3) o Leanstral 1.5, um modelo especializado em provas matemáticas formais usando o assistente de provas Lean 4. Os pesos estão disponíveis sob licença Apache 2.0, e uma API gratuita já está no ar.

O Leanstral 1.5 pertence à família Mistral Small 4 e atualiza o modelo Leanstral-2603 anterior. O foco é prova automatizada de teoremas (ATP) e engenharia de provas — um campo cada vez mais relevante para verificação de software, segurança de contratos inteligentes e matemática computacional.

Arquitetura: 119 bilhões de parâmetros com ativação eficiente

O modelo usa arquitetura mixture-of-experts (MoE) com 128 especialistas, ativando apenas 4 por token. No total são 119 bilhões de parâmetros, mas apenas 6,5 bilhões ficam ativos por token — o que mantém o custo computacional baixo enquanto a capacidade total permanece alta.

A janela de contexto é de 256 mil tokens. A entrada aceita texto e imagem (multimodal), mas a saída é apenas texto. O modelo opera como um agente de código: edita arquivos, executa comandos bash e interage com o servidor de linguagem Lean (LSP) que expõe objetivos, erros e informações de tipo em tempo real.

Treinamento em três estágios

O treinamento do Leanstral 1.5 segue três fases: mid-training, fine-tuning supervisionado (SFT) e aprendizado por reforço com CISPO. Dois ambientes de RL moldam o comportamento agentivo do modelo:

• Ambiente multiturno: o modelo recebe um enunciado de teorema, tenta prová-lo ou refutá-lo, lê o feedback do compilador Lean e refina a prova ao longo de múltiplas tentativas até ter sucesso ou esgotar o orçamento de tokens.
• Ambiente de agente de código: o Leanstral trabalha dentro de um sistema de arquivos real, podendo completar provas parciais, construir lemas auxiliares e persistir através de compactação de contexto — essencial para tarefas longas que excedem a janela de tokens.

Benchmarks: saturação do miniF2F e 587 problemas do PutnamBench

O Leanstral 1.5 satura o miniF2F, alcançando 100% tanto no conjunto de validação quanto no de teste. No PutnamBench — uma das avaliações mais difíceis de raciocínio matemático — resolve 587 dos 672 problemas.

O modelo também estabelece um novo estado da arte nos benchmarks de álgebra FATE-H (87%) e FATE-X (34%). No FLTEval, construído a partir de pull requests reais do repositório do Último Teorema de Fermat, o pass@1 sobe de 21,9 para 28,9 e o pass@8 vai de 31,9 para 43,2.

O desempenho é particularmente notável considerando o custo: o Leanstral supera o Opus 4.6 no FLTEval (39,6 de pass@8) por um sétimo do custo, e amplia a vantagem sobre modelos open-source de três a dez vezes maiores. No PutnamBench, cada problema custa cerca de US$ 4 — uma fração dos US$ 300+ estimados para o Seed-Prover 1.5 em configuração máxima.

Test-time scaling: quanto mais tokens, melhor o resultado

Um dos comportamentos mais relevantes do Leanstral 1.5 é o test-time scaling: aumentar o orçamento de tokens por tentativa melhora diretamente os resultados. A equipe da Mistral reporta 44 problemas resolvidos com 50 mil tokens, 244 com 200 mil, 493 com 1 milhão e 587 com 4 milhões de tokens no PutnamBench pass@8.

Casos reais: bugs encontrados em repositórios de código

Embora treinado primariamente em matemática, o Leanstral também verifica código. A Mistral documenta dois estudos de caso relevantes para engenheiros:

• Prova de complexidade O(log n) para uma implementação real de árvore AVL, usando indução estrutural e rastreamento de tempo monádico via a mônada TimeM. A prova rodou por mais de 2,7 milhões de tokens em 22 compactações de contexto.
• Detecção de bugs em 57 repositórios open-source usando um pipeline automatizado que traduz Rust para Lean via Aeneas. O Leanstral inferiu a intenção do desenvolvedor e gerou propriedades de corretude. Foram sinalizadas 47 propriedades violadas e 11 bugs genuínos — cinco deles nunca antes reportados no GitHub.

Um dos bugs estava na função sign para decodificação zigzag no crate datrs/varinteger. Com a entrada Std.U64.MAX, a expressão (value + 1) causava overflow — resultando em crashes no modo debug e corrupção silenciosa em release.

Como usar: API gratuita, Mistral Vibe ou self-hosting

O caminho mais simples é via Mistral Vibe, o CLI de agentes da Mistral. O Leanstral roda no plano gratuito — basta habilitar “Labs models” na conta, criar uma chave de API e executar:

uv tool install mistral-vibe
uv tool update mistral-vibe
vibe --setup
# Dentro do Vibe:
/leanstall
exit
vibe --agent lean

Para self-hosting, é necessário vLLM 0.24.0 ou superior. O serve exige cerca de 4 GPUs com tensor-parallel-size 4 e 200 mil tokens de contexto máximo. O modelo também suporta tool calling no estilo OpenAI, e a Mistral recomenda o servidor lean-lsp-mcp para integração mais profunda com o ecossistema Lean.

O lançamento do Leanstral 1.5 reforça a aposta da Mistral AI em modelos especializados e de nicho — uma estratégia diferente de competir diretamente em chatbots generalistas. A combinação de licença aberta, API gratuita e desempenho de ponta em provas formais coloca o Leanstral como ferramenta relevante para equipes que trabalham com verificação de software, segurança de sistemas críticos e matemática computacional.