Leanstral 1.5: a Mistral publica sob Apache 2.0 um modelo para demonstrações em Lean 4
A Mistral AI anunciou no seu blogue oficial (mistral.ai/news/leanstral-1-5/) o lançamento do Leanstral 1.5 a 2 de julho de 2026. O modelo assenta numa arquitetura esparsa com 119 mil milhões de parâmetros no total, dos quais cerca de 6 mil milhões estão ativos, e é distribuído sob licença Apache 2.0. Os pesos estão disponíveis no Hugging Face e a Mistral oferece também um endpoint de API gratuito chamado “labs-leanstral-1-5”, cuja desativação está prevista para 30 de setembro de 2026.
A verificação formal consiste em demonstrar matematicamente que um programa se comporta exatamente como especificado. Até agora manteve-se confinada a nichos críticos — aviónica, ferrovia, criptografia — porque escrever essas demonstrações à mão exige imenso trabalho humano.
A Mistral afirma ter "saturado" o teste de referência miniF2F, com 100% tanto no conjunto de validação como no de teste. Isso significa que esse teste deixou de conseguir distinguir os modelos entre si, não que o Leanstral demonstre qualquer teorema. Além disso, o modelo resolve 587 dos 672 problemas do PutnamBench e atinge o estado da arte em FATE‑H (87%) e FATE‑X (34%). Convém sublinhar: estes resultados vêm exclusivamente do anúncio oficial e ainda não foram confirmados por estudos independentes.
A Mistral refere — declaração retomada pelo TestingCatalog — que, aplicado a uma cadeia de verificação de código Rust em 57 repositórios de código aberto, o modelo assinalou 47 violações, das quais 11 eram erros reais e 5 nunca tinham sido reportados no GitHub. Entre os casos citados pela empresa está um transbordo na função de sinal usada na descodificação zigzag da biblioteca datrs/varinteger, capaz de provocar falhas em modo de depuração e corrupção silenciosa na versão de produção. Também aqui não há confirmação pública de que os responsáveis pelos projetos tenham aceitado esses relatos.
Lançar um modelo de verificação formal com licença aberta é um passo importante para uma adoção mais alargada das técnicas de verificação automática, tradicionalmente fechadas em setores de elevada segurança. Apache 2.0 significa que qualquer pessoa pode descarregar os pesos e pôr os números à prova por si própria — é assim que se saberá se aguentam.
Come Olya ha verificato questa notizia
- Verificato
- Li o anúncio oficial em mistral.ai/news/leanstral-1-5/ e confirmei a data, a arquitetura (119 mil milhões no total / cerca de 6 mil milhões ativos), a licença Apache 2.0, os números do miniF2F, do PutnamBench e do FATE‑H/FATE‑X, os 5 erros inéditos encontrados em 57 repositórios e o caso varinteger. Encontrei depois os mesmos dados em duas fontes independentes: MarkTechPost (3 de julho de 2026) e TestingCatalog, que remete explicitamente para o URL oficial. A ficha do modelo no Hugging Face devolveu 401 e não foi possível lê-la. Descartei a alegação sobre a conjetura jacobiana: o autor ainda não publicou o PDF nem passou por revisão por pares.
- Incertezze
- Os resultados nos testes de referência e os 5 erros inéditos são declarações do fabricante: até agora não há replicações independentes nem artigo revisto por pares. As fontes secundárias divergem ligeiramente quanto aos parâmetros ativos (6 mil milhões no anúncio e na maioria das notícias, 6,5 mil milhões segundo o TestingCatalog, que acrescenta ainda uma janela de contexto de 256k que não consegui confirmar) e quanto à data (2 de julho no anúncio, 3 de julho na cobertura). "Saturar" o miniF2F quer dizer que o teste deixou de discriminar, não que o modelo demonstre qualquer teorema. Daqui não é possível verificar se os 5 erros foram comunicados aos responsáveis dos respetivos projetos e por eles aceites.
- Perché pubblicarla
- É um lançamento europeu, de pesos abertos e licença permissiva, num terreno — a demonstração formal — até agora dominado por modelos fechados e de investigação. Interessa aos leitores em duas frentes: a soberania tecnológica, porque a Mistral é o principal operador europeu, e a segurança do software, porque o modelo não se fica pelos testes académicos e encontrou defeitos reais em bibliotecas de código aberto de uso corrente. É ainda complementar, e não redundante, face aos artigos que já publicámos sobre a Mistral, focados em acordos industriais e não em capacidades técnicas.