Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?

1. Planteamiento del Problema

La Verificación Formal (FV) es crítica para garantizar la corrección de los diseños de hardware (RTL). Sin embargo, verificar diseños industriales complejos sigue siendo un cuello de botella debido a la naturaleza "a nivel de bits" de la mayoría de las herramientas de comprobación de modelos. Estas herramientas luchan por construir pruebas matemáticas de alto nivel, agnósticas a los bits, requeridas para propiedades complejas.

El enfoque estándar para resolver esto es la Demostración por Inducción, que requiere lema auxiliares (reforzamientos inductivos) para probar una propiedad. Actualmente, generar estos lemas es una tarea manual y laboriosa realizada por ingenieros expertos en FV. El artículo aborda la pregunta: ¿Pueden los Modelos de Lenguaje Grandes (LLM) automatizar la extracción de estos lemas auxiliares para construir argumentos inductivos válidos para la verificación de hardware?

2. Metodología: Un Enfoque Neurosimbólico

Los autores proponen un marco neurosimbólico que combina las capacidades generativas de los LLM con el rigor de las herramientas simbólicas formales. El sistema no depende únicamente de la salida del LLM; en su lugar, utiliza al LLM para generar candidatos y a un solucionador formal para verificarlos y filtrarlos.

A. Componentes Principales

1. Marcos de Prompting para LLM: Se utilizan dos estrategias distintas para generar lemas candidatos:

   • No Agente (Prompt Único): Utiliza un prompt de Few-Shot que contiene $k$ ejemplos de tripletes (Diseño RTL, Propiedad, Lemas Inductivos). Los ejemplos se seleccionan mediante similitud semántica (usando transformadores de oraciones) de un pool pre-construido de Cadena de Pensamiento (CoT). El LLM se muestrea $n$ veces con el mismo prompt para recopilar candidatos diversos.
   • Agente (Interacción Iterativa): Enmarca la generación de lemas como un bucle. El LLM propone lemas, que son verificados por la herramienta formal. Si la verificación falla, la herramienta proporciona retroalimentación (indicando qué lemas fallaron y por qué) y un mensaje de "reparación". El LLM luego refina sus sugerencias en turnos posteriores (hasta 5 iteraciones).

2. Algoritmo de Razonamiento Formal (FINDINDSTRENGTH):

   • Este algoritmo toma el conjunto de lemas candidatos generados por el LLM e intenta encontrar un subconjunto que forme un Reforzamiento Inductivo válido.
   • Reforzamiento Inductivo: Un conjunto de lemas $L$ tal que $L \land \text{Propiedad}$ es un invariante inductivo (satisface la iniciación y la consecución).
   • Proceso:
     1. Filtrado: Verifica si los lemas individuales son invariantes inductivos (usando 1-inducción) o se mantienen hasta una profundidad acotada (usando Comprobación de Modelos Acotada, BMC).
     2. Ordenamiento: Prioriza los lemas conocidos como invariantes inductivos sobre aquellos que solo se mantienen dentro de un límite.
     3. Búsqueda de Subconjunto: Itera a través de los prefijos de la lista ordenada para encontrar el subconjunto más pequeño que, al conjuntarse con la propiedad objetivo, forme un invariante inductivo válido.
   • Herramientas: Implementado utilizando EBMC (una herramienta de verificación formal) con $k$-inducción y BMC.

B. Conjunto de Datos

El marco se evaluó en 110 tareas de verificación que comprenden:

• 58 diseños SystemVerilog (de fuentes como VCEGAR, VIS, v2c, y diseños personalizados de FIFO/Arbiter/CAM).
• 47 ejemplos derivados de programas C: Código C traducido a Máquinas de Estados Finitos (FSM) en SystemVerilog para probar la generalización.
• Pool CoT: Un pequeño conjunto de ejemplos escritos manualmente utilizados para el prompting de Few-Shot.

3. Contribuciones Clave

1. Generación Neurosimbólica de Lemas: Demuestra el primer caso de uso de LLM específicamente para extraer lemas auxiliares para construir pruebas formales en verificación de hardware.
2. Marco de Prompting Dual: Implementa y compara un enfoque estático de Few-Shot contra un enfoque Agente iterativo, mostrando que este último puede guiar al LLM lejos de caminos incorrectos.
3. Evaluación Empírica: Proporciona un estudio exhaustivo en 110 tareas, destacando que los LLM pueden generar con éxito argumentos inductivos no triviales para diseños RTL de código abierto de tamaño medio.
4. Manejo de Alucinaciones: Demuestra que, aunque los LLM alucinan (produciendo lemas sintácticamente inválidos o lógicamente incorrectos), una capa de filtrado formal puede extraer eficazmente las pruebas correctas del ruido.

4. Resultados Experimentales

Los experimentos se realizaron en instancias de Amazon EC2 utilizando seis LLM de última generación (GPT-5, Claude 3.7, Claude 4 Sonnet, Claude 4.5 Sonnet, Claude 4.5 Haiku, Claude 4.5 Opus).

• Tasa de Éxito: El marco generó con éxito argumentos inductivos demostrablemente correctos para el 84% de las 110 tareas de verificación.
  • Configuración Agente: Resolvió 92/110 ejemplos (tasa de éxito del 84%).
  • Configuración No Agente: Resolvió 84/110 ejemplos (tasa de éxito del 76%).
• Rendimiento del Modelo: Claude 4.5-Opus tuvo el mejor rendimiento, resolviendo 88 ejemplos en la configuración Agente.
• Comparación con Herramientas SOTA:
  • Los autores identificaron 31 "benchmarks" desafiantes donde las herramientas industriales de última generación (JasperGold, VC-Formal, rIC3) fallaron en probar la propiedad dentro de un tiempo de espera de 10 minutos.
  • El enfoque basado en LLM resolvió instancias que estas herramientas SOTA no pudieron, particularmente en casos que requerían reforzamientos inductivos complejos (por ejemplo, diseños específicos de FIFO y Arbiter).
  • En algunos casos donde el LLM encontró el lema correcto pero la verificación formal agotó el tiempo de espera, el resultado se consideró aún un éxito en términos de generación de lemas, ya que el cuello de botella fue el tiempo de ejecución de la herramienta de verificación, no el razonamiento del LLM.
• Análisis de Errores:
  • Los LLM ocasionalmente alucinaron sintaxis SVA (por ejemplo, operadores inválidos, variables no definidas) o utilizaron caracteres no ASCII.
  • La configuración Agente fue más eficiente, encontrando a menudo soluciones con menos lemas totales al refinar iterativamente el espacio de búsqueda.

5. Significado e Impacto

• Valor Industrial: Este enfoque tiene el potencial de reducir significativamente el esfuerzo manual requerido por los ingenieros de Verificación Formal. Al automatizar el descubrimiento de lemas auxiliares, reduce la barrera para aplicar métodos formales a diseños de hardware complejos.
• Más allá de la Memorización: Los resultados sugieren que los LLM están realizando un razonamiento genuino en lugar de una simple memorización, ya que generalizaron con éxito a ejemplos derivados de C y manejaron variaciones en la instanciación de parámetros y la nomenclatura de registros.
• Futuras Direcciones: Los autores planean extender el marco para manejar múltiples propiedades simultáneamente, escalar a diseños industriales más grandes y validar el enfoque en un entorno industrial real.

Conclusión: El artículo establece que los LLM, cuando se acoplan con herramientas de verificación formal en un bucle neurosimbólico, son un método viable y poderoso para automatizar la parte más difícil de las pruebas de inducción de hardware: el descubrimiento de lemas auxiliares.