IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking

Ce papier présente IC3-Evolve, un cadre d'évolution de code hors ligne utilisant un LLM pour optimiser automatiquement l'algorithme IC3 de vérification matérielle via des correctifs validés par des preuves ou des contre-exemples, garantissant ainsi l'absence de dépendance aux modèles d'IA lors de l'exécution tout en améliorant les performances sur des benchmarks industriels.

L'essentiel

🏗️ Le Problème : L'Architecte et le Bâtiment

Imaginez que vous construisez un gratte-ciel (un circuit électronique complexe). Avant de le construire, vous devez vous assurer qu'il ne s'effondrera jamais, même lors d'un ouragan ou d'une tempête de neige (des situations rares et extrêmes).

Pour cela, vous utilisez un inspecteur de sécurité très intelligent (appelé IC3 dans le monde réel). Cet inspecteur vérifie chaque étage, chaque poutre et chaque coin.

• S'il trouve un défaut, il dit : "DANGER !" et vous montre exactement où le bâtiment va s'effondrer.
• S'il ne trouve rien, il dit : "SÉCURITÉ !" et vous donne un certificat officiel prouvant que le bâtiment est solide.

Le souci ? Cet inspecteur est très bon, mais il est aussi un peu lent et capricieux. Son efficacité dépend de milliers de petits "réglages" (comme la façon dont il choisit par où commencer, ou combien de temps il passe à vérifier une poutre).
Aujourd'hui, pour améliorer cet inspecteur, des humains experts doivent passer des années à ajuster ces boutons à la main. C'est comme essayer de régler une radio en tournant des boutons au hasard : ça prend du temps, c'est fragile, et si on appuie sur le mauvais bouton, tout peut se casser.

---

🤖 La Solution : IC3-Evolve (L'Atelier de Réparation Automatique)

Les auteurs de cette étude ont créé un système appelé IC3-Evolve. Au lieu de laisser un humain ajuster les boutons, ils ont fait appel à un robot très intelligent (une Intelligence Artificielle de type LLM) pour réécrire le code de l'inspecteur.

Mais il y a un piège : si le robot fait une erreur, l'inspecteur pourrait dire "SÉCURITÉ" alors qu'il y a un danger, ce qui serait catastrophique.

Comment ils ont résolu ce problème ? La "Porte de Sécurité"

C'est ici que l'idée devient géniale. Ils ont installé une porte de sécurité infaillible (qu'ils appellent Proof-/Witness-Gated Validation) entre le robot et le monde réel.

Voici comment ça marche, étape par étape :

1. Le Robot Propose : L'IA lit le code de l'inspecteur et dit : "J'ai une idée ! Si on change ce petit bouton ici, l'inspecteur ira plus vite." Elle propose une petite modification (un "patch").
2. Le Test Rigoureux (La Porte de Sécurité) : Avant même de voir si c'est plus rapide, le système teste la modification avec deux règles strictes :
   • Si l'inspecteur dit "DANGER" : Il doit fournir une preuve vidéo (une trace) que l'on peut rejouer pour voir l'effondrement. Si la vidéo ne correspond pas à la réalité, le robot est éliminé.
   • Si l'inspecteur dit "SÉCURITÉ" : Il doit fournir un certificat mathématique vérifiable par un autre système indépendant. Si le certificat est faux, le robot est éliminé.
3. Le Résultat : Si la modification passe ces deux tests, elle est acceptée. Sinon, elle est jetée à la poubelle, même si elle semblait plus rapide.

L'analogie du Chef Cuisinier :
Imaginez un chef cuisinier (l'IA) qui essaie de créer une nouvelle recette pour un plat très délicat.

• Il propose d'ajouter un ingrédient secret pour que ça cuise plus vite.
• Mais avant de servir le plat aux clients, un dégustateur officiel (la porte de sécurité) goûte.
• Si le plat est empoisonné (faux positif), le chef est viré.
• Si le plat est juste bon mais pas sûr, il est rejeté.
• Seul le plat sûr ET meilleur est gardé.

---

🚀 Les Résultats : Un Moteur Plus Puissant, Sans Robot

Après des centaines d'essais et d'erreurs (tous filtrés par la porte de sécurité), le système a produit un nouvel inspecteur, IC3-Evolve.

• Il est plus rapide : Il trouve les défauts ou prouve la sécurité beaucoup plus vite que les versions précédentes.
• Il est autonome : Une fois le travail terminé, le robot (l'IA) est retiré. Le nouvel inspecteur est un logiciel classique, tout seul, sans avoir besoin d'Internet ou d'une IA pour fonctionner. C'est comme si le robot avait écrit le manuel d'instructions, puis s'était effacé.
• Il est fiable : Grâce à la "porte de sécurité", on est certain à 100 % qu'il ne fait pas d'erreurs de jugement.

🌟 En Résumé

Cette recherche montre qu'on peut utiliser l'Intelligence Artificielle pour améliorer des logiciels de sécurité critique, sans jamais compromettre la sécurité.

Au lieu de laisser l'IA prendre des décisions en temps réel (ce qui est risqué et lent), on l'utilise en arrière-plan pour réécrire le code, puis on vérifie chaque changement avec des règles mathématiques strictes. Le résultat est un outil de vérification plus rapide, plus intelligent, mais qui fonctionne de manière simple et fiable, comme une machine bien huilée.

C'est comme si on avait laissé un architecte robot réinventer les fondations d'un pont, mais qu'on avait obligé chaque nouvelle brique à passer un test de résistance avant d'être posée. Résultat : un pont plus solide, construit plus vite, sans qu'il y ait de robot sur le chantier une fois fini.

Résumé technique

1. Problématique

La vérification formelle des circuits matériels, et plus spécifiquement le model checking de sécurité (vérification de propriétés de sûreté), repose souvent sur l'algorithme IC3 (également connu sous le nom de Property-Directed Reachability ou PDR). Bien que IC3 soit un algorithme de pointe capable de prouver la sécurité (SAFE) ou de trouver des contre-exemples (UNSAFE), ses performances pratiques sont extrêmement dépendantes d'un réseau complexe d'heuristiques et de choix d'implémentation (gestion des obligations de preuve, généralisation des clauses, interactions avec les moteurs SAT, etc.).

Les défis majeurs identifiés sont :

• Coût et fragilité du réglage manuel : L'optimisation manuelle de ces heuristiques est laborieuse, coûteuse et fragile. Une amélioration sur un type d'instances peut entraîner des régressions sur d'autres.
• Limites des approches ML en ligne : Les méthodes précédentes intégrant l'apprentissage automatique (ML) directement dans la boucle de vérification (pour prédire des clauses ou guider la recherche) introduisent des coûts d'inférence, de la latence et des problèmes de reproductibilité, ce qui les rend difficiles à déployer dans des flux industriels.
• Besoin de robustesse : Les solutions basées sur le ML doivent garantir une correction absolue (soundness), ce qui est difficile à assurer lorsque le modèle influence directement le processus de preuve.

2. Méthodologie : IC3-Evolve

Le papier propose IC3-Evolve, un cadre de évolution de code hors ligne (offline) piloté par un Grand Modèle de Langage (LLM). L'objectif est d'améliorer automatiquement l'implémentation d'un solveur IC3 sans introduire de dépendance au modèle ML lors de l'exécution finale.

Principes clés :

• Évolution de code contrôlée : Le LLM agit comme un agent "programmeur" qui propose de petits correctifs (patches) limités à des slots heuristiques spécifiques (zones de code pré-définies comme la gestion des obligations de preuve, la généralisation inductive, etc.).
• Validation par "Portes de Preuve et de Témoin" (Proof-/Witness-Gated) : C'est le cœur de la sécurité du système. Aucun correctif n'est promu s'il ne passe pas des vérifications rigoureuses :
  • Si le solveur retourne SAFE, il doit produire un invariant inductif vérifiable indépendamment (via l'outil CERTIFAIGER).
  • Si le solveur retourne UNSAFE, il doit produire une trace de contre-exemple rejouable (via AIGSIM).
  • Toute modification qui échoue à produire ces artefacts ou qui échoue à leur vérification est rejetée immédiatement, garantissant que la correction logique (soundness) n'est jamais compromise.
• Stratégie de recherche Compass & Jump : Un agent "évaluateur" analyse les performances (métriques PAR2, nombre d'instances résolues) et génère un MoveSet (liste de recommandations). Une politique de recherche guide le LLM pour explorer soit un seul slot (Compass), soit plusieurs slots simultanément (Jump) pour découvrir des synergies, tout en évitant les régressions.
• Résultat final : Le produit déployé est un solveur IC3 autonome et optimisé. Le LLM n'est utilisé que pendant la phase d'entraînement (hors ligne), éliminant tout coût d'inférence et toute dépendance au modèle lors de la vérification industrielle.

3. Contributions Clés

1. Framework IC3-Evolve : Introduction d'un système d'évolution de code hors ligne qui transforme l'ingénierie des heuristiques IC3 en un processus d'optimisation contrôlé et auditable.
2. Validation par portes rigoureuses : Mise en place d'un protocole où la promotion d'un correctif est conditionnée exclusivement par la réussite de vérifications de preuve (certificats) et de témoin (traces), empêchant le déploiement de modifications non valides.
3. Stratégie Compass & Jump : Développement d'une politique de recherche adaptative qui explore à la fois des raffinements locaux et des changements transversaux entre modules, guidée par des diagnostics automatisés.
4. Preuve de concept industrielle : Démonstration que l'évolution de code peut découvrir des améliorations heuristiques pratiques et généralisables sur des benchmarks publics (HWMCC) et industriels, surpassant les approches de composition naïve.

4. Résultats Expérimentaux

Les expériences ont été menées sur 100 instances publiques du HWMCC (Hardware Model Checking Competition) pour l'évolution, et évaluées sur des ensembles de données non vus (HWMCC Set B) et 302 instances industrielles.

• Performance : IC3-Evolve a considérablement surpassé les bases de référence (IC3ref, ABC, rIC3).
  • Sur l'ensemble HWMCC Set B, il a résolu 94 instances (contre 89 pour le meilleur concurrent rIC3-CaDiCaL) avec un temps moyen pondéré (PAR2) de 464,56 s (contre 524,35 s pour rIC3).
  • Sur les benchmarks industriels, il a résolu 225 instances (contre 182 pour rIC3) avec un PAR2 de 1044,26 s (contre 1449,78 s).
• Étude d'ablation :
  • Les variantes limitées à un seul slot (ex: seulement la gestion des obligations de preuve) ont montré des gains marginaux et instables.
  • La composition naïve des meilleurs correctifs individuels a échoué à atteindre les performances de l'approche complète, prouvant que les heuristiques IC3 sont fortement couplées et nécessitent une évolution coordonnée.
• Sécurité : L'étude de cas "No-gate counterfactual" a montré qu'un correctif qui aurait amélioré les performances sans la porte de validation aurait été rejeté car il produisait des artefacts de preuve invalides, confirmant l'importance cruciale du mécanisme de sécurité.

5. Signification et Impact

Ce travail démontre qu'il est possible d'utiliser les LLM pour l'optimisation d'algorithmes complexes de vérification formelle tout en maintenant des garanties de correction strictes.

• Paradigme de déploiement : Il propose un modèle où le LLM est un outil de conception hors ligne, produisant un artefact final "pur" (sans ML), ce qui résout les problèmes de latence et de reproductibilité des approches "ML-in-the-loop".
• Ingénierie des heuristiques : Il prouve que l'optimisation des solveurs IC3 n'est pas une simple question de réglage de paramètres isolés, mais nécessite une exploration systémique et coordonnée de l'espace de recherche, que l'évolution guidée par LLM peut effectuer efficacement.
• Futur de la vérification : IC3-Evolve ouvre la voie à l'automatisation de l'ingénierie des solveurs formels, permettant de découvrir des combinaisons d'heuristiques robustes qui échapperaient à l'intuition humaine, tout en garantissant que chaque amélioration est mathématiquement justifiée par des preuves vérifiables.