🤖 AI

P $^{3}$ : Joint Program-and-Proof Planning for Verified Code Generation

El artículo presenta $P^3$ , un flujo de trabajo agéntico basado en LLM que planifica conjuntamente programas y sus pruebas formales para superar las ineficiencias de la generación secuencial, logrando un rendimiento de vanguardia y reducciones de costos significativas en los bancos de pruebas de generación de código verificado, incluyendo un nuevo conjunto de datos derivado de repositorios llamado Lean4Commit0.

Autores originales: Zenan Li, Ziran Yang, Peiyang Song, Zhaoyu Li, Kaiyu Yang

Publicado 2026-08-11

📖 8 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Zenan Li, Ziran Yang, Peiyang Song, Zhaoyu Li, Kaiyu Yang

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que le estás enseñando a un robot superinteligente a escribir una historia. Le das al robot una consigna y este te devuelve un relato. Pero aquí está el truco: no quieres solo una historia; quieres una historia que esté matemáticamente garantizada como verdadera, sin agujeros en la trama, sin magia que rompa las leyes de la física y sin personajes que desaparezcan sin explicación. Este es el mundo de la generación de código verificado. Es un rincón de la informática donde le pedimos a la Inteligencia Artificial no solo que escriba software, sino que escriba software que venga con su propia "prueba de corrección": un certificado matemático que dice: "Prometo que este código hará exactamente lo que dije que haría, para cada situación posible".

Durante mucho tiempo, la forma estándar de hacer esto fue como una danza de dos pasos: primero, el robot escribe el código (la historia), y luego, un equipo separado de lectores de pruebas de robots intenta comprobar si la historia tiene sentido. Si los lectores de pruebas encuentran un agujero en la trama, devuelven la historia al escritor para que la arregle. El escritor parchea la historia, la envía de vuelta y el ciclo se repite. Pero este artículo sugiere que esta danza de "escribir y luego comprobar" es a menudo torpe e ineficiente. Es como intentar construir un puente y luego, después de haberlo terminado, darse cuenta de que olvidaste poner las vigas de soporte, obligándote a demolerlo y reconstruirlo. Los autores de este artículo proponen una nueva forma: en lugar de escribir el código y luego la prueba por separado, el robot debería planificar el puente entero —tanto la carretera como los soportes— al mismo tiempo, asegurando que encajen perfectamente desde el primer boceto.

El Problema: La Trampa del "Escribir-luego-Comprobar"

El artículo, titulado "Joint Program-and-Proof Planning for Verified Code Generation" (Planificación Conjunta de Programa y Prueba para la Generación de Código Verificado), aborda un cuello de botella frustrante en la forma en que la IA escribe software verificado. Actualmente, la mayoría de los sistemas siguen un flujo de trabajo de "primero el programa, luego la prueba". Es como pedirle a un chef que cocine una comida compleja y luego, una vez que la comida está en la mesa, pedirle a un crítico gastronómico que demuestre que los ingredientes estaban frescos y el método de cocción era seguro. Si el crítico encuentra un problema (como pollo crudo), el chef tiene que volver atrás, recocer el plato y esperar que al crítico le guste esta vez.

Los autores argumentan que este enfoque secuencial es defectuoso. Cuando la IA se compromete a escribir el código primero, puede elegir una estructura que parezca bien en la superficie pero que sea una pesadilla de demostrar. Por ejemplo, imagina que la IA escribe un programa para encontrar el número más grande en una lista. Podría elegir un método que sea corto y rápido de escribir, pero que requiera una regla matemática increíblemente compleja y oculta para demostrar que funciona. Una vez escrito el código, la IA se queda atrapada: tiene que inventar una prueba superdifícil para que coincida con ese código específico o destruir el código y empezar de nuevo. Esto conduce a mucho tiempo, dinero desperdiciado y "bucles de reparación" donde la IA sigue parcheando el código y la prueba, pero nunca terminan de encajar.

La Solución: P3 (El Planificador "Mano a Mano")

Para solucionar esto, los investigadores introducen P3, un nuevo flujo de trabajo donde la IA actúa como un maestro arquitecto que dibuja el plano tanto del edificio como de la inspección de seguridad antes de colocar un solo ladrillo.

En lugar de saltar directamente a escribir el código, P3 crea primero un plan unificado. Este plan es un boceto de alto nivel que responde a dos preguntas a la vez:

¿Cómo funcionará el código? (El "Esbozo del Programa")
¿Cómo demostraremos que funciona? (El "Esbozo de la Prueba")

El plan decide la estructura de la solución. Elige la "forma" adecuada para el código (como elegir entre un bucle recursivo o un fold) y simultáneamente elige las reglas matemáticas correspondientes (invariantes) necesarias para demostrar que esa forma es segura. Es como decidir: "Construiremos un puente usando cables de suspensión, por lo tanto, nuestro plan de prueba debe incluir la comprobación de la tensión de esos cables".

Una vez que el plan compartido está fijado, la IA entonces "elabora" los detalles. Escribe el código real y la prueba real, pero solo está rellenando los huecos de un plano previamente acordado. Si la prueba falla, la IA sabe exactamente dónde mirar porque la estructura ya fue decidida. Si el plan es malo (por ejemplo, el diseño del puente es imposible), la IA vuelve a la etapa de planificación para redibujar el plano, en lugar de parchar frenéticamente el edificio terminado.

El Nuevo Campo de Prueba: Lean4Commit0

Los autores se dieron cuenta de que las pruebas anteriores para estos sistemas de IA eran demasiado fáciles, como pedirle al robot que resuelva acertijos matemáticos de un libro de texto. El software del mundo real es más desordenado. Para probar adecuadamente su nuevo método, construyeron un nuevo benchmark llamado Lean4Commit0.

Extrajeron información de 108 bibliotecas de software de código abierto real (escritas en Python, Rust, C/C++ y Java) y convirtieron sus características principales en desafíos de "código verificado". En lugar de tareas simples como "sumar dos números", estos desafíos implican relaciones complejas entre diferentes partes de un programa. Por ejemplo, en un sistema de configuración, podrían pedirle a la IA que demuestre que "si estableces un ajuste en 'Alto' y luego lo cambias a 'Bajo', el sistema recuerda correctamente el ajuste 'Bajo'". Estas tareas requieren que la IA comprenda cómo diferentes funciones se comunican entre sí, lo que las hace mucho más difíciles que los problemas de libros de texto.

Lo que Encontraron: La Planificación Inteligente Gana

El equipo probó P3 contra cuatro de los modelos de IA más potentes disponibles (incluyendo versiones de Codex, Gemini y Claude) a través de tres benchmarks diferentes: Verina, AlgoVeri y su nuevo Lean4Commit0.

Los resultados fueron claros: Planificar juntos funciona mejor que escribir por separado.

Tasa de Éxito: P3 resolvió más tareas que cualquier otro método en cada una de las pruebas. En las tareas más difíciles, mejoró la tasa de éxito entre 4.6 y 11.2 puntos porcentuales en comparación con los mejores métodos existentes.
Eficiencia: No se trató solo de resolver más problemas; se trató de resolverlos de forma más rápida y económica. En tareas difíciles, P3 redujo el costo de las llamadas a la API hasta en un 40% y recortó el tiempo empleado hasta en un 37%. Esto se debe a que la IA no perdió tiempo intentando demostrar cosas imposibles o reescribiendo código que era estructuralmente erróneo.
La Ventaja "Conjunta": Para demostrar que la "planificación conjunta" era el ingrediente secreto, realizaron una prueba donde la IA planificaba el código pero no planificaba la prueba de antemano. Este método de "planificación solo de código" funcionó peor que P3, confirmando que pensar en la prueba mientras se planifica el código es lo que marca la diferencia.

Un Ejemplo del Mundo Real: El Árbol Rojo-Negro

Para mostrar cómo funciona esto en la práctica, los autores analizaron un problema clásico de la informática: eliminar un nodo de un "árbol rojo-negro" (una estructura de datos compleja utilizada para organizar datos de manera eficiente).

La Forma Antigua (Programa-luego-Prueba): La IA se comprometió con una forma específica de eliminar el nodo. Resultó que esta forma era tan estructuralmente desordenada que la prueba requería más de 6,300 líneas de código solo para reparar los huecos, o fallaba por completo.
La Forma P3: La IA primero planificó la eliminación. Se dio cuenta de que un enfoque estructural diferente sería más fácil de demostrar. Se mantuvo fiel a ese plan y resolvió el problema en solo 1,105 líneas.

Por Qué Esto Importa

Este artículo sugiere que, para que la IA escriba software verdaderamente fiable, debemos dejar de tratar el "código" y la "prueba" como dos trabajos separados. Al obligar a la IA a pensar en la seguridad matemática del código mientras está diseñando el código mismo, obtenemos software que no solo es correcto por construcción, sino también más barato y rápido de producir. Es un cambio de "arreglarlo después" a "construirlo bien a la primera", asegurando que el software en el que confiamos sea tan sólido como las matemáticas que demuestran que funciona.

Resumen Técnico: P3 – Planificación Conjunta de Programa y Prueba para la Generación de Código Verificado

1. Planteamiento del Problema

El artículo aborda la generación de código verificado, una tarea en la que un Modelo de Lenguaje Grande (LLM) debe sintetizar tanto un programa ejecutable ( $\pi$ ) como una prueba verificable por máquina ( $\kappa$ ) que demuestre que el programa satisface una especificación formal ( $\sigma = (P, Q)$ ). A diferencia de la generación basada en pruebas (tests), la corrección debe sostenerse para todas las entradas admisibles, no solo para un conjunto finito de ejemplos.

Los autores identifican un cuello de botella crítico en el flujo de trabajo de facto actual, que sigue un esquema secuencial de "programa-luego-prueba":

El LLM se compromete con una implementación concreta.
Una etapa de demostración separada intenta descargar las obligaciones de la prueba.
Si la verificación falla, el sistema entra en un frágil bucle de "parche y reintento", alternando entre corregir el código y corregir las pruebas.

Este enfoque secuencial sufre de dos problemas principales:

Efectividad: Un programa generado sin anticipar su prueba puede carecer de las propiedades estructurales necesarias (por ejemplo, estrategias de descomposición o invariantes de inducción específicas). Las reparaciones locales suelen fallar al intentar recuperar una estructura apta para la prueba que nunca fue planificada.
Eficiencia: Se desperdician recursos computacionales significativos (tokens y tiempo) explorando reparaciones para implementaciones que son estructuralmente incompatibles con los requisitos de prueba de la especificación.

El artículo se inspira en el principio de Dijkstra de que los programas y sus argumentos de corrección deben desarrollarse "mano a mano", argumentando que la implementación y la estructura de la prueba se restringen mutuamente.

2. Metodología: El Marco P3

Los autores proponen P3, un flujo de trabajo agéntico que desacopla la planificación de la elaboración para asegurar la consistencia estructural entre el programa y la prueba antes de que cualquiera de los dos se materialice por completo.

2.1 Planificación Conjunta de Programa y Prueba

En la primera etapa, el agente LLM genera un plan unificado ( $\rho$ ) basado en la especificación $\sigma$ . Este plan no es meramente código; es un esquema de alto nivel que contiene cuatro compromisos específicos:

Contrato Formal: Instrucciones algorítmicas y restricciones asintóticas.
Descomposición del Programa: La variable de recursión, la estructura de ramificación, la representación de datos y las medidas de terminación.
Dependencias de Librerías: Funciones concretas y lemas existentes que se utilizarán.
Obligaciones de Prueba: El predicado de puente (bridging predicate), la estructura de inducción/casos y las declaraciones de lemas auxiliares necesarios.

El agente valida estos planes candidatos al nivel de esquema. Un plan se rechaza si el esquema del programa viola las instrucciones, si la descomposición no preserva el predicado de puente, o si el predicante no implica la poscondición. El agente selecciona el plan que minimiza la carga de prueba anticipada.

2.2 Elaboración Guiada por el Plan

Una vez seleccionado un plan $\rho$ , el agente entra en la etapa de elaboración:

Implementación: El agente escribe el código ( $\pi$ ) adhiriéndose estrictamente a la descomposición y estructura fijadas en $\rho$ .
Andamiaje de la Prueba (Proof Scaffold): El agente escribe un esqueleto de prueba ( $\kappa$ ) que refleja la estructura del plan (por ejemplo, principios de inducción específicos o divisiones de casos), dejando brechas locales (representadas como sorry) para tácticas detalladas.
Refinamiento: El agente utiliza la retroalimentación de Lean 4 (vía LSP/MCP) para llenar estas brechas. Crucialmente, si las reparaciones locales fallan repetidamente o si el predicado de puente resulta demasiado débil, el agente identifica esto como un fallo a nivel de plan. En lugar de oscilar erráticamente entre ediciones de código y de prueba, el agente retrocede a la etapa de planificación para revisar $\rho$ .

Esta separación permite al agente distinguir entre errores de nivel de elaboración (corregibles localmente) y errores de nivel de plan (que requieren un replanteamiento estructural), reduciendo significamente el espacio de búsqueda.

3. Benchmark: Lean4Commit0

Para evaluar la generación de código verificado en entornos realistas más allá de los algoritmos de libros de texto, los autores introducen Lean4Commit0.

Fuente: Derivado de 108 librerías de código abierto del mundo real en Python, Rust, C/C++ y Java.
Alcance: Extrae APIs centrales y codifica sus comportaciones como tareas de Lean, incluyendo especificaciones relacionales que restringen el comportamiento conjunto de múltiples funciones (por ejemplo, la consistencia entre las operaciones set y get).
Control de Calidad: Un proceso de tres etapas asegura la calidad de la especificación:
1. Satisfacción de Referencia: Verifica que la implementación original de la librería satisface la especificación de Lean.
2. Rechazo de Mutación: Asegura que la especificación rechaza comportamientos alterados por mutaciones (evitando especificaciones sub-restringidas).
3. Revisión por LLM: Identifica especificaciones triviales o irrelevantes.
Escala: El benchmark final contiene 511 marcadores de posición de implementación y 519 marcadores de posición de teoremas.

4. Resultados Experimentales

Los autores evaluaron P3 contra dos líneas base —un agente PLAIN (sin estrategia específica) y un agente SEQ (programa-luego-prueba)— utilizando cuatro backends de LLM de frontera (Codex-GPT-5.5, Gemini-3-Pro, Claude-Sonnet-4.6, Claude-Opus-4.7) a través de tres benchmarks: Verina, AlgoVeri y Lean4Commit0.

Tasas de Resolución: P3 logró la tasa de resolución más alta en cada configuración de (benchmark, modelo).
- Comparado con la línea base más fuerte, P3 mejoró las tasas de resolución entre 4.6 y 11.2 puntos porcentuales.
- En el subconjunto difícil de los benchmarks, P3 redujo los costos de API por tarea hasta en un ~40% y el tiempo de ejecución (wall-clock time) hasta en un ~37%.
Estudio de Ablación: Una comparación con PLAN-SEQ (que planifica las elecciones de implementación pero no la estructura de la prueba) mostró que la planificación conjunta contribuye específicamente con una ganancia adicional de 3.3 a 8.3 puntos porcentuales. Esto aísla el beneficio de anticipar la estructura de la prueba durante la fase de planificación.
Caso de Estudio: En una tarea de eliminación de un árbol rojo-negro balanceado hacia la izquierda, la línea base de programa-luego-prueba falló tras generar 6,344 líneas de código o tuvo éxito solo con invariantes de reconstrucción redundantes (1,176 líneas). P3, al comparar planes antes de comprometerse, resolvió la tarea en 1,105 líneas.

5. Significación y Reivindicaciones

El artículo sostiene que P3 demuestra que la generación de código verificado puede hacerse más efectiva y eficiente tratando el programa y la prueba como artefactos co-diseñados en lugar de salidas secuenciales.

Consistencia Estructural: Al establecer un plan estructural compartido, P3 asegura que la implementación y la prueba sean consistentes "por construcción", evitando la necesidad de una reconciliación post-hoc.
Escalabilidad a Código del Mundo Real: La introducción de Lean4Commit0 cierra la brecha entre los benchmarks académicos (algoritmos de libros de texto) y el software de producción (restricciones de API relacionales), mostrando que la planificación conjunta es particularmente beneficiosa para tareas complejas a nivel de librería.
Eficiencia: El marco reduce el comportamiento de "oscilación" (thrashing) común en los bucles de reparación iterativa, lo que conduce a ahorros significativos en recursos computacionales y tiempo.

Los autores concluyen que, si bien el verificador (Lean 4) sigue siendo la autoridad final, la capacidad del agente para planificar el programa y la prueba de forma conjunta aumenta significamente la probabilidad de producir una solución verificada dentro de límites de recursos prácticos.