Los LLM están haciendo viable la verificación formal de software a una escala mucho mayor
Los modelos de lenguaje grandes están empezando a hacer práctica la verificación formal de software a gran escala, por ejemplo generando enormes pruebas en Rocq/Coq que muestran que los binarios compilados no fallan para todas las entradas dentro de ciertos límites. Quienes comentan ven esto como un avance real para la seguridad y la fiabilidad, pero subrayan que solo verifica el código respecto de una especificación formal, no si esa especificación coincide con los requisitos reales y desordenados ni con la intención humana. El hilo explora preguntas más amplias sobre si los LLM están chocando con una “envolvente convexa” del conocimiento humano, su dificultad con la abstracción y la creatividad, y hasta dónde pueden llegar las pruebas automáticas dadas limitaciones fundamentales como el problema de la parada y la complejidad de los sistemas reales.
LLM, verificación formal y límites de capacidad
- Varios comentarios conectan los resultados de Anthropic con la idea de la “envolvente convexa”: los LLM interpolan dentro de la práctica matemática humana, pero pueden tener dificultades para inventar abstracciones fundamentalmente nuevas.
- Algunos sostienen que los LLM son fuertes para avanzar a través de demostraciones grandes y de estilo conocido, pero toparán con muros de complejidad sin mejores estrategias de abstracción y razonamiento.
- Otros responden que el aprendizaje por refuerzo en tareas más कठिनास podría dar lugar a estrategias de prueba emergentes mejores, así que el límite no está claramente fijado.
Estilo de demostración, abstracción y complejidad
- Las demostraciones generadas por agentes se describen como extremadamente verbosas, expandiendo cada detalle de ejecución de bajo nivel.
- Esto refleja cómo los LLM escriben código y pruebas: frágil, concreto, repetitivo, con modularización débil.
- Varias personas señalan que escalar la verificación requerirá ingeniería de demostraciones similar a la humana: abstracciones modulares, lemas reutilizables y mejores principios de razonamiento.
- Hay optimismo de que entrenar con buena estructura de pruebas podría mejorar la calidad general del código, especialmente en ecosistemas fuertemente tipados, funcionales y similares a Rust.
¿Qué se verifica realmente? Especificaciones, modelos y límites
- Se enfatiza mucho que “formalmente verificado” siempre significa “con respecto a una especificación/modelo formal”, que puede no coincidir con la intención real ni con el hardware real.
- Preocupa que los LLM puedan generar teoremas vacíos o mal especificados que aun así pasen el verificador, dando una falsa confianza.
- Algunos destacan límites clásicos (problema de la parada, teorema de Rice), mientras que otros subrayan que eso no impide probar propiedades útiles para programas específicos y no arbitrarios.
- Se traza una distinción entre verificación (el código coincide con la especificación), validación (la especificación coincide con las necesidades del mundo real) y la dificultad de esta última.
Flujos de trabajo, herramientas y niveles de abstracción
- Varios profesionales informan éxito usando LLM con Lean/Rocq, ESBMC, Alloy, Verus, etc., especialmente para pruebas de equivalencia (por ejemplo, reescrituras de C a Rust, optimizaciones frente a implementaciones de referencia).
- Verificar binarios compilados o LLVM IR se considera poderoso pero “brutal”, y requiere términos de prueba grandes, generados por máquina; justo ahí es donde la escala de los LLM brilla.
- Otros sostienen que la equivalencia con una referencia de oro es más manejable que las especificaciones completas y se adapta bien a sistemas heredados (por ejemplo, COBOL, C de Postgres).
Futuros declarativos vs realidad imperativa
- Un bando predice un cambio hacia lenguajes declarativos deterministas con ricos sistemas de tipos/efectos y verificabilidad integrada, haciendo de las pruebas formales el valor por defecto.
- Los escépticos dudan que un lenguaje declarativo suficientemente flexible y eficiente pueda evitar volverse efectivamente imperativo o recrear el problema del “compilador suficientemente inteligente”.
- La discusión toca DSL, fragmentos declarativos incrustados (SQL, LINQ, Inform7) y la semántica de sistemas distribuidos.
Pruebas, fuzzing, seguridad y adopción
- Muchos ven que la principal ganancia práctica hoy es: probar que las propiedades del fuzzing se cumplen para todas las entradas (sin fallos, idas y vueltas, leyes algebraicas), ofreciendo garantías más fuertes que el fuzzing por sí solo.
- Hay debate sobre si esto es “verdadera” verificación formal o solo pruebas con superpoderes, pero la mayoría coincide en que sigue siendo un salto sustancial para la seguridad y la robustez.
- Algunos están entusiasmados con rebajar la barrera de entrada a herramientas como Alloy, TLA+ y métodos formales en dominios críticos para la seguridad o de alta garantía; otros predicen una adopción limitada fuera de nichos “paranoicos”.
Preocupaciones socioeconómicas y de flujo de trabajo
- Varios desarrolladores describen a los LLM como algo que a la vez empodera (experimentación más rápida, más verificación) y desmoraliza (pérdida de oficio, miedo por la estabilidad profesional).
- Existe la preocupación de que la industria gaste los “dividendos de verificación” de los LLM en más velocidad y sistemas más descuidados, en lugar de en una garantía realmente mayor.
- Un tema recurrente: los LLM amplifican tendencias existentes: los equipos descuidados generan más descuido; los equipos cuidadosos pueden avanzar hacia verificación que antes era demasiado cara.