Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification

Resumen Técnico: Goedel-Code-Prover

1. El Problema: La Brecha entre Generación de Código y Verificación Formal

Aunque los Modelos de Lenguaje Grandes (LLMs) han avanzado significativamente en la generación de código, su capacidad para garantizar la corrección formal es limitada. Las pruebas empíricas (como pruebas unitarias) no pueden certificar la ausencia de errores lógicos sutiles o violaciones de especificaciones.

La verificación formal en Lean 4 ofrece una solución rigurosa mediante la construcción de pruebas verificables por máquina. Sin embargo, automatizar este proceso para el código es mucho más difícil que para las matemáticas puras debido a tres desafíos fundamentales:

1. Descomposición sin base (Ungrounded decomposition): A diferencia de las matemáticas, donde existe un vasto corpus de razonamiento informal en libros y papers que los LLMs pueden aprender, el razonamiento sobre la corrección del código es escaso en los datos de entrenamiento. Los LLMs carecen de la intuición para descomponer problemas de código en lemas útiles.
2. Proliferación de conceptos: Cada programa introduce un "universo conceptual" nuevo (funciones, invariantes de estructuras de datos, flujos de control) sin bibliotecas compartidas (como Mathlib en matemáticas) que ofrezcan lemas reutilizables.
3. Desplazamiento en la distribución de tácticas: Las tácticas necesarias para verificar código (lógica discreta, recursión, reflexión computacional) difieren sustancialmente de las tácticas algebraicas predominantes en las pruebas matemáticas, lo que hace que los modelos entrenados en matemáticas fallen al intentar probar subobjetivos de código.

2. Metodología: Búsqueda Jerárquica de Pruebas

Los autores proponen un marco de búsqueda jerárquica de pruebas que descompone los objetivos de verificación complejos en subobjetivos estructuralmente más simples antes de intentar generar tácticas de prueba.

Componentes Clave:

• Marco de Trabajo (Lean 4): El sistema opera en un bucle de "planificación y prueba".

  • Fase 1 (Descomposición de Lemas): El modelo divide un teorema de verificación en una serie de lemas intermedios.
  • Fase 2 (Completado de Lemas): El mismo modelo intenta probar cada lema hoja mediante la generación iterativa de tácticas y refinamiento basado en retroalimentación del compilador de Lean.

• Puntuación de Descomposición Principista (Decomposition Score):
  El núcleo de la metodología es una métrica de puntuación ($S$) que sirve tanto como recompensa de entrenamiento como criterio de clasificación en tiempo de inferencia. Esta puntuación combina dos ejes:

  1. Justificación Constructiva: Verifica que los lemas propuestos impliquen lógicamente el teorema padre (mediante reconstrucción de pruebas) y que no contengan contraejemplos (usando quickcheck para búsqueda automática de contraejemplos).
  2. Efectividad Estructural: Mide la reducción de la complejidad. Se define como la reducción en la "huella de operadores" (número de operadores lógicos y del dominio en el Árbol de Sintaxis Abstracta - AST) entre el objetivo original y los subobjetivos.
     $$S = r \cdot v$$
     Donde $v$ es la validez binaria (1 si pasa los filtros, 0 si no) y $r$ es la tasa de reducción estructural.

• Entrenamiento del Modelo (Goedel-Code-Prover-8B):
  Se entrena una única política unificada para realizar tanto la descomposición como la completación de pruebas.

  • Inicialización Supervisada (SFT): Se utiliza un modelo base (Qwen-3-8B) fine-tuneado con 281k pares de descomposición y 151k pares de completación generados por modelos de vanguardia.
  • Aprendizaje por Refuerzo Híbrido (Hybrid RL): Para resolver la discrepancia de recompensas (la descomposición tiene una señal densa y continua, mientras que la completación es binaria y dispersa), se utiliza un enfoque híbrido:
    • La descomposición se optimiza mediante GRPO (Group Relative Policy Optimization) usando la puntuación $S$ continua.
    • La completación se estabiliza mediante repetición supervisada de trayectorias de prueba de alta calidad, evitando que el gradiente de la descomposición domine y estagne la habilidad de prueba.

3. Contribuciones Clave

1. Marco de Búsqueda Jerárquica: Un sistema que descompone objetivos de verificación de código en lemas estructurales antes de la generación de tácticas, abordando la complejidad del dominio.
2. Puntuación de Descomposición Unificada: Una métrica que combina justificación lógica y simplicidad estructural, alineando estrictamente el objetivo de entrenamiento con el criterio de búsqueda en tiempo de inferencia.
3. Pipeline de RL Híbrido: Un método de entrenamiento que equilibra la exploración estructural (descomposición) con la generación estable de pruebas (completación) dentro de una sola política.
4. Modelo Eficiente y Potente: Demostración de que un modelo de 8 mil millones de parámetros (Goedel-Code-Prover-8B), específicamente entrenado para esta tarea, supera a modelos de vanguardia mucho más grandes.

4. Resultados Experimentales

El marco se evaluó en tres conjuntos de datos de verificación de código en Lean 4: Verina (189 tareas), Clever (161 tareas) y AlgoVeri (77 tareas), totalizando 427 tareas.

• Rendimiento General: El modelo Goedel-Code-Prover-8B logró una tasa de éxito de prueba del 62.0% en promedio.
• Comparativa:
  • Superó a los modelos de razonamiento de vanguardia (como GPT-5.3-Codex, Claude-Opus-4.6) que intentan generar pruebas en un solo paso.
  • Superó a los "provers" neuronales más grandes (hasta 84 veces más grandes, como DeepSeek-Prover-V2-671B) con una mejora de 2.6x sobre la línea base más fuerte.
• Escalabilidad: Se observó un escalado consistente en tiempo de inferencia; las tasas de éxito mejoraron monótonamente al aumentar el presupuesto de búsqueda (iteraciones) y el presupuesto de muestreo paralelo ($pass@k$).
• Complejidad de las Pruebas: Las pruebas verificadas promediaron entre 8 y 17 lemas descompuestos y más de 130 líneas de código de prueba, demostrando la capacidad del sistema para realizar razonamiento estructurado profundo.

5. Significado e Impacto

Este trabajo es significativo porque cierra la brecha entre la generación de código y la verificación formal rigurosa.

• Democratización de la Verificación: Demuestra que no se necesitan modelos masivos (cientos de miles de millones de parámetros) para la verificación formal de código si se utiliza una arquitectura adecuada (descomposición jerárquica) y un entrenamiento específico.
• Superación de la Brecha Matemática-Código: Aborda explícitamente por qué los métodos exitosos en matemáticas fallan en código y propone soluciones técnicas (puntuación de descomposición, RL híbrido) para superar la falta de corpus de razonamiento informal en el software.
• Eficiencia: Ofrece una ruta escalable y eficiente para la verificación de software en entornos críticos, donde la corrección es obligatoria.

En resumen, Goedel-Code-Prover establece un nuevo estado del arte en la verificación automática de código, demostrando que la planificación jerárquica guiada por una métrica de calidad unificada es la clave para automatizar la demostración de teoremas en el dominio del software.