RefactorProof: las demostraciones de los LLM se rompen tras refactorizar el código

Los benchmarks de generación verificable de código suelen comprobar la demostración sobre una única implementación fija. Los autores de RefactorProof quisieron saber qué ocurre si se reescribe la implementación conservando el comportamiento. A partir de las 185 tareas de VERINA que compilan en su entorno fijado, construyeron 458 variantes certificadas por Lean. La especificación y la demostración verificable no cambiaron ni un byte. El resultado: en las refactorizaciones estructurales, las demostraciones dejan de pasar la verificación de forma masiva. Entre las demostraciones de referencia de VERINA, la proporción de supervivientes (task-normalized structural PSR) es del 4,3%; entre los demostradores LLM especializados, del 13,3–26,8%.

Cómo funciona la prueba de fragilidad

La idea es simple y cruda. Una demostración formal está ligada al texto concreto del programa: nombres, orden de las definiciones, estructura de las expresiones. Si un desarrollador extrae una función, cambia la forma de un cálculo o renombra una variable, lógicamente no cambia nada, pero la demostración en Lean puede dejar de compilar. En el desarrollo real se refactoriza constantemente, así que la pregunta de si la demostración sobrevivirá a un cambio es práctica.

VERINA aporta demostraciones de referencia solo para 46 tareas, y todas pertenecen a la división básica. Por eso los autores basan las principales comparaciones entre modelo y referencia en 21–25 tareas cortas y no recursivas, elegidas para que todos los participantes partan del mismo terreno. Es una muestra reducida, y el alcance de las conclusiones debe leerse con esa salvedad.

Las máquinas son frágiles, pero los humanos lo son más

El giro inesperado es que las demostraciones de los modelos resultaron más robustas que las de referencia. En tareas comparables, la proporción global de demostraciones no modificadas que sobreviven es mayor en los modelos que en los artefactos de VERINA. Los intervalos de confianza del 95% de los tres modelos no incluyen el cero.

• DeepSeek-Prover-V2-7B: +15,6 puntos respecto a la referencia
• Goedel-Prover-V2-32B: +18,8 puntos
• Goedel-Prover-V2-8B: +20,3 puntos

El orden se mantiene al excluir las variantes T1, que las superan absolutamente todas, al agregar equilibrando por familias de refactorización y con reglas alternativas de selección de la demostración válida aplicables en la práctica. La causa probable es que las demostraciones de referencia están escritas para una forma concreta del código y muy atadas a ella, mientras que los modelos suelen producir demostraciones más directas y menos dependientes de los detalles de la construcción. Es una hipótesis: los autores no demuestran ese mecanismo.

Que se rompa no significa que arreglarlo sea caro

La principal salvedad del artículo se refiere al coste de la rotura. Las correcciones predefinidas de un solo identificador arreglan 51 de las 54 caídas estructurales elegibles de las demostraciones de referencia y 58 de las 85 caídas elegibles de las demostraciones de los modelos. Es decir, gran parte de la «fragilidad» se elimina con un arreglo barato, y en las demostraciones de referencia se arregla casi todo. Para los modelos el panorama es peor: alrededor del 68% frente al 94%.

Por eso RefactorProof mide únicamente la estabilidad de la demostración no modificada ante la refactorización. No evalúa el coste de mantener la demostración una vez rota, y los autores lo subrayan de forma explícita.

Parámetros clave del estudio

• Benchmark: RefactorProof, derivado de VERINA
• Tareas de origen: 185 (compilan en el entorno fijado de Lean)
• Variantes certificadas: 458
• Demostraciones de referencia de VERINA: 46 tareas, solo la división básica
• Muestra comparable: 21–25 tareas cortas y no recursivas
• PSR estructural de las demostraciones de referencia: 4,3%
• PSR estructural de los demostradores especializados: 13,3–26,8%
• Modelos evaluados: DeepSeek-Prover-V2-7B, Goedel-Prover-V2-32B, Goedel-Prover-V2-8B
• Reparación con la corrección de un solo identificador: 51/54 en las de referencia, 58/85 en las de los modelos
• Sede: NeurIPS 2026 Workshop on AI for Verifiable Coding; categorías cs.AI, cs.LO, cs.SE

Qué cambiar en la práctica

Los equipos que construyen pipelines del tipo «el LLM escribe el código y la demostración, Lean verifica» reciben una señal clara: comprobar sobre una única implementación fija sobrestima la fiabilidad. Añada al CI variantes refactorizadas del programa y ejecute la demostración contra ellas. Si la demostración falla, pruebe primero correcciones automáticas baratas de identificadores: según los datos del trabajo, resuelven una proporción considerable de los casos.

Al evaluar modelos prover, no se fije solo en la proporción de tareas resueltas, sino también en la supervivencia de las demostraciones cuando cambia el código. Para los autores de benchmarks, la conclusión también es directa: hay que medir tanto la estabilidad como el coste de reparación. Este segundo indicador todavía no existe en RefactorProof.