El nuevo modelo gratuito de Mistral encuentra errores reales demostrando que el código es correcto
Mistral ha publicado Leanstral 1.5, un pequeño modelo de código abierto que redacta demostraciones matemáticas formales y ya ha encontrado cinco errores reales en código abierto.
Mistral AI acaba de publicar Leanstral 1.5, un modelo gratuito que hace algo que la mayoría de las IA no puede: demostrar con certeza matemática que un fragmento de código o una afirmación matemática es realmente correcto, en vez de limitarse a concluir que «probablemente está bien según los patrones». Y en su primera prueba en el mundo real ya encontró cinco errores que habían permanecido ocultos a plena vista.
Leanstral 1.5 está diseñado para Lean 4, un «asistente de demostración». Puedes imaginarlo como un lenguaje de programación en el que todas las afirmaciones deben ser impecables desde el punto de vista lógico antes de que el ordenador las acepte. Es muy distinto de un chatbot de IA normal, capaz de mostrarse seguro aunque esté equivocado. El modelo es pequeño para los estándares actuales, 6.000 millones de parámetros activos y licencia Apache 2.0, por lo que cualquiera puede utilizarlo, modificarlo o ejecutarlo localmente, pero tiene una capacidad extraordinaria: «satura» miniF2F, una conocida prueba matemática, lo que significa que acierta absolutamente todos los problemas, y resolvió 587 de los 672 problemas de PutnamBench, una colección de preguntas de matemáticas de competición célebres por su dificultad.
El titular más práctico es que Mistral aplicó Leanstral 1.5 a 57 repositorios reales de código abierto y este señaló cinco errores desconocidos hasta entonces. Por ejemplo, una pequeña biblioteca para codificar números, varinteger, utilizada en el proyecto datrs, tenía un fallo al gestionar el signo que provocaba una corrupción de datos silenciosa con una entrada específica en un caso límite. Ninguna persona lo había detectado. El modelo sí lo hizo al demostrar de verdad el comportamiento del código, en lugar de deducirlo a partir de ejemplos.
Qué está pasando realmente: La mayoría de las herramientas de IA para programar funcionan mediante reconocimiento de patrones. Han leído mucho código y predicen qué viene a continuación. Este enfoque funciona bien la mayor parte del tiempo, pero puede pasar por alto errores lógicos sutiles, especialmente esos casos límite con una diferencia de uno como el que acaba de encontrar Leanstral. La verificación formal invierte el método: en vez de predecir, demuestra. Históricamente ha sido un trabajo lento y reservado a especialistas. Que un modelo abierto, gratuito y con 6.000 millones de parámetros lo haga lo bastante bien como para encontrar errores reales indica que este ámbito especializado empieza a ser accesible, en lugar de permanecer encerrado en laboratorios académicos.
Qué significa esto para ti: Si solo sientes curiosidad por la IA, no necesitas tocar esta herramienta: es especializada, como una llave dinamométrica, no un martillo. Si programas profesionalmente, en especial software crítico para la seguridad, bibliotecas criptográficas, analizadores sintácticos o sistemas integrados, merece la pena echarle un vistazo: es gratuita, funciona sin enviar tu código a una API en la nube y ya ha demostrado que puede detectar lo que se escapó a una revisión humana. Para la mayor parte de la programación cotidiana, tus herramientas actuales siguen siendo la opción adecuada; esta es para aquellos momentos en los que «probablemente está bien» no es suficiente.
Fuentes
El gran informe anual de Stanford sobre la IA ya está aquí, y la brecha de confianza se amplía
El AI Index 2026 de Stanford HAI muestra rápidos avances en capacidad junto con más incidentes de seguridad, peores puntuaciones de transparencia y una brecha creciente entre la confianza de expertos y ciudadanos.
