Neural Theorem Proving for Verification Conditions: A Real-World Benchmark

Resumen Técnico: Demostración de Teoremas Neuronal para Condiciones de Verificación (NTP4VC)

Planteamiento del Problema
La verificación de programas es una piedra angular de la fiabilidad del software, sin embargo, su adopción sigue limitada a dominios de seguridad crítica. Un cuello de botella principal es el esfuerzo manual requerido para demostrar las Condiciones de Verificación (VC, por sus siglas en inglés)—proposiciones lógicas que codifican la corrección de un programa. Aunque los Demostradores Automáticos de Teoremas (ATP) sobresalen en dominios específicos, frecuentemente fallan en VCs del mundo real, lo que requiere anotaciones y demostraciones manuales extensas. Además, la Demostración de Teoremas Neuronal (NTP) ha mostrado potencial en competiciones matemáticas, pero su aplicación al dominio específico y de alto riesgo de la demostración automatizada de VC en la verificación de programas permanece en gran medida inexplorada. Asimismo, los benchmarks existentes para la demostración de teoremas suelen centrarse en lemas auxiliares o acertijos matemáticos en lugar de las VCs directas generadas por los pipelines de verificación industrial, y carecen de soporte para múltiples lenguajes formales.

Metodología
Los autores introducen NTP4VC, una tarea y un benchmark diseñados para evaluar la capacidad de los Modelos de Lenguaje de Gran Escala (LLMs) para automatizar la demostración de VC. La metodología consta de tres componentes principales:

1. Extracción y Traducción de Corpus:

   • El benchmark aprovecha proyectos de verificación industrial existentes (por ejemplo, el planificador del kernel de Linux, el asignador de memoria de Contiki-OS) procesados a través de pipelines establecidos: Frama-C (para código C) y Why3 (como backend de verificación).
   • Dado que las VCs nativas en lenguajes de NTP convencionales como Lean son escasas para proyectos industriales, los autores desarrollaron un pipeline de traducción basado en reglas. Este sistema extrae las VCs de Why3 y las traduce a Isabelle, Lean y Rocq (anteriormente Coq).
   • La traducción se basa en aproximadamente 2,400 reglas de mapeo y reescritura escritas por expertos (por lenguaje) para asegurar la preservación semántica y la expresión idiomática en el lenguaje objetivo, evitando la falta de fiabilidad de la traducción basada en LLMs.

2. Proceso de Complicación:

   • Las VCs extraídas directamente de proyectos verificados suelen ser "demasiado fáciles" porque los desarrolladores humanos ya han proporcionado suficientes anotaciones (por ejemplo, assert, lemma y anotaciones de aplicación de lemas) para guiar a los ATP.
   • Para crear casos de benchmark desafiantes, los autores implementaron un proceso de complicación que elimina sistemáticamente estas anotaciones auxiliares. Esto devuelve las VCs a un estado más cercano a la verificación totalmente automatizada, aumentando significativamente la dificultad mientras se mantiene la demostrabilidad (asumiendo un demostrador suficientemente fuerte).

3. Construcción del Benchmark:

   • El benchmark final consiste en 600 VCs cuidadosamente seleccionadas de un total de más de 7,500 candidatas.
   • El conjunto está equilibrado entre dos categorías:
     • Perlas de Programas (50%): Programas funcionales mínimos que capturan puntos de dolor de la verificación (algoritmos, estructuras de datos, problemas de competición como VerifyThis).
     • Verificación Real de C (50%): VCs derivadas de proyectos C industriales (por ejemplo, Contiki-OS, kernel de Linux, parsers de X.509).
   • La dificultad está calibrada de tal manera que el ATP predefinido más fuerte en Why3 (Auto_Level_3) logra una tasa de éxito entre el 20% y el 25%, asegurando una mezcla de problemas resolubles y abiertos.

Contribuciones Clave

• Definición de NTP4VC: El artículo define formalmente la tarea de aplicar la generación de pruebas basada en aprendizaje automático para automatizar la demostración de VC, identificándola como un cuello de botella crítico en la verificación de programas.
• Método de Extracción Fiable: Un método novedoso y de código abierto para extraer y traducir VCs de pipelines de verificación industrial a múltiples lenguajes de ITP utilizando reglas escritas por expertos en lugar de LLMs, garantizando la fidelidad semántica.
• Primer Benchmark Multilenguaje del Mundo Real: La introducción de NTP4VC, el primer benchmark dirigido específicamente a la demostración automatizada de VC a través de Isabelle, Lean y Rocq, presentando una mezcla diversa de casos algorítmicos e industriales.
• Evaluación Exhaustiva: Una evaluación extensa de siete modelos, incluyendo LLMs de propósito general (por ejemplo, GPT-4o-mini, Qwen3) y demostradores de teoremas especializados (por ejemplo, DeepSeek-Prover-V2, Goedel-Prover), junto con demostradores "hammer" clásicos (Sledgehammer, CoqHammer).

Resultos
La evaluación revela desafíos significativos para los modelos NTP actuales en la verificación de programas:

• Bajas Tasas de Acierto: Incluso los mejores modelos con alto rendimiento logran tasas de éxito muy bajas. El modelo especializado por lenguaje con mejor desempeño (Minilang) logra solo un 2.08% de pass@1 en Isabelle. Los modelos de propósito general funcionan incluso peor (por ejemplo, GPT-o4-mini-high con un 1.19% de pass@1).
• Comparación con Hammers: Los demostradores basados en hammers clásicos superan significativamente a los modelos neuronales. Sledgehammer logra un 18.00% de pass@1 en Isabelle, y CoqHammer logra un 5.67% en Rocq.
• Análisis de Errores: Los modos de fallo difieren de los benchmarks matemáticos. Los modelos NTP luchan con:
  • Errores Sintácticos: ~24% de las pruebas de Isabelle fallan debido a paréntesis desparejados o problemas de sintaxis en fórmulas profundamente anidadas.
  • Confusión Semántica: Los modelos a menudo producen código pragmáticamente incorrecto (por ejemplo, asignaciones imperativas en Lean en lugar de tácticas declarativas) o aplicaciones de tácticas repetitivas y sin sentido.
  • Alucinación: Los modelos invocan frecuentemente tácticas inexistentes (por ejemplo, why3 en Rocq) o constantes no definidas.
• Especificidad del Dominio: Los hammers funcionan notablemente mejor en las tareas de "Verificación Real de C" que en las de "Perlas de Programas", lo que sugiere que las técnicas de razonamiento clásico (solvers SMT) están altamente optimizadas para escenarios de verificación industrial, mientras que los modelos NTP tienen dificultades en ambos dominios.

Significancia y Reivindicaciones
El artículo sostiene que NTP4VC establece un benchmark fundacional para avanzar las aproximaciones neuronales a la verificación de programas. Los resultados resaltan una brecha sustancial entre las capacidades actuales de NTP y los requisitos de la verificación de programas del mundo real, indicando que la verificación de programas demanda capacidades de razonamiento fundamentalmente distintas a las de los problemas de competición matemática. Los autores afirman que, si bien los LLMs muestran potencial, se necesita un progreso significativo en el manejo de la naturaleza larga, profundamente anidada y sintácticamente rígida de las VCs. El trabajo proporciona una infraestructura necesaria (benchmark y pipeline de extracción) para impulsar la investigación futura hacia el cierre de esta brecha, potencialmente conduciendo a avances en la verificación automatizada de programas. Los autores se mantienen modestos, señalando que los casos del benchmark se derivan de proyectos formalmente verificados, pero reconociendo que errores de implementación en el pipeline de traducción podrían, teóricamente, hacer que algunos casos sean indemostrables, aunque han tomado medidas exhaustivas para mitigarlo.