Leanstral 1.5 es un modelo gratuito con licencia Apache-2.0 y 6B parámetros activos que ofrece mejoras significativas de rendimiento en verificación formal y análisis de código. Logra resultados state-of-the-art en múltiples benchmarks y descubre bugs previamente desconocidos en repositorios de código abierto.
- Satura completamente miniF2F (100% en los conjuntos de validación y prueba).
- Resuelve 587/672 problemas de PutnamBench, superando a Seed-Prover 1.5 con una fracción del costo.
- Logra nuevas puntuaciones state-of-the-art de 87% en FATE-H y 34% en FATE-X.
- Descubre 5 bugs previamente no reportados en 57 repositorios probados utilizando un pipeline automatizado.
- Demuestra un fuerte escalado durante la prueba, resolviendo 587 problemas con un presupuesto de 4M tokens.
El modelo habilita la verificación formal práctica al hacer que la ingeniería rigurosa de pruebas sea más accesible y rentable para codebases del mundo real.