Resumen: La demostración de teoremas es fundamental para la verificación de programas, donde la prueba automatizada de las Condiciones de Verificación (VC) sigue siendo un cuello de botella principal. La verificación de programas en el mundo real frecuentemente encuentra VC difíciles que los probadores automatizados de teoremas (ATP) existentes no pueden probar, lo que genera una necesidad crítica de pruebas manuales extensas que sobrecargan la aplicación práctica. Si bien la demostración de teoremas neuronales (NTP) ha logrado un éxito significativo en competencias matemáticas, demostrando el potencial de los enfoques de aprendizaje automático para el razonamiento formal, su aplicación a la verificación de programas (particularmente la demostración de VC) permanece en gran medida inexplorada. A pesar del trabajo existente sobre síntesis de anotaciones y demostración de teoremas relacionados con la verificación, ningún punto de referencia se ha centrado específicamente en este cuello de botella fundamental: la demostración automatizada de VC. Este trabajo presenta la demostración de teoremas neuronales para condiciones de verificación (NTP4VC), presentando el primer punto de referencia multilingüe del mundo real para esta tarea. A partir de proyectos del mundo real como Linux y el kernel Contiki-OS, nuestro punto de referencia aprovecha los procesos industriales (Why3 y Frama-C) para generar casos de prueba semánticamente equivalentes en los lenguajes formales de Isabelle, Lean y Rocq. Evaluamos modelos de lenguaje grande (LLM), tanto de propósito general como aquellos ajustados para la demostración de teoremas, en NTP4VC. Los resultados indican que, aunque los LLM son prometedores en la prueba de VC, aún quedan desafíos importantes para la verificación del programa, lo que resalta una gran brecha y oportunidad para investigaciones futuras.
Publicado originalmente en export.arxiv.org el 27 de enero de 2026.
Ver fuente original
