Leanstral 1.5: Inteligência artificial redefine a verificação formal de código

A Mistral AI anunciou o lançamento do Leanstral 1.5, um novo modelo de linguagem de código aberto licenciado sob a licença de software livre Apache-2.0. Desenvolvido especificamente para atuar na engenharia de provas formais e na verificação de sistemas de software utilizando a linguagem de programação Lean 4, este modelo revoluciona a forma como engenheiros e matemáticos abordam a corretude de algoritmos. O modelo conta com um total de 119 bilhões de parâmetros, mas foi projetado para manter apenas 6 bilhões de parâmetros ativos por token processado. Essa eficiência arquitetônica permite que o Leanstral 1.5 ofereça recursos avançados de computação matemática com uma pegada operacional extremamente leve, tornando a verificação formal acessível para uma gama muito mais ampla de cientistas da computação e desenvolvedores de software em todo o mundo.

Em termos de resultados práticos de avaliação, o Leanstral 1.5 alcançou um marco histórico ao saturar completamente o benchmark miniF2F, registrando um índice absoluto de 100% de acerto tanto em seu conjunto de validação quanto no conjunto de testes. No exigente PutnamBench, que reúne problemas matemáticos da prestigiada competição universitária William Lowell Putnam, o modelo resolveu com sucesso 587 de 672 problemas apresentados, demonstrando um raciocínio lógico profundo e de longo horizonte. Além disso, o Leanstral 1.5 estabeleceu novos recordes de estado da arte nas avaliações de álgebra abstrata de nível de pós-graduação e doutorado, alcançando uma pontuação de 87% no benchmark FATE-H e de 34% no exigente FATE-X. Esses números posicionam o modelo como uma ferramenta de liderança absoluta no ecossistema global de inteligência artificial aplicada à matemática pura.

Um dos principais atrativos do Leanstral 1.5 frente a outras soluções de ponta do mercado de tecnologia é a sua drástica eficiência financeira e operacional. Enquanto modelos concorrentes como o Seed-Prover 1.5 (em sua configuração de alto desempenho 'high') chegam a custar mais de US$ 300 por problema resolvido — exigindo um orçamento computacional massivo de até 10 dias de processamento em placas gráficas por problema (10 H20-days) —, o Leanstral 1.5 resolve problemas equivalentes no PutnamBench com um custo estimado de apenas US$ 4 por problema. Essa redução de quase cem vezes no custo computacional de inferência põe fim ao monopólio das grandes corporações sobre a verificação formal de código, permitindo que equipes locais de engenharia de software e pesquisa acadêmica validem sistemas críticos sem comprometer seus orçamentos.

Para além do domínio dos testes puramente acadêmicos de matemática teórica, o Leanstral 1.5 demonstrou um impacto prático real ao identificar de forma autônoma 5 falhas de software (bugs) anteriormente desconhecidas e não reportadas no GitHub em um conjunto de 57 repositórios de código aberto testados. Esse desempenho prático comprova que a engenharia de provas rigorosa, que historicamente era vista como um campo puramente acadêmico, lento e financeiramente inviável para a indústria comum, agora pode ser integrada de forma fluida a fluxos de trabalho tradicionais de desenvolvimento de software comercial para prevenir incidentes de segurança antes mesmo que o código chegue aos ambientes de produção.

A distribuição ampla do Leanstral 1.5 pela plataforma Hugging Face e por meio de endpoints de API gratuitos busca acelerar a adoção de métodos de engenharia de provas, preenchendo o vazio de ferramentas abertas de alto desempenho para o ecossistema Lean 4.

O processo de treinamento

O desenvolvimento do Leanstral 1.5 envolve um processo de treinamento sofisticado estruturado em três fases principais sequenciais: a fase de mid-training (treinamento intermediário), a fase de supervised fine-tuning (ajuste fino supervisionado, ou SFT) e, finalmente, uma fase de reinforcement learning (aprendizado por reforço) orientada pelo inovador algoritmo CISPO. Esta combinação metodológica permite ao modelo não apenas memorizar a sintaxe matemática da linguagem Lean 4, mas também desenvolver uma intuição lógica para a resolução de teoremas e correção de provas falhas por meio de ciclos contínuos de feedback sistêmico. O modelo é exposto a grandes volumes de dados de código-fonte estruturado e provas matemáticas formais, permitindo que os pesos dos seus 119 bilhões de parâmetros totais se ajustem para prever as táticas de prova mais prováveis de compilar com sucesso.

Na fase crítica de aprendizado por reforço com o CISPO, o Leanstral 1.5 utiliza extensivamente dois ambientes de treinamento distintos, projetados para simular cenários de engenharia do mundo real. O primeiro desses cenários é o chamado ambiente multiturn (multiturno). Neste ambiente dinâmico, o modelo de inteligência artificial recebe o enunciado formal de um teorema matemático específico e tem como tarefa provar ou refutar logicamente a declaração apresentada. O Leanstral 1.5 submete uma proposta inicial de prova ao compilador da linguagem Lean, que por sua vez compila o código e retorna feedbacks detalhados com mensagens de erro, tipos incorretos ou objetivos não alcançados. Com base exclusivamente nesse retorno sintático e semântico do compilador, o modelo refina iterativamente sua abordagem a cada nova tentativa, repetindo o loop até que a prova compile com absoluto sucesso ou que o orçamento computacional total alocado para a tarefa seja inteiramente esgotado.

O segundo ambiente de treinamento, denominado code agent (agente de código), coloca o Leanstral 1.5 na posição de um desenvolvedor de software humano que opera diretamente em um sistema de arquivos bruto (raw filesystem). Nesse ambiente altamente complexo, o modelo não apenas gera texto isolado, mas interage ativamente com o sistema operacional: ele cria e edita arquivos de código-fonte de forma autônoma, executa comandos diretamente no terminal bash do sistema e interage de forma síncrona com o Lean language server (LSP). Essa integração em tempo real com o servidor de linguagem permite ao modelo inspecionar em tempo de execução os objetivos matemáticos (goals), mensagens detalhadas de erro e informações completas de tipos contidas no código.

A capacidade de atuar diretamente como um agente de arquivos capacita o Leanstral 1.5 a lidar com tarefas de engenharia de longo horizonte que vão muito além da resolução de teoremas em linha única. O modelo aprende a navegar de forma inteligente por árvores de repositórios complexas, completando provas parciais herdadas de outros desenvolvedores, construindo de forma autônoma lemas auxiliares que servem de base para provas maiores e persistindo na tarefa ao longo de múltiplos ciclos de compactação de contexto de memória (context compaction). O resultado final desse fluxo completo de engenharia de provas gerado pelo modelo é verificado quanto à sua corretude matemática absoluta por meio de uma versão customizada e modificada da ferramenta SafeVerify desenvolvida internamente, garantindo que a lista de teoremas alvo tenha sido comprovada sem qualquer brecha lógica.

Desempenho nos testes avançados

Para quantificar rigorosamente o avanço trazido pelo Leanstral 1.5, o modelo foi submetido a uma série de testes comparativos usando os benchmarks mais exigentes de matemática formalizados do mundo acadêmico. O miniF2F, um teste de referência entre sistemas para matemática formalizada, apresenta desafios que vão desde problemas aritméticos de nível escolar básico até questões de nível da IMO (Olimpíada Internacional de Matemática). Abrangendo áreas como álgebra de ensino médio, análise combinatória complexa e teoria analítica dos números, o miniF2F exige dos modelos uma extrema flexibilidade na aplicação de táticas. O fato de o Leanstral 1.5 ter saturado completamente os conjuntos de validação e teste com 100% de sucesso demonstra que a barreira dos problemas tradicionais de olimpíada de matemática foi superada por esta nova arquitetura de aprendizado por reforço.

No PutnamBench, que contém um total de 672 problemas extraídos diretamente da tradicional e dificílima Competição Matemática William Lowell Putnam, o Leanstral 1.5 demonstrou uma superioridade notável quando comparado aos seus concorrentes de mercado. O modelo superou a versão de alta especificação do Seed-Prover 1.5 (Seed-Prover 1.5 high) por uma margem de 7 problemas resolvidos adicionais, mesmo custando apenas uma pequena fração do valor operacional exigido pelo rival. Adicionalmente, o Leanstral 1.5 superou de forma consistente outras arquiteturas conceituadas da categoria, como o Goedel-Architect (avaliado sem a ajuda de orientações ou guias em linguagem natural), o AxProverBase e o dispendioso Aleph Prover (cujo custo de inferência oscila pesadamente entre US$ 54 e US$ 68 por problema sem obter o mesmo índice de resolução lógica).

As capacidades do Leanstral 1.5 em matemática de nível avançado também foram testadas nos benchmarks FATE-H e FATE-X, projetados especificamente para avaliar conceitos abstratos de álgebra em níveis de mestrado e doutorado, respectivamente. Esses testes cobrem tópicos extremamente densos de pesquisa acadêmica formal, tais como teoria de grupos ordenados, propriedades estruturais de anéis matemáticos e teoria de módulos sobre anéis não comutativos. Ao cravar os novos recordes históricos de 87% de aproveitamento no FATE-H e 34% de aproveitamento no FATE-X, o Leanstral 1.5 provou que sua capacidade de raciocínio simbólico é capaz de compreender e formalizar conceitos que desafiam até mesmo estudantes humanos de pós-graduação avançada.

Outro marco importante estabelecido com este lançamento é a disponibilização integral como código aberto do benchmark FLTEval, um repositório de testes baseado em pull requests reais submetidos ao famoso projeto colaborativo do Último Teorema de Fermat (Fermat's Last Theorem) em Lean 4. O FLTEval serve como o teste definitivo de engenharia de provas em condições reais, simulando a complexidade, a desorganização de bases de código legadas e as restrições arquitetônicas que engenheiros de software e matemáticos enfrentam no dia a dia. Ao rodar o Leanstral 1.5 nesta base de dados, a taxa de sucesso Pass@1 (uma única tentativa de prova de primeira) saltou de 21.9% registrados na geração anterior para sólidos 28.9%, enquanto a métrica Pass@8 (taxa de acerto considerando até oito caminhos de prova independentes) disparou de 31.9% para impressionantes 43.2%.

Para efeito de comparação de performance e custo de hardware, a métrica de Pass@8 do Leanstral 1.5 no benchmark FLTEval superou os 39.6% obtidos pelo modelo Opus 4.6, que é uma das maiores e mais caras inteligências artificiais proprietárias do mercado de processamento de linguagem natural. O feito torna-se ainda mais impressionante quando se constata que o Leanstral 1.5 roda com um custo de infraestrutura equivalente a apenas um sétimo (1/7) do valor cobrado para a execução do Opus 4.6. Além disso, o novo modelo open-source da Mistral AI expandiu de forma significativa sua liderança de desempenho contra modelos de código aberto concorrentes de tamanho de 3 a 10 vezes maior, demonstrando o poder de sua arquitetura de apenas 6B de parâmetros ativos.

Além da eficiência em termos de custo, o Leanstral 1.5 demonstrou a maior capacidade de escalabilidade em tempo de teste (test-time scaling) já observada em modelos dedicados à inferência de lógica formal e matemática. Um estudo detalhado do comportamento do modelo no PutnamBench sob o indicador Pass@8 revelou um crescimento constante, linear e suave à medida que o orçamento de tokens por tentativa de prova foi expandido de 25.000 (25k) tokens para um teto de 4.000.000 (4M) de tokens. Em termos quantitativos de eficiência computacional, a inteligência artificial solucionou 44 problemas matemáticos quando limitada a um orçamento restrito de 50.000 (50k) tokens; esse número escalou de maneira previsível para 244 problemas resolvidos com um limite de 200.000 (200k) tokens, saltando para 493 resoluções bem-sucedidas em 1.000.000 (1M) de tokens e culminando em impressionantes 587 problemas elucidados ao alcançar a marca de 4.000.000 (4M) de tokens por tentativa.

Verificação de árvores AVL

Embora o treinamento do Leanstral 1.5 tenha sido primariamente direcionado para lidar com o formalismo da matemática pura, o modelo revelou uma aptidão extraordinária na área de verificação formal de código-fonte de sistemas de computação. Um dos principais estudos de caso apresentados para ilustrar essa competência operacional envolve a prova matemática das garantias de tempo de execução e complexidade de espaço das chamadas árvores AVL. Árvores AVL são estruturas de dados clássicas na ciência da computação que consistem em árvores binárias de busca autobalanceadas, as quais garantem por design uma altura máxima de O(log n) através de operações sucessivas de rotação e rebalanceamento durante cada inserção ou exclusão de nós no sistema de arquivos.

Realizar a prova formal de que uma implementação real de árvore AVL realmente cumpre as garantias de complexidade computacional O(log n) é um desafio histórico para a comunidade de métodos formais devido à alta complexidade lógica envolvida na recursão e nos ponteiros da estrutura. A tarefa executada com sucesso pelo Leanstral 1.5 exigiu o uso de técnicas avançadas de indução estrutural para espelhar perfeitamente a estrutura recursiva dos nós da árvore binária, além de um controle cirúrgico do tempo de processamento monádico através de estruturas de rastreamento de tempo. Adicionalmente, o modelo foi obrigado a desenvolver uma análise de caso exaustiva de todas as combinações e caminhos possíveis de rotação de rebalanceamento.

Ao longo de um processo computacional massivo que consumiu mais de 2.7 milhões de tokens e exigiu 22 processos sucessivos de compactação de contexto de memória, o Leanstral 1.5 desmembrou e analisou sistematicamente cada uma das camadas da mônada TimeM utilizada para encapsular as propriedades temporais da estrutura. Este esforço analítico permitiu à inteligência artificial expor e analisar as computações de baixo nível em execução, mesmo quando estas se encontravam intrinsecamente intercaladas com o fluxo de controle principal e com as condicionais lógicas de rebalanceamento dos nós.

Ao término da computação, o modelo Leanstral 1.5 foi capaz de estabelecer com rigor matemático um limite extremamente preciso de exatamente 48 passos de execução por unidade de altura da árvore, somado a uma constante fixa de tempo para a operação crítica de inserção de dados. Em seguida, a inteligência artificial conectou logicamente a altura máxima da árvore ao tamanho total do conjunto de dados por meio de uma relação logarítmica perfeita. O resultado prático foi a entrega de uma prova formal, completa e verificada pelo compilador de Lean 4 de que as operações de inserção e remoção nesta implementação de árvore AVL mantêm-se estritamente na complexidade assintótica de tempo O(log n), fornecendo uma garantia teórica inquebrável para sistemas de software que dependem dessa estrutura em produção.

Descoberta de bugs ocultos

Para colocar à prova o potencial prático de segurança cibernética e garantia de qualidade do Leanstral 1.5, os engenheiros desenharam e implementaram uma esteira (pipeline) de automação completa para encontrar vulnerabilidades estruturais de software. O fluxo de trabalho da ferramenta inicia-se com a utilização do compilador Aeneas, uma ferramenta especializada capaz de traduzir código escrito em Rust diretamente para a linguagem de lógica matemática formal Lean. Uma vez traduzido o código de Rust para a representação semântica do Lean, o Leanstral 1.5 entra em ação para inferir a real intenção funcional do desenvolvedor humano e gerar, de forma autônoma, as propriedades lógicas de corretude que aquele bloco de código específico deveria idealmente satisfazer sob condições normais de uso.

O processo de comprovação destas propriedades lógicas de segurança segue uma estratégia sequencial altamente rigorosa de múltiplas tentativas. Primeiramente, o Leanstral 1.5 tenta provar a validade da propriedade de corretude gerada em até 4 tentativas sequenciais e independentes no compilador de Lean 4. Caso todas as quatro tentativas de provar a corretude do código falhem por problemas de compilação ou inconsistências de dados, a esteira computacional de IA muda de direção e tenta provar o oposto exato: ela busca demonstrar a negação lógica da propriedade original em mais 4 tentativas adicionais. Se a negação lógica for provada com sucesso, significa que existe um caminho no qual o código original falhará inevitavelmente sob determinadas condições de execução, revelando matematicamente a presença de um bug estrutural na lógica do programa.

Ao rodar essa esteira de testes de forma automatizada ao longo de 57 repositórios de código aberto diferentes desenvolvidos originalmente na linguagem de programação Rust, o processo automatizado sinalizou com sucesso um total de 47 propriedades de código violadas logicamente. Um exame humano aprofundado revelou que, dessas notificações, 11 correspondiam a bugs de software genuínos, dos quais 5 erros de programação nunca haviam sido reportados anteriormente por nenhuma ferramenta de análise ou usuário na plataforma de desenvolvimento GitHub. O resultado confirma o potencial dos modelos de inferência formal baseados em inteligência artificial para detectar anomalias profundas e falhas lógicas raras de sistema que ferramentas de verificação estática padrão simplesmente não conseguem capturar devido às suas limitações heurísticas de busca.

Um dos bugs mais notáveis identificados de forma 100% automatizada pela esteira do Leanstral 1.5 ocorreu diretamente na função de sinal (sign function) utilizada no algoritmo de decodificação zigzag (zigzag decoding) da biblioteca varinteger, sob o pacote de desenvolvimento datrs/varinteger. O algoritmo de zigzag decoding é amplamente utilizado na computação para serializar inteiros de tamanho variável de forma eficiente, mapeando números negativos em inteiros positivos para otimizar o espaço em disco ou a largura de banda de transmissão de rede.

O bug de estouro lógico manifestava-se especificamente quando o sistema recebia como dado de entrada o valor de limite máximo do tipo inteiro sem sinal de 64 bits, definido na linguagem de programação como Std.U64.MAX. Ao processar este valor extremo de entrada, a expressão matemática interna representada por (value + 1) sofria um estouro de capacidade física (overflow de inteiros), resultando no travamento completo do sistema de execução (crash) em ambientes compilados em modo de depuração (debug mode) ou em corrupção silenciosa de dados (silent corruption) quando o binário era executado em modo de produção (release mode). Este tipo específico de falha extrema de estouro de limite de memória (edge case) é tradicionalmente indetectável em testes unitários convencionais ou ferramentas de teste de estresse por fuzzer, mas foi facilmente capturado de forma lógica pelo pipeline do Leanstral 1.5.

Instalação e configuração prática

O acesso ao Leanstral 1.5 foi projetado para ser o mais desimpedido e direto possível para engenheiros de sistemas, pesquisadores acadêmicos e analistas de segurança de software em todo o mundo. O modelo está oficialmente licenciado sob os termos de uso amigáveis ao mercado comercial da licença Apache-2.0. Seus pesos de rede neural pré-treinados e prontos para uso estão integralmente disponíveis para download na plataforma Hugging Face, e também há acesso síncrono por meio de um endpoint de API gratuito denominado exatamente como leanstral-1-5, permitindo que qualquer desenvolvedor integre as capacidades de verificação matemática em seus próprios aplicativos sem custo inicial de infraestrutura de hardware dedicada.

Para iniciar o uso local do modelo, recomenda-se fortemente a utilização do Mistral Vibe, uma ferramenta integrada de terminal projetada para agilizar o gerenciamento de modelos e agentes de raciocínio. O desenvolvedor deve, em primeiro lugar, instalar e atualizar o utilitário Mistral Vibe em seu terminal utilizando o gerenciador de pacotes moderno do Python com os seguintes comandos sequenciais de linha de comando: uv tool install mistral-vibe, seguido por uv tool update mistral-vibe, e finalizando o processo de inicialização local com a execução do comando de configuração inicial vibe --setup em seu sistema operacional de preferência.

Uma vez configurada a ferramenta Mistral Vibe no ambiente de desenvolvimento local, o programador pode instalar a versão completa do modelo Leanstral 1.5 executando o comando /leanstallexit na interface e, em seguida, iniciar o agente interativo de táticas matemáticas para Lean 4 por meio da execução direta no console do terminal do utilitário vibe --agent lean. Com esses comandos simples, o ambiente de desenvolvimento local fica automaticamente conectado à inteligência artificial, que passa a escutar e responder a comandos de provas diretamente na máquina do engenheiro de sistemas de maneira fluida.

Com o objetivo de otimizar ao máximo o fluxo de trabalho de engenharia de provas formais e fornecer recursos visuais aprimorados em tempo de execução, é altamente recomendado que os usuários procedam com a instalação da extensão Lean LSP MCP (Model Context Protocol). Para realizar esta integração, o desenvolvedor deve editar o arquivo de configuração local localizado no caminho do diretório padrão ~/.vibe/config.toml e inserir as configurações adequadas no bloco de servidores MCP do arquivo, as quais instruirão a aplicação sobre como inicializar o servidor de linguagem matemática de maneira integrada ao fluxo de trabalho do agente.

O trecho específico de configuração a ser inserido manualmente no arquivo de configuração ~/.vibe/config.toml deve conter os seguintes parâmetros exatos estruturados na linguagem de marcação TOML:

[[mcp_servers]]
name = 'lean-lsp'
transport = 'stdio'
command = 'uvx'
args = ['lean-lsp-mcp']
tool_timeout_sec = 600

Caso não existam outros servidores MCP já previamente configurados e ativos neste arquivo de marcação de dados, o desenvolvedor poderá necessitar remover manualmente a linha vazia contendo mcp_servers = [] para evitar problemas de compatibilidade ou erros de parsing de sintaxe na inicialização do serviço. Após esta breve etapa de ajuste de infraestrutura, o desenvolvedor estará pronto para solicitar que o Leanstral 1.5 resolva teoremas complexos, depure caminhos de prova incompletos ou faça contribuições diretas para repositórios compartilhados de produção.