Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers

El artículo presenta Strat2Rocq, un enfoque que extrae y formaliza estrategias de prueba de modelos de lenguaje grandes para enriquecer el contexto de demostración de provadores simbólicos como CoqHammer, logrando así mejorar significativamente sus tasas de éxito en la verificación de software.

Lo esencial

¡Claro que sí! Imagina que el mundo de la verificación de software (asegurar que un programa no tenga errores) es como un laboratorio de detectives.

Aquí te explico de qué trata este paper, Strat2Rocq, usando analogías sencillas:

1. El Problema: Dos tipos de detectives

En este laboratorio hay dos tipos de investigadores para resolver casos (probar que un código es seguro):

• El Detective Lógico (El Proveedor Simbólico): Es como un robot muy estricto y rápido. Sigue reglas matemáticas al pie de la letra. Es barato, seguro (no comparte secretos) y funciona en cualquier computadora. Pero a veces se atasca porque es demasiado literal; si no ve el paso exacto, no puede saltar al siguiente.
• El Detective Intuitivo (La IA o LLM): Es un genio humano (o una IA muy avanzada) que tiene mucha "intuición". Puede ver patrones y saltar pasos lógicos de un solo golpe. Es muy bueno, pero es caro (necesita mucha energía), lento y, si le muestras tu código secreto, podría "contarlo" a otros (riesgo de seguridad).

El dilema: Las empresas quieren usar al Detective Intuitivo por su talento, pero no pueden permitirse el costo ni el riesgo de seguridad. Quieren usar al Detective Lógico, pero a veces se queda atascado.

2. La Idea Brillante: "Robar" la intuición

Los autores se preguntaron: "¿Podemos enseñarle al Detective Lógico a pensar como el Detective Intuitivo, sin tener que invitar a este último a la oficina?"

La respuesta es Sí. Y así nace Strat2Rocq.

3. ¿Cómo funciona Strat2Rocq? (El proceso en 2 pasos)

Imagina que el Detective Intuitivo (la IA) está resolviendo un caso muy difícil.

• Paso 1: La Grabación (Minería Offline)
  En lugar de dejar que la IA resuelva el caso en vivo, la ponemos a trabajar en un "gimnasio" con miles de casos antiguos.

  1. Pedimos a la IA: "Resuelve este caso y explícame cómo lo hiciste paso a paso".
  2. La IA dice: "Bueno, vi que A más B es igual a C, así que salté directamente a la conclusión".
  3. Aquí viene la magia: El sistema toma ese "salto intuitivo" de la IA y lo convierte en una regla oficial escrita en un libro de leyes (un "lema" formal).
  • Analogía: Es como si el chef estrella (la IA) te dijera: "El secreto de mi salsa es añadir sal antes del vinagre". Tú no necesitas al chef en tu cocina; solo escribes esa regla en tu libro de recetas y la guardas.

• Paso 2: La Aplicación (Prueba Online)
  Ahora, cuando llega un caso nuevo y difícil, el Detective Lógico (CoqHammer) abre su libro de reglas.

  • Antes: Miraba las reglas básicas y se atascaba.
  • Ahora: Mira su libro y ve: "¡Ah! Hay una regla nueva que dice 'Si ves X, salta a Y' (esa regla que robamos de la IA)".
  • ¡Boom! El detective lógico usa esa nueva regla y resuelve el caso rápidamente, sin necesidad de llamar al chef estrella.

4. Los Resultados: ¡Funciona!

Los autores probaron esto con software real (como compiladores y sistemas operativos).

• El Detective Lógico mejoró un 13.41%: Resolvió muchos más casos que antes.
• El Detective Intuitivo también se benefició: Cuando la IA usó esas reglas robadas, también resolvió más casos y gastó menos "energía" (tokens).
• Seguridad total: Todo el proceso de "robado de ideas" se hizo antes, en privado. Cuando llega el caso real, no se necesita internet ni servidores caros; todo ocurre en la computadora local.

En resumen

Este paper es como crear un "manual de trucos".
En lugar de depender de un genio costoso cada vez que tienes un problema, le pides al genio que te enseñe sus trucos una sola vez, los escribes en un libro y luego cualquier persona (o robot) puede usar esos trucos para resolver problemas difíciles de forma rápida, barata y segura.

La moraleja: No necesitas ser un genio para resolver problemas difíciles si tienes acceso a los trucos de los genios.

Resumen técnico

Resumen Técnico: Strat2Rocq

1. El Problema

La verificación de software mediante demostración de teoremas interactiva (ITP) es crucial, pero la escritura de pruebas formales requiere un esfuerzo humano masivo. Aunque los Grandes Modelos de Lenguaje (LLMs) han demostrado capacidades notables en la automatización de pruebas y complementan a los métodos simbólicos tradicionales, existen limitaciones significativas:

• Costo y Seguridad: El uso de LLMs en línea es costoso y plantea riesgos de seguridad para bases de código confidenciales (común en empresas de software crítico).
• Dependencia de Infraestructura: Los agentes híbridos que dependen de LLMs requieren recursos computacionales sustanciales, lo que los hace inviables para entornos con hardware limitado.
• La Brecha: Los sistemas puramente simbólicos (como CoqHammer) son seguros y eficientes, pero a menudo carecen de la "intuición" o estrategias de alto nivel que poseen los LLMs.

Pregunta de Investigación: ¿Es posible extraer las estrategias de prueba internas de los LLMs y formalizarlas para mejorar la capacidad de los probadores simbólicos, sin depender de los LLMs durante la fase de prueba en línea?

2. Metodología: Strat2Rocq

Los autores proponen Strat2Rocq, un marco de trabajo que extrae estrategias de LLMs y las convierte en lemas formales reutilizables en el lenguaje Rocq (Coq). El proceso se divide en dos etapas:

Etapa 1: Minería de Lemas Offline (Extracción de Estrategias)
En esta fase, se procesa un conjunto de teoremas de entrenamiento para extraer el conocimiento interno del LLM:

1. Generación de Prueba en Lenguaje Natural (NL): Para cada teorema, se solicita al LLM (usando prompts detallados con definiciones de tipos y funciones) que genere una prueba paso a paso en lenguaje natural. Se elige NL porque refleja mejor el proceso de razonamiento interno del modelo que un intento directo de generar código formal.
2. Generalización y Formalización: Se solicita al LLM que generalice los pasos de la prueba en NL para convertirlos en lemas generales y luego los formalice en Rocq.
3. Agente de Prueba Iterativo: Dado que la autoformalización es propensa a errores, se utiliza un agente de prueba que itera hasta un límite de rondas para corregir errores en los lemas y sus pruebas, asegurando que solo se guarden lemas válidos.

Etapa 2: Demostración de Teoremas Online (Mejora del Prover)
Una vez extraídos los lemas:

• Se inyectan en el contexto de los nuevos teoremas que se desea probar.
• Se utiliza CoqHammer (un probador simbólico de vanguardia para Rocq) para intentar demostrar el teorema objetivo.
• CoqHammer utiliza su mecanismo de selección de lemas (basado en KNN) para recuperar los lemas extraídos relevantes del contexto, permitiéndole aplicar las estrategias aprendidas del LLM sin necesidad de invocar al LLM en tiempo real.

3. Contribuciones Clave

1. Nuevo Problema de Investigación: Plantear la extracción offline de estrategias de LLMs para enriquecer probadores simbólicos, eliminando la necesidad de LLMs en la fase de inferencia.
2. Enfoque de Extracción: Un método novedoso que utiliza pruebas en lenguaje natural como intermediario para generalizar y formalizar estrategias en lemas verificables, superando las dificultades de la autoformalización directa.
3. Implementación y Validación: Desarrollo de Strat2Rocq y validación empírica en proyectos de código abierto de Rocq, demostrando mejoras significativas tanto en probadores simbólicos como en agentes de LLM.

4. Resultados Experimentales

Los experimentos se realizaron sobre un conjunto de datos de 2,394 teoremas de proyectos como CompCert, Coq-Art, Ext-Lib y Vfa.

• Mejora en Probadores Simbólicos (CoqHammer):

  • Strat2Rocq aumentó la tasa de éxito de CoqHammer en un 13.41% en promedio.
  • En el proyecto CompCert (un compilador C certificado), la mejora fue del 17.75%.
  • Mecanismo de mejora: Los lemas extraídos permiten evitar inducciones complejas (que CoqHammer no soporta nativamente) y mejoran la selección de lemas relevantes, transformando problemas difíciles en reducciones algebraicas simples.

• Robustez y Generalización:

  • El método funciona con diferentes LLMs backend (probado con Claude 3.7 Sonnet y o3-mini), obteniendo mejoras similares (~12-13%).
  • La combinación de lemas extraídos de diferentes LLMs mejora aún más el rendimiento, sugiriendo que sus estrategias internas son complementarias.

• Impacto en Agentes de LLM:

  • Curiosamente, los lemas extraídos también mejoraron el rendimiento de un agente de LLM (con RAG) en un 4.00%, reduciendo además el consumo de tokens en un ~5.87% al permitir que CoqHammer resuelva más teoremas por sí solo.

• Análisis de Ablación:

  • Se demostró que la etapa de generación de prueba en lenguaje natural es crítica. Al omitirla y pedir formalización directa, la cantidad de lemas extraídos cayó un 63.56% y el rendimiento general un 6.21%.

5. Significado e Implicaciones

• Seguridad y Eficiencia: Strat2Rocq ofrece una vía para capitalizar la inteligencia de los LLMs manteniendo la seguridad y el bajo costo de los sistemas puramente simbólicos. Esto es vital para la industria del software crítico y entornos con recursos limitados.
• Interpretabilidad de LLMs: El trabajo contribuye a la comprensión de cómo funcionan los LLMs. Al extraer sus estrategias como lemas simbólicos verificables, se crea un modelo aproximado de su comportamiento de razonamiento formal.
• Futuro: La técnica es adaptable a otros probadores simbólicos (como Lean o Isabelle) mediante la traducción de los lemas, prometiendo una mejora generalizada en la automatización de pruebas formales.

En conclusión, Strat2Rocq demuestra que el conocimiento "interno" de los LLMs puede ser destilado en una forma simbólica, segura y reutilizable, cerrando la brecha entre la intuición de los modelos de lenguaje y la rigurosidad de los probadores formales.