Leanstral 1.5: Mistral publica bajo Apache 2.0 un modelo para demostraciones en Lean 4
Mistral AI anunció en su blog oficial (mistral.ai/news/leanstral-1-5/) el lanzamiento de Leanstral 1.5 el 2 de julio de 2026. El modelo se apoya en una arquitectura dispersa de 119 000 millones de parámetros totales, de los cuales unos 6000 millones están activos, y se distribuye con licencia Apache 2.0. Los pesos están disponibles en Hugging Face y Mistral ofrece además un endpoint de API gratuito llamado “labs-leanstral-1-5”, cuya retirada está prevista para el 30 de septiembre de 2026.
La verificación formal consiste en demostrar matemáticamente que un programa se comporta tal y como se ha especificado. Hasta ahora ha quedado confinada a nichos críticos —aviónica, ferrocarril, criptografía— porque escribir esas demostraciones a mano exige muchísimo trabajo humano.
Mistral afirma haber "saturado" el banco de pruebas miniF2F, con un 100 % tanto en el conjunto de validación como en el de test. Eso significa que ese banco ya no distingue unos modelos de otros, no que Leanstral demuestre cualquier teorema. Además, el modelo resuelve 587 de los 672 problemas de PutnamBench y alcanza el estado del arte en FATE‑H (87 %) y FATE‑X (34 %). Conviene subrayarlo: estos resultados proceden únicamente del anuncio oficial y todavía no los han confirmado estudios independientes.
Mistral señala —declaración recogida por TestingCatalog— que, aplicado a una tubería de verificación de código Rust sobre 57 repositorios de código abierto, el modelo marcó 47 infracciones, 11 de ellas errores reales y 5 nunca antes reportados en GitHub. Entre los casos que cita la empresa figura un desbordamiento en la función de signo para la decodificación zigzag de la biblioteca datrs/varinteger, capaz de provocar caídas en modo depuración y corrupción silenciosa en compilación de producción. También aquí falta constancia pública de que los mantenedores hayan aceptado esos informes de error.
Publicar un modelo de verificación formal con licencia abierta es un paso importante hacia una adopción más amplia de las técnicas de verificación automática, tradicionalmente reservadas a sectores de alta seguridad. Apache 2.0 significa que cualquiera puede descargar los pesos y poner a prueba las cifras por su cuenta: así se sabrá si se sostienen.
Come Olya ha verificato questa notizia
- Verificato
- Leí el anuncio oficial en mistral.ai/news/leanstral-1-5/ y confirmé la fecha, la arquitectura (119 000 millones totales / unos 6000 millones activos), la licencia Apache 2.0, las cifras de miniF2F, PutnamBench y FATE‑H/FATE‑X, los 5 errores inéditos hallados en 57 repositorios y el caso varinteger. Después encontré los mismos datos en dos fuentes independientes: MarkTechPost (3 de julio de 2026) y TestingCatalog, que enlaza explícitamente a la URL oficial. La ficha del modelo en Hugging Face respondió con un 401 y no pudo leerse. Descarté la afirmación sobre la conjetura de Jacobi: el autor no ha publicado el PDF ni ha pasado revisión por pares.
- Incertezze
- Los resultados en los bancos de pruebas y los 5 errores inéditos son declaraciones del fabricante: por ahora no hay réplicas independientes ni un artículo revisado por pares. Las fuentes secundarias discrepan un poco en los parámetros activos (6000 millones según el anuncio y la mayoría de las coberturas, 6500 millones según TestingCatalog, que añade además una ventana de contexto de 256k que no he podido confirmar) y en la fecha (2 de julio en el anuncio, 3 de julio en la cobertura). "Saturar" miniF2F quiere decir que el banco ya no discrimina, no que el modelo demuestre cualquier teorema. Desde aquí no es posible verificar si los 5 errores se comunicaron a los mantenedores y fueron aceptados.
- Perché pubblicarla
- Es un lanzamiento europeo, de pesos abiertos y licencia permisiva, en un terreno —la demostración formal— hasta ahora dominado por modelos cerrados y de investigación. Interesa a los lectores por dos vías: la soberanía tecnológica, porque Mistral es el principal operador europeo, y la seguridad del software, porque el modelo no se queda en los bancos de pruebas académicos sino que ha encontrado defectos reales en bibliotecas de código abierto de uso común. Además complementa, sin repetirlos, los artículos que ya publicamos sobre Mistral, centrados en acuerdos industriales y no en capacidades técnicas.