Leanstral 1.5: abundancia de demostraciones para todos

• En medio de la tendencia de acercar más la verificación formal al trabajo real de desarrollo, Mistral AI presentó Leanstral 1.5, un modelo Apache-2.0 para Lean 4
• El modelo activa solo 6B de un total de 119B parámetros y fue entrenado con preentrenamiento intermedio, ajuste fino supervisado y aprendizaje por refuerzo CISPO para aprender tanto redacción de demostraciones como trabajo sobre repositorios de código
• Registró 100% en miniF2F, 587/672 en PutnamBench, 87% en FATE-H y 34% en FATE-X, mostrando un desempeño sólido tanto en benchmarks de demostración matemática como en evaluaciones reales de ingeniería de pruebas
• En verificación de código real, demostró la complejidad temporal O(log n) de árboles AVL y, mediante un pipeline de Rust a Lean, encontró 11 bugs reales en 57 repositorios
• Se publicaron los pesos y la API gratuita leanstral-1-5, por lo que puede aplicarse de inmediato a ingeniería práctica de demostraciones como prueba de teoremas, depuración de pruebas y contribuciones a repositorios

---

Lanzamiento de Leanstral 1.5 y características del modelo

• Leanstral 1.5 es un modelo creado para realizar ingeniería de demostraciones en Lean 4
• Su licencia es Apache-2.0 y su escala es de 119B parámetros totales con 6B parámetros activos
• Mejora el rendimiento en verificación formal, por lo que puede usarse no solo en benchmarks matemáticos sino también en verificación de propiedades de código real
• Saturó miniF2F, resolvió 587 de los 672 problemas de PutnamBench y alcanzó 87% en FATE-H y 34% en FATE-X

Entrenamiento en 3 etapas con aprendizaje a partir de retroalimentación de pruebas

• El entrenamiento se compone de 3 etapas: preentrenamiento intermedio, ajuste fino supervisado y aprendizaje por refuerzo basado en CISPO
• En el aprendizaje por refuerzo se usaron dos entornos
  • Entorno multi-turno: el modelo recibe un enunciado de teorema para demostrarlo o refutarlo, y revisa iterativamente la prueba con base en la retroalimentación del compilador de Lean
  • Si la prueba compila, se considera exitosa; de lo contrario, el ciclo continúa hasta resolver el problema o agotar el presupuesto
  • Entorno de agente de código: edita archivos en un sistema de archivos sin procesar como lo haría un desarrollador, ejecuta comandos de bash y consulta en tiempo real metas, errores e información de tipos con el servidor de lenguaje de Lean
• El entorno de agente de código aborda tareas largas como completar pruebas parciales dentro de un repositorio, escribir lemas auxiliares y continuar trabajando incluso después de varias compresiones de contexto
• La corrección final se verifica contra la lista de teoremas objetivo usando el fork de SafeVerify de Mistral

Benchmarks de matemáticas e ingeniería de demostraciones

• En la evaluación se usaron miniF2F, PutnamBench, FATE-H/FATE-X y FLTEval
  • miniF2F es un benchmark de matemática formal que abarca desde problemas elementales hasta problemas de nivel IMO
  • PutnamBench está compuesto por 672 problemas de la Putnam Mathematical Competition
  • FATE-H y FATE-X son benchmarks de álgebra abstracta de nivel de posgrado y doctorado, respectivamente
  • FLTEval evalúa la dificultad de ingeniería de demostraciones a partir de pull requests reales del repositorio de Fermat’s Last Theorem
• En miniF2F logró 100% tanto en el conjunto de validación como en el de prueba
• En PutnamBench y FATE-H/X se comparó con Goedel-Architect, Seed-Prover 1.5 high y AxProverBase sin guías de prueba en lenguaje natural
• Rendimiento en FATE-H/X: {b:87,34}
• En FATE-H logró 87% y en FATE-X 34%, estableciendo un nuevo mejor resultado
• En PutnamBench resolvió 7 problemas más que Seed-Prover 1.5 high, con un costo de alrededor de 4 dólares por problema
  • La configuración high de Seed-Prover usa un presupuesto de 10 H20-days por problema y se estima que cuesta más de 300 dólares
  • Algunos demostradores mejor posicionados operan bajo otras condiciones, como recibir guías de prueba en lenguaje natural o costar entre 54 y 68 dólares por problema, como Aleph Prover

Escalabilidad con presupuestos largos de razonamiento y FLTEval

• En PutnamBench, Leanstral 1.5 muestra un aumento suave y monótono del rendimiento Pass@8 a medida que se incrementa el presupuesto de tokens
• En experimentos que elevaron el presupuesto por intento de 25k a 4M tokens, la cantidad de problemas resueltos aumentó así
  • 50k tokens: 44 problemas
  • 200k tokens: 244 problemas
  • 1M tokens: 493 problemas
  • 4M tokens: 587 problemas
• El hecho de seguir razonando, editando archivos y corrigiendo durante millones de tokens sin interrumpirse se tradujo en mejoras de rendimiento
• FLTEval también se publicó como open source completo
• En FLTEval, Leanstral 1.5 elevó pass@1 de 21.9 a 28.9 y pass@8 de 31.9 a 43.2
• El pass@8 de 43.2 supera el 39.6 de Opus 4.6 y cuesta aproximadamente una séptima parte
• También mostró mejor rendimiento que modelos open source entre 3 y 10 veces más grandes

Casos reales de verificación de código

• Demostración de complejidad temporal de árboles AVL

  • Un árbol AVL es un árbol binario de búsqueda autoequilibrado que mantiene altura O(log n) mediante rebalanceo durante inserciones y eliminaciones
  • Leanstral 1.5 verificó sobre una implementación real que inserción y eliminación son O(log n)
  • Esta tarea requirió inducción estructural que reflejara la estructura recursiva del árbol, seguimiento temporal basado en mónadas y un análisis exhaustivo de casos sobre la ruta de rebalanceo
  • La prueba avanzó a lo largo de más de 2.7 millones de tokens y 22 compresiones de contexto
  • Leanstral desplegó sistemáticamente cada capa de la mónada TimeM para exponer cálculos mezclados con el flujo de control
  • Para la inserción, estableció un límite de 48 pasos por unidad de altura y un término constante cercano, conectando la altura con el tamaño del árbol mediante una relación logarítmica

• Detección de bugs en código Rust

  • El experimento de detección de bugs consistió en un pipeline donde Aeneas convierte código Rust a Lean y Leanstral infiere la intención del usuario en el código para generar propiedades de corrección
  • Leanstral intenta demostrar cada propiedad 4 veces y, si todas fallan, intenta demostrar su negación otras 4 veces
  • En 57 repositorios se marcaron 47 propiedades violadas, de las cuales 11 apuntaban a bugs reales
  • De esos bugs reales, 5 no habían sido reportados previamente en GitHub
  • Se encontró un caso en la función de signo de zigzag decoding de la librería datrs/varinteger
  • Cuando la entrada es Std.U64.MAX, la expresión (value + 1) provoca overflow
  • En modo debug ocurre un crash y en modo release se produce corrupción silenciosa de datos
  • Este edge case es uno que las pruebas comunes y el fuzzing pueden pasar por alto fácilmente

Despliegue y uso

• Los pesos están publicados en Hugging Face
• El endpoint de API gratuito se ofrece en la tarjeta del modelo con el nombre leanstral-1-5
• Mistral Vibe es el entorno recomendado
• El procedimiento inicial consiste en configurar Mistral Vibe, instalar Leanstral 1.5, ejecutar el agente, instalar opcionalmente Lean LSP MCP e iniciar el trabajo de demostración
• Se recomienda instalar Lean LSP MCP agregándolo a ~/.vibe/config.toml
• Si no hay un servidor MCP existente, puede ser necesario eliminar mcp_servers = []
• Leanstral puede usarse para resolver teoremas, depurar pruebas y contribuir a repositorios

[GN⁺]

Opiniones de Hacker News

• La crítica de que a Mistral le cuesta competir con los modelos grandes es válida, pero creo que en la práctica se está enfocando en ofrecer funciones específicas con alta calidad en modelos pequeños
  Uso Mistral para tareas como OCR o análisis de archivos, y si dejo 100 dólares en la cuenta, funciona durante un año sin preocuparme por el volumen de solicitudes
  El costo es ínfimo, así que aunque no pueda competir con Opus 4.8, sigue teniendo bastante valor

  • Me pregunto qué tan competitivo es realmente en OCR
    Calidad aceptable a bajo precio parece más un nicho que pagar 10 veces más por la máxima calidad para reducir errores después
  • Esos tontos europeos están optimizando para hacer buenos productos, no para ganar la mayor cantidad de dinero posible /s
  • No sé si “procesar documentos de todo un año por menos de 100 dólares al año” sea tan excelente como parece. Al menos desde la perspectiva de la competitividad europea, Mistral estaría fijando un techo de ingresos demasiado bajo
    El OCR ya es casi un commodity, y también se ofrece de forma básica en modelos open source o en lugares como AWS
    Además, con una etiqueta de 100 dólares al año es difícil generar lealtad, y como no hay costo de cambio, si aparece un precio más bajo los clientes pueden irse de inmediato
    Si una herramienta barata y fácil de replicar no tiene lock-in de clientes, se parece más a una función que a un negocio
    Para el comprador está bien, pero si se quiere que una empresa europea compita a largo plazo con rivales globales por capacidad de producto, parece una mala estrategia

• El trabajo en sí es bueno, pero el ejemplo de detección de bugs me pareció raro
  Decían que en la función sign del decodificado zigzag, con la entrada Std.U64.MAX, (value + 1) hace overflow y provoca un crasheo en modo debug y corrupción silenciosa en modo release; no sé si esto puede llamarse una condición de borde que las pruebas “normalmente pasan por alto”
  Unas malas pruebas lo pasarían por alto, pero una persona cuidadosa o un sistema de programación basado en aprendizaje automático suelen ser bastante buenos para pensar “debería probar valores extremos”. Sobre todo si es código que parsea entradas de usuario
  Me pregunto si encontraron un bug más interesante pero eligieron este ejemplo porque era difícil explicarlo rápido

  • En particular, la parte de que “también se le escapa al fuzzing” es extraña. El fuzzing que he visto normalmente explora valores de borde de forma deliberada
    Para una biblioteca de codificación como esta, el fuzzing sería una expectativa básica de código aceptable, y casi seguro lo habría encontrado en segundos
    De hecho, hice una prueba round-trip muy simple con proptest y en menos de un segundo salieron decenas de fallas y el siguiente resultado:
    thread 'signed_round_trip' (50528) panicked at tests/test.rs:72:1:
Test failed: attempt to multiply with overflow.
minimal failing input: value = 4611686018427387904
successes: 2
local rejects: 0
global rejects: 0
  • Quizás sea difícil decir que “normalmente se pasa por alto”, pero como realmente existía, sí es un bug que a veces se pasa por alto
    La ventaja de usar Lean es que reduce la necesidad de elegir de forma inteligente qué ejemplos probar
  • Esto es aseguramiento de calidad básico. Si las pruebas pasan por alto algo así, su utilidad sería mucho más limitada de lo que normalmente esperamos
    Me da curiosidad el perfil de los autores
  • Esto es simplemente publicidad basura
    Todos los sistemas de pruebas basadas en propiedades inventados alrededor de 1980 exploran valores de borde
    Las pruebas reales pueden ser difíciles por la semántica de C y C++, o la falta de ella. Porque se permite que el compilador diga “prueba aprobada” para cualquier entrada que lleve a comportamiento indefinido

• En medio del texto aparecen comparaciones con varios LLM de frontera, pero todos son modelos de hace medio año
  Me dio bastante risa porque suena a “nuestro nuevo modelo es mejor que modelos chinos de hace 3 generaciones”

  • Este es un modelo de 6 mil millones de parámetros, así que es una categoría totalmente distinta. De hecho, genera más expectativa como “modelo de lenguaje pequeño de frontera”
  • De acuerdo, pero el simple hecho de tener pesos abiertos y ser relativamente pequeño ya alcanza para el titular. Este modelo corre bastante bien

• La biblioteca es https://github.com/datrs/varinteger
  El mismo problema ya había sido reportado en ese repositorio una semana antes de que se publicara el paper, así que probablemente sea esa: https://github.com/datrs/varinteger/issues/8
  No sé si esta persona es empleada de Leanstral o si Leanstral simplemente tomó este issue
  La biblioteca es pequeña, sus pruebas son sorprendentemente deficientes y casi no se ha tocado en 8 años: https://github.com/datrs/varinteger/blob/master/tests/test.r...
  Las descargas parecen bajas, alrededor de mil por día: https://crates.io/crates/varinteger
  Así que no parece un éxito tan grande como para presentarlo como único ejemplo. La detección automática sí es útil, pero no sé si sea un logro destacable en este subcampo
  Nunca he usado un LLM para escribir pruebas formales, pero como los datos de entrenamiento tienden a ser escasos, no me sorprendería que sea más tosco que un modelo general de programación
  Como referencia, https://crates.io/crates/varinteger muestra https://github.com/mafintosh/varinteger-rs, pero esa dirección redirige a https://github.com/datrs/varinteger, así que, pese a las apariencias, parece ser la misma biblioteca

  • El problema de las pruebas formales es que a veces cuesta transmitir su valor
    El punto no es encontrar bugs, sino demostrar que ciertos tipos de bugs no existen bajo ciertas suposiciones
    Pero esa historia es difícil de vender, así que el marketing suele terminar yéndose por el lado de “encontramos este bug”

• ¿Puede ser útil incluso para alguien que no sabe nada de Lean? Quiero verificar el software en el que estoy trabajando, pero no tengo experiencia en verificación formal
  Me pregunto si se pueden obtener resultados aprovechables solo con la especificación, el código y un tiempo de aprendizaje limitado

  • Hay que entender la parte que se quiere demostrar, pero no hace falta entender todo el proceso de prueba
    Se parece más a leer tipos de Haskell que a matemáticas; da la sensación de que solo toma mucho vocabulario prestado de las matemáticas
  • Si se lee la sección “Bug Discovery: Finding Hidden Flaws” del artículo, parece que empezaron solo con código Rust y usaron el modelo para encontrar problemas en Rust open source
    Tal vez también se pueda recibir ayuda conversando para que escriba código Lean orientado a verificar una aplicación, aunque no estoy seguro
  • Como mínimo, hay que entender qué teorema se quiere demostrar sobre el código y cómo expresarlo en Lean
    Si no, no se puede verificar la salida
    Mecánicamente, puede haber demostrado alguna proposición comprobada como correcta, pero si no sabes qué significa esa proposición ni si abarca lo que realmente quieres verificar, no tiene sentido
  • Partiendo de no saber nada de Lean4, en unos 6 meses llegué al punto de hacer la mayor parte de mi programación en Lean4, y este proceso se aceleró mucho gracias a la asistencia de IA
    Es sorprendente lo consistentemente fluidos que son los modelos en Lean4. No solo los modelos de frontera, también modelos locales pequeños; parece que los LLM simplemente entienden bien Lean4
    Todavía me falta para llamarme experto en Lean4, pero ahora no necesito necesariamente asistencia para crear programas útiles
    Poder confiar en partes que no entiendo del todo, incluso con muy poco conocimiento, acelera muchísimo el aprendizaje. Obtener programas en los que se puede confiar aun con conocimiento incompleto es práctico y también motivador
    Siento que el límite no lo marcan todos los pasos intermedios de la prueba, sino la parte del lenguaje con la que describes tus axiomas y la superficie de tus proposiciones. Con el tiempo, para hacer más cosas habrá que entender más, pero en cierto sentido se puede trabajar de forma segura en un nivel N+1
    Lean4 también es un lenguaje de programación disfrutable, aparte de su rol como demostrador de teoremas, y además es sorprendentemente rápido
    Lo estoy usando conectado a io_uring, y en muchos casos es mucho más rápido que C++/libuv o Rust/Tokio
    A veces, cuando aparecen colas grandes en métricas como la latencia p99.99, hace falta ajustar cosas como cambiar números a ancho fijo, pero C++ y Rust también requieren ajustes

• Me parece interesante que estén impulsando Lean 4 para verificación formal
  Pensaba que ese terreno era más de Isabelle/HOL y TLA+
  Habría esperado, al menos, un modelo entrenado para usar los tres. Para la derivación hacia adelante en álgebra lineal, Isabelle/Isar también parece mejor; ¿alguien puede explicarlo?

  • Es cierto que Lean tuvo menos adopción en verificación de software que Isabelle o Rocq, el antiguo Coq
    En este campo, incluso Agda se ha usado más
    Dicho eso, Lean está ganando bastante impulso como alternativa, sobre todo por su capacidad como lenguaje funcional de propósito general
    Personalmente, me parecen más prácticos los enfoques basados en lógica de Hoare o lógica de separación, que facilitan alinear requisitos y especificaciones. Me gustan Dafny y F*

• Me pareció divertido que en el anuncio de Twitter los desarrolladores mencionaran de pasada Le Chaton Fat
  Independientemente de si realmente estuvieron involucrados en Le Chaton Fat, parece que pronto saldrá un verdadero modelo “generalista grande” nuevo
  Como lo mencionaron directamente incluso después del revuelo mediático, genera expectativa. Ojalá el nombre sea más creativo que “Large 4”

• Se puede probar Leanstral 1.5 en la versión más reciente de OpenATP
  OpenATP es un paquete Python y una CLI open source para demostradores automáticos de teoremas de tipo agente, con soporte básico para ejecutarse localmente en Docker o de forma remota en un sandbox de Modal
  GitHub: https://github.com/henryrobbins/open-atp
  Docs: https://open-atp.henryrobbins.com