Mistral AI liberó Leanstral 1.5, un modelo open-source bajo licencia Apache 2.0 diseñado específicamente para verificación formal en el lenguaje de programación Lean 4. Este entorno se usa para demostrar formalmente teoremas matemáticos y verificar la corrección de software, un ámbito donde los modelos de lenguaje suelen tropezar por la exigencia de razonamiento simbólico paso a paso.

El anuncio confirma dos apuestas fuertes de la casa francesa. Primero, que la verificación formal es un vector serio para diferenciar modelos open-weight frente a los closed-source. Segundo, que la matemática de alto nivel es un terreno donde publicar cifras concretas todavía mueve la aguja del mindshare técnico.

¿Qué benchmarks superó Leanstral 1.5?

Los resultados publicados por Mistral son directos y comparables:

  • miniF2F: 100% de aciertos. El benchmark cubre desde problemas de secundaria hasta el nivel olimpiada matemática.
  • PutnamBench: 587 de 672 problemas resueltos, un 87,3%. El corpus proviene de la William Lowell Putnam Mathematical Competition.
  • FATE-H: 87%. Testea álgebra a nivel maestría en áreas como teoría de grupos.
  • FATE-X: 34%. Testea álgebra doctoral, incluyendo teoría de anillos.

Según Mistral, Leanstral 1.5 lidera el campo open-source en PutnamBench, FATE-H y FATE-X. El único modelo que lo supera en PutnamBench es Aleph Prover, que es closed-source.

De teoremas a bugs reales

El modelo se entrenó principalmente para matemáticas, pero Mistral asegura que también rinde bien en verificación de código. En una prueba práctica, Leanstral 1.5 escaneó 57 repositorios open source y detectó cinco bugs previamente desconocidos. Entre ellos, un bug de overflow en la librería Rust varinteger, un componente que afecta la seguridad de parsers en aplicaciones que manipulan enteros de longitud variable.

Este dato importa por lo que sugiere el pipeline: si un modelo entrenado para pruebas matemáticas encuentra bugs reales al usarlo como scanner formal, la brecha entre "verificación formal académica" y "auditoría de seguridad práctica" se acorta un poco más.

¿Cómo se entrenó y dónde probarlo?

El entrenamiento combinó tres etapas: mid-training, fine-tuning supervisado (SFT) y aprendizaje por refuerzo (RL), la receta estándar post-2024 en la industria.

Los pesos están disponibles en Hugging Face y Mistral también ofrece una API gratuita para probar el modelo sin infraestructura propia. La licencia Apache 2.0 permite uso comercial sin restricciones, lo que abre la puerta a integraciones en toolchains privadas de verificación.

Contexto para desarrolladores en LatAm

Para equipos hispanohablantes que trabajan con Lean 4 o auditan librerías críticas (fintech, criptografía, sistemas embebidos), la combinación "modelo abierto + API gratuita" reduce la barrera de entrada. Un servidor con una GPU consumer alcanza para experimentar; correrlo en producción exige compute serio, pero la fase de prototipado se puede hacer contra la API pública sin costo.

La escena chilena todavía ve la verificación formal como un tema de doctorado, pero herramientas como esta empiezan a hacerla accesible para equipos de ingeniería que auditan smart contracts, kernels o firmware embarcado.