es.wedoany.com Noticia: La empresa europea de inteligencia artificial Mistral AI anunció el pasado día 2 de este mes, hora local, el lanzamiento del modelo Leanstral 1.5, orientado al lenguaje de programación Lean 4 para la formalización de demostraciones matemáticas. Este modelo cuenta con un total de 119B parámetros, activa 6B parámetros y se publica bajo la licencia de código abierto Apache-2.0.
Mistral AI indicó que el modelo Leanstral 1.5 logró una tasa de finalización del 100% tanto en el conjunto de validación como en el conjunto de prueba del benchmark matemático formal miniF2F; resolvió 587 de las 672 preguntas de Lean 4 en el conjunto de problemas del concurso matemático PutnamBench; y para la serie de benchmarks de álgebra abstracta FATE, alcanzó una tasa de éxito del 87% en el nivel de maestría FATE-H y del 34% en el nivel de doctorado FATE-X, siendo ambos los mejores resultados. Estas pruebas demuestran que la capacidad matemática del modelo ya ha alcanzado un nivel utilizable.
Mistral AI destacó la ventaja de coste del nuevo modelo: para los problemas del conjunto de datos PutnamBench, el gasto medio de resolución de Leanstral 1.5 es de solo 4 dólares, mientras que Seed-Prover 1.5 requiere más de 300 dólares y Aleph Prover también necesita entre 54 y 68 dólares.
En aplicaciones de escenarios reales, Leanstral 1.5 marcó 47 atributos de incumplimiento en los 57 repositorios de código probados, de los cuales 11 apuntaban a defectos reales, incluyendo 5 problemas que no habían sido reportados anteriormente en GitHub.
