Mistral acaba de soltar Leanstral 1.5, un modelo abierto especializado en demostrar teoremas matemáticos y verificar que el software hace lo que dice. Lo publicó el 10 de julio bajo licencia Apache 2.0, la más permisiva que hay: se puede usar en producto comercial, modificar y autohospedar sin pedir permiso.
Es una apuesta distinta a la carrera de los chatbots. Mientras casi todos pelean por el asistente que responde de todo, la francesa se ha ido a un nicho durísimo donde la respuesta o es correcta o no vale nada.
Puntos clave de Leanstral 1.5
- Licencia Apache 2.0, disponible con endpoint de API gratuito y en Hugging Face para autohospedaje.
- Arquitectura Mixture-of-Experts con 119.000 millones de parámetros totales, de los que solo 6.000 millones se activan en cada inferencia.
- 100% en los conjuntos de validación y test de miniF2F, y 587 de 672 problemas resueltos en PutnamBench.
- Usó una séptima parte del cómputo que Opus 4.6 habría gastado en la misma tarea de PutnamBench.
Qué hace un modelo que demuestra teoremas
Leanstral trabaja con Lean 4, un asistente de demostración interactiva que se usa tanto en matemática académica como en verificación de software. La diferencia con un modelo de lenguaje normal es la exigencia: aquí no hay margen para alucinar. Una demostración formal o pasa el verificador o falla, sin puntos intermedios.
Los números que enseña Mistral son fuertes en ese terreno. Además del 100% en miniF2F y los 587 de 672 en PutnamBench, resolvió 87 tareas de álgebra abstracta de nivel de posgrado (FATE-H) y 34 de nivel doctoral (FATE-X). PutnamBench recoge problemas del estilo de la Putnam, la competición matemática universitaria más dura de Estados Unidos, así que 587 de 672 no es un número menor.
La arquitectura ayuda a entender el ahorro. Un Mixture-of-Experts con 119.000 millones de parámetros totales pero solo 6.000 millones activos en cada inferencia significa que el modelo es grande en conocimiento pero barato en cada llamada, porque enciende una fracción pequeña de la red cada vez.
El dato que más importa a quien paga la factura es el de eficiencia. Resolver la misma tarea de PutnamBench con una séptima parte del cómputo de Opus 4.6 significa que hacer verificación seria deja de exigir un presupuesto de laboratorio de frontera.
De las matemáticas al código real
La parte práctica es la verificación de software. Mistral enseña una tubería automatizada de verificación de Rust con Aeneas: pasó por 57 repositorios open source, detectó 47 propiedades violadas y confirmó 11 fallos genuinos. Eso no es un ejercicio de pizarra, es encontrar bugs de verdad en código que ya está publicado.
Que salga abierto y con licencia comercial cambia quién puede usarlo. Cualquier empresa puede bajarlo de Hugging Face y meterlo en su propio pipeline sin depender de una API de pago ni mandar su código a un tercero. Para Mistral es también una jugada de posicionamiento: Europa marcando terreno en un vertical técnico mientras los modelos abiertos ganan peso frente a los cerrados.
Por qué importa
Si tu empresa escribe software que no se puede permitir errar (pagos, cálculo de impuestos, lógica financiera), la verificación formal deja de ser cosa solo de la academia. Un modelo abierto y barato que caza bugs reales en repositorios reales es una herramienta que un equipo técnico puede probar esta misma semana, sin contrato ni presupuesto de frontera.
El movimiento también confirma una tendencia que conviene tener en el radar. La IA está bajando a verticales concretos donde el acierto es medible al 100%, no a base de sonar convincente. En esos terrenos, un modelo abierto que cuesta una séptima parte del cómputo es más interesante que el flagship más caro. Vale la pena mirar qué parte de tu operación tiene ese tipo de problema con respuesta correcta o incorrecta, sin grises.
Relacionado
