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

1. Énoncé du problème

La Vérification Formelle (VF) est cruciale pour garantir la correction des conceptions matérielles (RTL). Cependant, la vérification de conceptions industrielles complexes reste un goulot d'étranglement en raison de la nature « au niveau des bits » de la plupart des outils de model checking. Ces outils peinent à construire des preuves mathématiques de haut niveau, indépendantes des bits, nécessaires pour des propriétés complexes.

L'approche standard pour résoudre ce problème est la Preuve par Induction, qui nécessite des lemmes auxiliaires (renforcements inductifs) pour prouver une propriété. Actuellement, la génération de ces lemmes est une tâche manuelle et laborieuse effectuée par des ingénieurs experts en VF. Le papier aborde la question suivante : Les Grands Modèles de Langage (LLM) peuvent-ils automatiser l'extraction de ces lemmes auxiliaires pour construire des arguments inductifs valides pour la vérification matérielle ?

2. Méthodologie : Une approche neurosymbolique

Les auteurs proposent un cadre neurosymbolique qui combine les capacités génératives des LLM avec la rigueur des outils symboliques formels. Le système ne repose pas uniquement sur la sortie du LLM ; il utilise plutôt le LLM pour générer des candidats et un solveur formel pour les vérifier et les filtrer.

A. Composants principaux

1. Cadres de prompt pour LLM : Deux stratégies distinctes sont utilisées pour générer des lemmes candidats :

   • Non-Agentic (Prompt unique) : Utilise un prompt Few-Shot contenant $k$ exemples de triplets (Conception RTL, Propriété, Lemmes Inductifs). Les exemples sont sélectionnés par similarité sémantique (en utilisant des transformateurs de phrases) à partir d'un pool pré-construit de Chain-of-Thought (CoT). Le LLM est échantillonné $n$ fois avec le même prompt pour recueillir des candidats diversifiés.
   • Agentic (Interaction itérative) : Cadre la génération de lemmes comme une boucle. Le LLM propose des lemmes, qui sont vérifiés par l'outil formel. Si la vérification échoue, l'outil fournit un retour (indiquant quels lemmes ont échoué et pourquoi) et un message de « réparation ». Le LLM affine ensuite ses suggestions lors des tours suivants (jusqu'à 5 itérations).

2. Algorithme de raisonnement formel (FINDINDSTRENGTH) :

   • Cet algorithme prend l'ensemble des lemmes candidats générés par le LLM et tente de trouver un sous-ensemble qui forme un Renforcement Inductif valide.
   • Renforcement Inductif : Un ensemble de lemmes $L$ tel que $L \land \text{Propriété}$ est un invariant inductif (satisfait l'initiation et la consécutivité).
   • Processus :
     1. Filtrage : Vérifie si les lemmes individuels sont des invariants inductifs (en utilisant l'induction 1-induction) ou s'ils tiennent jusqu'à une profondeur bornée (en utilisant le Model Checking Borné, BMC).
     2. Tri : Priorise les lemmes connus pour être des invariants inductifs par rapport à ceux qui ne tiennent que dans une borne.
     3. Recherche de sous-ensemble : Itère à travers les préfixes de la liste triée pour trouver le plus petit sous-ensemble qui, lorsqu'il est conjugué à la propriété cible, forme un invariant inductif valide.
   • Outils : Implémenté en utilisant EBMC (un outil de vérification formelle) avec l'induction $k$ et le BMC.

B. Jeu de données

Le cadre a été évalué sur 110 tâches de vérification comprenant :

• 58 conceptions SystemVerilog (provenant de sources telles que VCEGAR, VIS, v2c, et des conceptions FIFO/Arbiter/CAM personnalisées).
• 47 exemples dérivés de programmes C : Code C traduit en Machines à États Finis (FSM) SystemVerilog pour tester la généralisation.
• Pool CoT : Un petit ensemble d'exemples écrits à la main utilisés pour le prompt Few-Shot.

3. Contributions clés

1. Génération neurosymbolique de lemmes : Démontre le premier cas d'utilisation de LLM spécifiquement pour extraire des lemmes auxiliaires afin de construire des preuves formelles en vérification matérielle.
2. Cadre de prompt dual : Implémente et compare une approche statique Few-Shot à une approche Agentic itérative, montrant que cette dernière peut orienter le LLM loin des chemins incorrects.
3. Évaluation empirique : Fournit une étude complète sur 110 tâches, mettant en évidence que les LLM peuvent générer avec succès des arguments inductifs non triviaux pour des conceptions RTL open-source de taille moyenne.
4. Gestion des hallucinations : Prouve que bien que les LLM hallucinent (produisant des lemmes syntaxiquement invalides ou logiquement incorrects), une couche de filtrage formel peut extraire efficacement les preuves correctes du bruit.

4. Résultats expérimentaux

Les expériences ont été menées sur des instances Amazon EC2 utilisant six LLMs de pointe (GPT-5, Claude 3.7, Claude 4 Sonnet, Claude 4.5 Sonnet, Claude 4.5 Haiku, Claude 4.5 Opus).

• Taux de réussite : Le cadre a généré avec succès des arguments inductifs prouvés corrects pour 84 % des 110 tâches de vérification.
  • Configuration Agentic : A résolu 92/110 exemples (taux de réussite de 84 %).
  • Configuration Non-Agentic : A résolu 84/110 exemples (taux de réussite de 76 %).
• Performance des modèles : Claude 4.5-Opus a obtenu les meilleurs résultats, résolvant 88 exemples dans la configuration Agentic.
• Comparaison avec les outils SOTA :
  • Les auteurs ont identifié 31 benchmarks « difficiles » où les outils industriels de pointe (JasperGold, VC-Formal, rIC3) ont échoué à prouver la propriété dans un délai de 10 minutes.
  • L'approche basée sur les LLM a résolu des instances que ces outils SOTA ne pouvaient pas résoudre, en particulier dans les cas nécessitant des renforcements inductifs complexes (par exemple, des conceptions FIFO et Arbiter spécifiques).
  • Dans certains cas où le LLM trouvait le bon lemme mais où la vérification formelle dépassait le délai, le résultat était toujours considéré comme une réussite en termes de génération de lemmes, car le goulot d'étranglement était le temps d'exécution de l'outil de vérification et non le raisonnement du LLM.
• Analyse des erreurs :
  • Les LLM hallucinaient occasionnellement la syntaxe SVA (par exemple, opérateurs invalides, variables non définies) ou utilisaient des caractères non ASCII.
  • La configuration Agentic était plus efficace, trouvant souvent des solutions avec moins de lemmes totaux en affinant itérativement l'espace de recherche.

5. Signification et impact

• Valeur industrielle : Cette approche a le potentiel de réduire considérablement l'effort manuel requis par les ingénieurs en Vérification Formelle. En automatisant la découverte de lemmes auxiliaires, elle abaisse la barrière à l'application des méthodes formelles à des conceptions matérielles complexes.
• Au-delà de la mémorisation : Les résultats suggèrent que les LLM effectuent un raisonnement véritable plutôt qu'une simple mémorisation, car ils généralisent avec succès aux exemples dérivés de C et gèrent les variations dans l'instanciation des paramètres et la dénomination des registres.
• Perspectives futures : Les auteurs prévoient d'étendre le cadre pour gérer plusieurs propriétés simultanément, de le mettre à l'échelle pour des conceptions industrielles plus grandes et de valider l'approche dans un environnement industriel réel.

Conclusion : Le papier établit que les LLM, lorsqu'ils sont couplés à des outils de vérification formelle dans une boucle neurosymbolique, constituent une méthode viable et puissante pour automatiser la partie la plus difficile des preuves d'induction matérielle : la découverte de lemmes auxiliaires.