Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought

Resumen Técnico: VCoT-Bench - Evaluación mediante Cadenas de Pensamiento de Verificación

1. El Problema

A medida que los Modelos de Lenguaje Grandes (LLM) se integran en el desarrollo de software seguro, su capacidad para cumplir con los rigurosos requisitos de la verificación formal de programas en Rust sigue siendo incierta.

• Limitación de las evaluaciones actuales: Los trabajos existentes (como AlphaVerus, AutoVerus) tratan la verificación como una "caja negra", evaluando a los modelos únicamente mediante resultados binarios (éxito/fracaso) en la generación de hints (pistas) de prueba.
• La brecha de comprensión: Este enfoque binario oculta si el modelo realmente comprende la lógica deductiva necesaria o si simplemente explota patrones estadísticos y alineación sintáctica.
• La barrera técnica: Los demostradores de teoremas automatizados (ATP) como Z3 (utilizado por el marco de verificación Verus) generan trazas de prueba extremadamente verbosas y de bajo nivel (miles de líneas con igualdades triviales), lo que impide a los humanos y a los LLMs analizar el proceso de razonamiento subyacente.

2. Metodología

Para abordar estas limitaciones, los autores proponen un enfoque en dos etapas: la creación de una herramienta de extracción de razonamiento y un nuevo estándar de evaluación.

A. VCoT-Lift (Marco de Extracción)
Es un framework basado en LLMs diseñado para elevar el razonamiento de bajo nivel de Z3 a pasos de verificación de alto nivel y legibles por humanos, denominados Cadenas de Pensamiento de Verificación (VCoT).

• Objetivo: Transformar las trazas de Z3 en pasos semánticos equivalentes en Verus (invariantes de bucle, aserciones, funciones de lema).
• Pipeline de cuatro etapas:
  1. Transformador de Pruebas: Convierte las pruebas de Z3 en pruebas de Verus. Utiliza una jerarquía de reglas de Z3 (Alto, Medio, Bajo nivel) para guiar la atención del LLM hacia los pasos semánticamente informativos.
  2. Verificador de Pruebas: Evalúa la completitud de la transformación. Utiliza agentes especializados por tipo de regla (ej. Modus Ponens, Lema) y un filtro de abstracción para ignorar pasos triviales o redundantes.
  3. Poda (Pruner): Elimina pasos redundantes o triviales para mejorar la concisión, basándose en criterios definidos para invariantes, aserciones y lemas.
  4. Reparación de Pruebas: Un agente interactúa con el compilador de Verus para detectar y corregir errores sintácticos o semánticos, asegurando la solidez (soundness) de la prueba final.

B. VCoT-Bench (Benchmarks de Evaluación)
Utilizando VCoT-Lift, los autores construyen un benchmark exhaustivo de 1,988 tareas de finalización de VCoT.

• Construcción: Se extraen "agujeros de prueba" (bloques semánticos eliminados) de las pruebas VCoT completas.
• Dimensiones de Evaluación: El benchmark mide el rendimiento en tres dimensiones ortogonales:
  1. Ratio (VCoT-Bench-Ratio): Robustez ante diferentes grados de pérdida de información (desde 10% hasta 100% de bloques eliminados).
  2. Tipo (VCoT-Bench-Type): Competencia en tipos específicos de pruebas: Invariantes de bucle, Aserciones y Funciones de Lema.
  3. Ubicación (VCoT-Bench-Loc): Sensibilidad a la posición de los pasos faltantes (Inicio, Medio, Final).

3. Contribuciones Clave

1. Concepto VCoT: Introduce la noción de "Cadena de Pensamiento de Verificación" como una verdad fundamental (ground truth) explícita para la verificación formal.
2. Herramienta VCoT-Lift: El primer framework capaz de abstraer el razonamiento de demostradores de teoremas (Z3) a pasos de verificación de alto nivel (Verus) de manera sólida y completa.
3. Benchmark VCoT-Bench: Un conjunto de datos estandarizado que permite una evaluación granular más allá del simple "pasa/falla", analizando la capacidad de razonamiento deductivo.
4. Estudio Empírico: Una evaluación exhaustiva de 10 LLMs de última generación (incluyendo GPT-5, Claude, Gemini, DeepSeek y Qwen), revelando limitaciones críticas.

4. Resultados Principales

El estudio de 10 modelos de vanguardia revela una fragilidad severa y una brecha significativa entre los LLMs actuales y los demostradores de teoremas automatizados:

• Fragilidad ante la pérdida de contexto: La precisión cae drásticamente incluso con una pérdida mínima de información.
  • Con solo un 10% de bloques eliminados, el mejor modelo (Claude Sonnet 4.5) alcanza solo un 71.58% de precisión.
  • Con un 100% de eliminación (construcción completa desde cero), el rendimiento colapsa (ej. Claude cae al 17.22%, Qwen 3 "think" al 0.66%).
  • Conclusión: Los LLMs dependen de patrones sintácticos locales y andamiaje contextual, no de la deducción desde primeros principios.
• Umbral de ruptura: Existe un umbral crítico alrededor del 40% de eliminación de bloques, donde la continuidad lógica colapsa y el rendimiento se estanca en niveles bajos independientemente de la eliminación adicional.
• Dificultad por Tipo de Prueba:
  • Las Aserciones son las más difíciles (precisión más baja), ya que requieren un razonamiento preciso dependiente del estado.
  • Las Invariantes de Bucle son las más fáciles de completar sintácticamente, pero son las más discriminativas: separan claramente a los modelos con capacidad de verificación real de los que solo hacen coincidencia de patrones.
• Dificultad por Ubicación:
  • El Medio de la prueba es la parte más difícil. Los modelos luchan con el "razonamiento conector" (propagar invariantes, rastrear la evolución del estado), mientras que el inicio y el final (que siguen patrones más reconocibles) son más manejables.
• Escala vs. Rendimiento: Aunque los modelos más grandes generalmente rinden mejor, la escala no garantiza la capacidad de razonamiento deductivo en tareas de verificación complejas. Curiosamente, algunos modelos con "pensamiento" (Chain of Thought) a veces rinden peor que sus versiones directas, sugiriendo que el razonamiento verbalizado puede introducir ruido en la precisión sintáctica y semántica requerida.

5. Significado e Impacto

Este trabajo cambia el paradigma de la evaluación de LLMs en verificación formal:

• De "Caja Negra" a "Caja Transparente": Demuestra que evaluar solo el resultado final es insuficiente; es necesario inspeccionar el proceso de razonamiento.
• Limitación Actual: Revela que, a pesar de los avances, los LLMs actuales carecen de la capacidad de razonamiento deductivo robusto necesaria para reemplazar o asistir eficazmente a los demostradores de teoremas en la verificación de código crítico de Rust.
• Futuro: VCoT no solo sirve como herramienta de evaluación, sino que ofrece una señal de supervisión concreta para entrenar futuros sistemas de verificación basados en aprendizaje, guiándolos hacia una alineación simbólica real y no solo a la imitación sintáctica.

En resumen, el artículo concluye que los LLMs actuales no razonan como demostradores de teoremas automatizados; su éxito en la verificación es frágil y depende excesivamente del contexto local, fallando estrepitosamente cuando se requiere construir cadenas deductivas complejas sin andamiaje.