La IA reescribe CPython en Lean y descubre 418 fallos en Python
Formalizing CPython
Un proyecto usó agentes de IA para copiar las funciones de CPython en Lean, línea por línea, y verificar cada prueba con un comprobador automático. El resultado: 613.318 líneas de Lean, 18.898 teoremas y 4.071 funciones validadas por un segundo agente independiente. El proceso destapó 418 informes de errores en Python, de los cuales unos 55 pueden provocar caídas o corrupción de memoria con código Python normal.
Lo más difícil no fue conseguir que los agentes de IA escribieran pruebas, sino conseguir pruebas que realmente significaran algo.
- debugnik
¿No sería más productivo gastar los tokens en añadir anotaciones ACSL para verificar CPython con Frama-C? Verificarías el runtime real en lugar de una traducción hecha por IA, y las correcciones podrían contribuirse directamente upstream.
- anewhnaccount2
El mismo enfoque para la stdlib de Julia: https://discourse.julialang.org/t/formalizing-julia-in-lean-...
- jakobnissen
Creo que este enfoque para la caza de bugs es súper prometedor (obviamente, encuentra un montón de bugs). El problema a largo plazo es cómo se puede hacer este tipo de caza de bugs de forma rutinaria, por ejemplo, como parte de una suite de tests. El enfoque que han tomado estas personas, el mismo que cuando lo hizo la gente de Julia, no es realmente automatizable, porque requiere mucho trabajo tanto humano como de agentes de IA.
Supongo que a largo plazo tiene que estar integrado en el lenguaje, para evitar que el código y las pruebas en Lean se desvíen. Es decir, podrían ser propiedades opt-in que se escriben junto al código y que luego se comprueban en la suite de tests. Muy similar a las comprobaciones normales del compilador, salvo que más expresivas y costosas, y hechas solo en tiempo de test.
- tomtom1337
Estoy confundido en algunos puntos, ¡me encantaría que alguien pudiera aclararlos!
- si la reescritura en Lean ocurre línea por línea, ¿cómo pueden las dos implementaciones diferir en su resultado (Paso 2)?
- ¿cómo sabe este enfoque "algo que siempre debería ser verdad" en el Paso 3 (es la inteligencia del LLM "adivinando"?).
- erfgh
¿Alguien lee artículos escritos por IA? Esta es una pregunta seria.