Las pruebas de Lean para código generado por IA fallan tras refactorizaciones en el 13-27% de los casos

Cuando un modelo de lenguaje escribe código y le adjunta de inmediato una prueba matemática formal de su corrección en Lean, el resultado parece sólido como una roca: el programa garantiza hacer exactamente lo que se le pide. Pero todas las pruebas existentes verifican el resultado contra una sola versión fija del código. En el desarrollo real, el código se reescribe constantemente: la lógica repetida se extrae a una función separada, se reordenan operaciones, se invierten condiciones, mientras el comportamiento del programa permanece inalterado. La pregunta es si la prueba antigua sobrevive a ese tipo de reestructuración, aunque el significado del código no haya cambiado.

Los autores del trabajo proponen una metodología llamada RefactorProof para medir exactamente esto. Tomaron 185 problemas del conocido benchmark VERINA (que verifica tanto el código como las pruebas en Lean) y aplicaron a cada problema cinco tipos de reescrituras mecánicas y totalmente automáticas: extraer un fragmento de lógica a una función separada, intercambiar operandos en operaciones conmutativas, invertir condiciones, etc. Para cada reescritura, se demostró por separado mediante Lean que el comportamiento del programa no había cambiado. El resultado fueron 458 variantes de código verificadas. Luego, cada variante se emparejó con la prueba original (idéntica byte por byte) para ver si Lean seguía aceptándola.

Qué resultó frágil y qué no

Las pruebas de referencia que los autores de VERINA escribieron a mano para 46 problemas sobrevivieron a la refactorización casi sin pérdidas: una tasa de fallos de solo el 4,3%. Pero eso no significa que las pruebas manuales sean inherentemente más robustas: esos 46 problemas son los más sencillos del benchmark, con una longitud mediana de código de una sola línea, y solo el 6,5% de ellos son recursivos.

Las pruebas generadas por modelos especializados en demostración de teoremas —DeepSeek-Prover-V2-7B y dos versiones de Goedel-Prover-V2 (8B y 32B)— fallaron mucho más a menudo: las tasas de fallo oscilaron entre el 13,3% y el 26,8%. Pero al comparar los modelos con la referencia en un conjunto de problemas idéntico y comparable, el panorama se invierte: las pruebas de los modelos sobreviven a la refactorización con más frecuencia que las de referencia —15,6 puntos más para DeepSeek-7B, 18,8 puntos para Goedel-32B y 20,3 puntos para Goedel-8B—. La diferencia es estadísticamente significativa en los tres casos.

Por qué unas pruebas se derrumban y otras resisten

Los investigadores identificaron un mecanismo concreto detrás de esta resiliencia. Las pruebas de referencia suelen comenzar con el comando `unfold`, que despliega la definición de la función directamente en el texto. Las pruebas de los modelos, en cambio, suelen comenzar afirmando explícitamente que una llamada a función y su cuerpo son iguales mediante la táctica `rfl` (un llamado "puente definicional"), y luego demuestran el resto de forma automática.

Cuando el código se traslada a una función separada (extracción de lógica), ese "puente" resulta ser mucho más duradero: a nivel de tareas, las pruebas con puente sobreviven en 6 de 6 casos, mientras que las demás estrategias solo lo logran en 6 de 31. Pero este recurso tiene una contrapartida: si la reescritura cambia sustancialmente el cuerpo de la función (y no solo su ubicación), un puente anclado al texto específico de ese cuerpo deja de pasar la comprobación de tipos; esas pruebas solo sobreviven 0 de 3 veces, frente a 17 de 19 en pruebas más generales, no atadas a una formulación concreta.

Un fallo no es una catástrofe

La principal conclusión práctica es que una prueba que deja de pasar la verificación tras una refactorización no implica necesariamente una reescritura costosa. Los investigadores lo comprobaron directamente: tomaron las pruebas fallidas e intentaron corregirlas con un único cambio puntual sencillo: renombrar un identificador. De 54 fallos elegibles en pruebas de referencia, se corrigieron 51 de esta forma; de 85 fallos en pruebas generadas por modelos, se corrigieron 58.

Para los equipos que confían en la generación verificable de código por IA, la conclusión es sencilla: el mero hecho de que una prueba deje de pasar tras una refactorización no es motivo de pánico ni una señal de que un modelo sea, en principio, peor generando pruebas. Es más bien una señal de que conviene integrar en el pipeline de verificación una comprobación automática y una reparación ligera de pruebas tras cualquier cambio de código, en lugar de considerar el fallo como un veredicto definitivo sobre la calidad del modelo.