Claude demuestra que el código de 123 bibliotecas de código abierto nunca fallará
LLMs are making formal software verification feasible at a much larger scale
En colaboración con Theorem, Anthropic utilizó Claude para generar pruebas formales de seguridad a nivel de código ensamblador RISC-V en 123 bibliotecas de código abierto de OSS-Fuzz. Las pruebas, que suman unos 180 millones de líneas de Rocq, garantizan que los programas siempre terminan sin errores de memoria ni fallos de aserción para cualquier entrada de hasta 64 MB. Además, Claude encontró y corrigió errores que habían pasado desapercibidos durante años, incluso con billones de ejecuciones de fuzzing.
Claude demostró que estos programas siempre terminan normalmente sin activar errores de seguridad de memoria ni fallar aserciones, para cada entrada menor de 64 MB y cada respuesta y diseño de memoria modelados del sistema operativo Linux.
- yazaddaruvala
Creo que en realidad ocurrirá algo más bien lo contrario. Los LLM no verificarán formalmente el código de estilo imperativo generado por LLM. Nosotros (incluido el desarrollo agéntico) pasaremos de los lenguajes imperativos, saltándonos los funcionales, y nos moveremos hacia lenguajes declarativos deterministas.
Probablemente, una proliferación de lenguajes experimentales, todos más o menos similares a Typescript para SQL, con operadores significativamente más matizados para capturar de forma concisa los mismos resultados que los lenguajes imperativos.
Se compilarán para poder ejecutarse con buen rendimiento en desarrollo de videojuegos o incluso para el kernel de Linux (como si Linus fuera a aceptarlo alguna vez, jaja), pero además podrán ejecutarse en motores de ejecución distribuidos con, efectivamente, un espacio de memoria compartido, etc.
Permite artefactos significativamente más concisos. Menor probabilidad de alucinación, menos tokens de salida, menos iteraciones de bucles de pensamiento y lo bastante conciso para que los humanos lo revisen (en los dominios que lo necesiten).
Además de eso, sintaxis adicional tipo teoremas para limitar drásticamente la capacidad de las funciones, etc., probablemente algún tipo de sistema de efectos de más alto nivel para la verificación. Usado para muchas cosas como "compilación en tiempo constante para funciones criptográficas", y también "garantizar el cumplimiento ACID" para escrituras y lecturas en un contexto local, y cosas como "garantizar entrega única" para funciones en un motor de ejecución distribuido.
Llegados a ese punto, cada programa estará verificado formalmente por defecto. Podrías pensarlo como AdaErlangSQL+++
- jaykru
Del apéndice [0]: "Las pruebas escritas por agentes son igual de 'buenas' que cualquier otra prueba del mismo teorema, en el sentido de que demuestran el teorema de equivalencia. Sin embargo, está por verse si los agentes pueden escalar este estilo de prueba verboso directamente a programas más complejos. La experiencia de otros proyectos de verificación basados en agentes, como MachCSL, sugiere que la respuesta podría ser no: los agentes chocan con un muro de complejidad con el estilo de prueba verboso, y escalar requiere que las pruebas se estructuren en torno a mejores abstracciones modulares y principios de razonamiento. Si ese es el caso, ¿cómo podemos ayudar a los agentes a descubrir e introducir las abstracciones correctas para reducir esta complejidad? ¿Requiere esto la aportación de ingenieros de pruebas expertos, o podemos extraer principios comunes que guíen a los agentes a descubrir buenas abstracciones que permitan pruebas escalables?"
Algunos matemáticos han observado un patrón similar en las recientes oleadas de pruebas de LLM, lo que les ha llevado a sugerir que los LLM chocarán contra un muro en capacidad matemática justo más allá de la envolvente convexa de la matemática humana. El tipo de pruebas que se hacen en verificación formal es una prueba de tornasol bastante interesante para el razonamiento de los LLM, ya que los sistemas considerados no están necesariamente en la distribución (compárese con las matemáticas, donde los "sistemas" y estructuras con los que se trabaja, y las pruebas sobre ellos, aparecen en miles de libros individuales), así que las ventajas en conocimiento amplio de dominio que tienen los LLM preentrenados sobre los humanos no te compran realmente mucho. En mi opinión, esta observación […]
- malisper
Para los escépticos, he tenido un éxito decente usando verificación formal para mi reescritura en Rust de Postgres. Escribí un compilador que puede traducir tanto código Rust como C a Lean. Una vez que esas dos funciones están en Lean, hago que un LLM escriba una prueba en Lean de que se comportan de forma idéntica.
Hasta ahora, he demostrado que alrededor del 12% del código se comporta igual cuando se ejecuta en un solo hilo. Eso equivale a aproximadamente 70k líneas de código C. Esto ha encontrado diferencias de comportamiento muy menores, como que las operaciones de punto flotante entre plataformas pueden producir resultados distintos.
Estoy trabajando en averiguar cómo escalar esto, pero no veo ninguna limitación fundamental que impida escalarlo más.
- fedupnow
Tengo 35 años, estoy jodido si se salen con la suya. No voy a ir a los oficios, dejé la construcción a los 27 porque amaba demasiado la programación. Quería matarme prácticamente todos los días trabajando en el sector de la construcción. Me bebí mis veintes porque era horrible. Llevo años sobrio ahora enteramente gracias a la programación y a amar de verdad lo que hago. Pero esta empresa me está robando eso, de muchas maneras distintas.
Invertí un montón de mi vida y todos mis ahorros en esta transición. Ahora me gritan todos los días que me vaya a ser electricista porque Anthropic afirma que van a resolver el problema de la parada de alguna manera indirecta; ni siquiera tienen que hacer lo que afirman. Solo tienen que convencer al 20% del sector de que lo harán, y tipos como yo nunca tendrán la oportunidad de trabajar el tiempo suficiente para jubilarse.
Realmente no creo que lo consigan, pero si lo hacen, voy a acabar sin hogar programando desde la biblioteca pública porque no voy a empezar de cero otra vez.
- sestep
He estado haciendo esto en el trabajo las últimas semanas. Es extremadamente potente poder hacer que un agente abra un PR con algunos experimentos que muestran que hace alguna función más rápida usando SIMD o CUDA, y fusionarlo con confianza porque el PR tiene una prueba en Rocq de que es conductualmente equivalente a la implementación original.
- pinevale
¿Verificación formal contra qué?
¿La elusiva especificación formal con cobertura del 100% que abarca cada entrada prevista e imprevista, los intereses de cada parte interesada y cada posible comportamiento del usuario? ¿En la era del vibecoding? No, la página tiene la decencia de reconocer que eso no existe.
Al final, se conforman con encontrar fallos con un fuzzer convencional, arreglar los fallos y luego... ¿escribir una prueba formal de que el fallo está arreglado? Eso parece... bastante inútil, ¿no? ¿Me estoy perdiendo algo aquí?
- Olscore
Construir una casa tiene tres capas:
1. Visión: lo que queremos (nuestra intención)
2. Plano: la especificación que escribimos (nuestro diseño)
3. Inspección: comprobar lo que construimos contra el plano (las pruebas)
Esta investigación hace que la inspección sea casi perfecta. Pero una inspección solo comprueba el plano, no nuestra visión, así que una casa construida a partir del plano equivocado puede aun así pasar una inspección perfecta. La otra mitad es asegurarse de que el plano coincide con nuestra intención y se mantiene así mientras los agentes construyen. Estoy trabajando en eso, así que creo que esto es complementario:
- passive
Esto parecía una posibilidad alta, pero dado que nuestra adopción de los LLM en el software hasta ahora ha consistido mayormente en tirar por la borda las buenas prácticas, soy escéptico de que nos lleve a una verificación ampliada.
Es como Bezos hablando de que vamos a tener semanas laborales de 3 días mientras hace que sus empleados meen en una botella.