Mistral lanza Leanstral 1.5 para pruebas formales, reduce el costo a aproximadamente 4 dólares por problema.

Según OneMillion_AI, Mistral AI lanzó recientemente Leanstral 1.5, un modelo de prueba formal para Lean 4 con 119 mil millones de parámetros totales y 65 mil millones de parámetros activos. El modelo se publica bajo licencia Apache-2.0 con acceso gratuito a la API. En PutnamBench, Leanstral 1.5 logra un costo promedio de aproximadamente 4 dólares por problema para resolver, significativamente menor que los sistemas anteriores que costaban decenas a cientos de dólares por problema.

El modelo resuelve 587 de los 672 problemas de PutnamBench y alcanza un 87 % en el benchmark de álgebra abstracta FATE-H y un 34 % en FATE-X, estableciendo nuevos récords de rendimiento para su categoría. Más allá de las pruebas matemáticas, Leanstral 1.5 también se aplicó a la verificación de código, descubriendo 11 errores reales en 57 repositorios Rust de código abierto, 5 de ellos no reportados previamente.