Mistral presenta Leanstral, un agente open-source pensado para reducir el cuello de botella humano en la verificación de código y pruebas formales. ¿Te imaginas generar código que además se verifica automáticamente contra especificaciones estrictas? Esa es la idea: que la prueba no sea un trámite manual interminable, sino parte del propio agente.
Qué es Leanstral
Leanstral es el primer agente open-source entrenado específicamente para Lean 4, el asistente de pruebas capaz de expresar objetos matemáticos complejos y especificaciones de software. A diferencia de enfoques que envuelven modelos generalistas, Leanstral se diseñó para ser eficiente: tiene alrededor de 6B de parámetros activos y una arquitectura esparsa optimizada para tareas de proof engineering.
¿Qué significa esto en la práctica? Que no se trata solo de generar conjeturas: Leanstral genera, prueba y verifica dentro del flujo de trabajo formal, usando a Lean como verificador perfecto.
Abierto y accesible
- Pesos con licencia Apache 2.0 para que cualquiera pueda descargar y ejecutar el modelo en su propia infraestructura.
- Modo agente integrado en Mistral Vibe para empezar sin configuraciones con el comando
/leanstall. - API pública y gratuita/low-cost por tiempo limitado bajo el endpoint
labs-leanstral-2603para obtener retroalimentación real.
La apuesta es clara: visibilidad, reproducibilidad y uso real en repositorios formales.
Eficiencia y evaluación
Mistral presentó FLTEval, una suite de evaluación que mide utilidad en escenarios reales de ingeniería de pruebas en vez de problemas matemáticos aislados. En esa prueba, Leanstral compite con agentes comerciales y modelos open-source mucho más grandes.
Resultados clave (resumen):
- Leanstral logra mejores puntajes con mucho menos costo computacional que modelos abiertos gigantes.
- Frente a la familia Claude, Leanstral ofrece una relación costo/beneficio notable: por ejemplo,
pass@2alcanza 26.3 puntos costando solamente 36 USD, mientras que Sonnet cuesta 549 USD para 23.7 puntos y Opus llega más alto en calidad pero con costos muy superiores.
Tabla simplificada de la evaluación (puntaje | costo):
| Modelo | Costo (USD) | Puntaje |
|---|---|---|
| Haiku | 184 | 23.0 |
| Sonnet | 549 | 23.7 |
| Opus | 1650 | 39.6 |
| Leanstral | 18 | 21.9 |
| Leanstral pass@2 | 36 | 26.3 |
| Leanstral pass@4 | 72 | 29.3 |
| Leanstral pass@16 | 290 | 31.9 |
La traducción práctica: Leanstral escala con eficiencia y ofrece resultados competitivos sin necesitar huir hacia tamaños monstruosos.
Casos de uso reales
Mistral mostró ejemplos concretos para que esto no suene a promesa vaga:
-
Migraciones tras cambios en Lean: Leanstral diagnosticó un problema real en un post de Proof Assistants Stack Exchange. No adivinó; construyó código de prueba, reprodujo el error y explicó por qué
defbloqueaba la tácticarw. La solución propuesta fue usarabbrevpara crear un alias transparente. Resultado: explicación clara y un fix aplicable. -
Conversión y razonamiento sobre programas: se le dio material de Rocq y Leanstral tradujo definiciones a Lean, añadió notación útil y probó propiedades sobre programas sencillos, como demostrar que una asignación suma 2 al valor de una variable.
Estos ejemplos muestran que Leanstral no solo genera código; razona sobre él dentro del ecosistema formal.
Cómo probarlo hoy
- En Mistral Vibe: usa
/leanstallpara empezar sin instalaciones. - API Labs: llama a
labs-leanstral-2603mientras el endpoint permanezca disponible para recopilar uso real. - Descarga local: si prefieres control total, descarga los pesos Apache 2.0 y ejecútalos en tu hardware.
¿Eres investigador, desarrollador de pruebas formales o simplemente curioso? Puedes integrarlo en flujos de trabajo MCP a través de vibe; Leanstral está optimizado para obtener el máximo con lean-lsp-mcp.
Reflexión final
Leanstral representa un paso importante hacia agentes que no solo generan código, sino que lo verifican formalmente. No resuelve todos los problemas, pero baja la barrera de entrada: menos tiempo gastado en revisión humana, más velocidad para iterar en matemáticas de frontera y software crítico. ¿La mejor parte? Es open-source y accesible para que la comunidad lo ponga a prueba, mejore y lo haga realmente útil.