Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair

Imaginez que vous construisez un château massif et complexe avec des briques Lego numériques. C'est ce que font les ingénieurs lorsqu'ils conçoivent des puces informatiques : ils écrivent du code appelé RTL (Register Transfer Level) qui dicte le comportement des minuscules transistors. Mais voici le hic : si une seule brique est placée au mauvais endroit, tout le château pourrait s'effondrer lorsque l'on allume l'alimentation. Vérifier ces erreurs est la partie la plus difficile du travail, occupant souvent plus de la moitié du temps. Traditionnellement, les ingénieurs utilisent deux méthodes principales pour vérifier leur travail. La première est semblable à un « essai routier », où ils soumettent la puce à quelques scénarios spécifiques pour voir si elle casse. La seconde est la « vérification formelle », qui est une sorte de preuve mathématique super puissante garantissant que le château tiendra debout dans toutes les conditions possibles, et pas seulement celles qu'ils ont testées. Cependant, cette méthode de super-preuve nécessite généralement des logiciels coûteux et verrouillés que seules les grandes entreprises peuvent s'offrir.

Entrez le nouveau venu sur la scène : les Grands Modèles de Langage (LLM). Vous les connaissez peut-être comme les chatbots d'IA qui savent écrire des histoires ou du code. Récemment, des gens ont commencé à se demander : « Un IA peut-elle être l'architecte capable de réparer nos châteaux numériques brisés ? » La grande question est de savoir si une IA peut non seulement repérer une erreur, mais aussi la corriger d'une manière mathématiquement prouvée comme étant parfaite, sans avoir besoin d'acheter une licence de logiciel à un million de dollars. Ce document plonge dans cette question, tentant de construire un pont entre la créativité de l'IA et la logique stricte et inflexible des mathématiques formelles, en utilisant uniquement des outils gratuits et open-source.

Le détective IA et la boîte à outils open-source

Dans cette étude, un chercheur nommé Ha Trung Tran a conçu une équipe intelligente d'agents d'IA pour agir comme une équipe de réparation pour les conceptions de puces défectueuses. Voyez cela comme une escouade de détectives de haute technologie travaillant en boucle. Au lieu d'une seule IA essayant de tout faire à la fois, l'équipe est divisée : un agent lit les plans, un autre écrit les règles de ce que la puce devrait faire, un troisième vérifie le travail, et un quatrième répare réellement le code.

Le ingrédient secret ici est la façon dont ils vérifient les erreurs. La plupart des outils de réparation par IA se contentent de lancer quelques essais routiers (simulations) pour voir si la puce fonctionne. Mais cette équipe utilise un « backend formel » — un moteur mathématique gratuit et open-source composé d'outils appelés Yosys, SymbiYosys et Z3. Ce moteur ne se contente pas de deviner ; il tente de prouver mathématiquement que la puce est correcte. Si la puce échoue, le moteur ne dit pas simplement « c'est cassé ». Il remet à l'IA un « contre-exemple » spécifique, qui est comme une rediffusion vidéo montrant exactement comment le château s'est effondré. L'IA regarde ensuite cette vidéo, comprend ce qui a mal tourné, et tente de réparer. Ils répètent ce processus — vérifier, trouver le crash, réparer, vérifier à nouveau — jusqu'à ce que les mathématiques prouvent que la puce est parfaite ou qu'ils manquent d'essais.

La bonne nouvelle : Ça fonctionne (parfois)

Les chercheurs ont testé ce système sur six types différents de conceptions numériques, allant d'une partie simple de calculatrice (un ALU) à des contrôleurs de trafic et des unités de mémoire plus complexes. Les résultats sont un mélange de triomphe et de limites claires.

La star du spectacle était l'ALU (Unité Arithmétique et Logique), qui est comme le cerveau de calculatrice d'une puce. Les chercheurs l'ont intentionnellement cassée en remplaçant une opération « ET » par une opération « OU ». L'équipe d'IA a repéré l'erreur immédiatement. En seulement deux cycles de vérification et de réparation, ils ont réparé le code. Plus important encore, le moteur mathématique open-source a prouvé avec une certitude de 100 % que la correction était exacte pour chaque nombre possible que la puce pourrait traiter. Cela s'est produit lors des cinq tests, prenant en moyenne seulement 16,5 secondes. Cela a prouvé que l'idée fonctionne : une IA, guidée par des outils mathématiques open-source, peut trouver et réparer un véritable bug avec une garantie mathématique.

La mauvaise nouvelle : Là où l'IA s'est bloquée

Cependant, l'histoire n'est pas une victoire totale. Lorsque les chercheurs ont tenté le même processus sur les cinq autres conceptions, l'équipe d'IA s'est heurtée à un mur. Ils n'ont pas pu les réparer de manière fiable. Le document analyse soigneusement pourquoi ils ont échoué, identifiant quatre « modes de défaillance » distincts qui agissent comme des pièges pour l'IA :

1. Le piège de la « profondeur excessive » (Vacuité de couverture bornée) : Dans un cas (un compteur), le moteur mathématique a indiqué « ÉCHEC » alors que la correction était en réalité correcte. Pourquoi ? Parce que la conception avait besoin de fonctionner pendant 256 cycles pour atteindre un état spécifique, mais l'outil n'a regardé que 256 cycles de profondeur. C'était comme essayer de prouver qu'une voiture peut traverser le pays en ne la faisant rouler qu'un kilomètre ; l'outil ne pouvait pas voir la destination, donc il a abandonné. Le document note que c'est une limite de l'outil, et non de l'IA.
2. Le piège des « instructions confuses » (Ambiguïté de spécification) : Pour une autre conception (un arbitre), l'IA a essayé de suivre les règles écrites, mais les règles demandaient quelque chose d'impossible (comme un feu de signalisation qui change sans horloge). L'IA a fidèlement suivi les instructions impossibles, menant à une impasse.
3. Le piège du « voyage dans le temps » (Bugs de logique temporelle) : Dans deux cas (un émetteur UART et une mémoire FIFO), les bugs concernaient des événements se produisant sur plusieurs étapes temporelles. L'IA était excellente pour réparer la logique à étape unique (comme la calculatrice), mais elle avait du mal à raisonner sur des séquences d'événements se déroulant dans le temps.
4. Le piège des « trop nombreuses règles » (Pression multi-propriétés) : Dans le dernier cas (un esclave AXI Lite), il y avait tellement de règles que la puce devait respecter simultanément que réparer une règle en brisait une autre. L'IA s'est retrouvée coincée dans une boucle, incapable de trouver une solution qui satisfasse tout le monde.

Un bug caché dans la boîte à outils

Il y a également eu une découverte surprenante concernant les outils open-source eux-mêmes. Les chercheurs ont découvert que l'outil Yosys, qui aide à traiter le code, possède une particularité cachée. Si vous essayez d'attacher les vérifications de sécurité (assertions) à la conception en utilisant une méthode spécifique appelée « bind », l'outil les ignore silencieusement. C'est comme installer une caméra de surveillance dans une pièce mais avoir la caméra débranchée ; le système pense que tout va bien parce qu'il ne voit jamais la caméra. Les chercheurs ont dû changer leur méthode pour « injecter » les vérifications directement dans le code pour s'assurer que le moteur mathématique les voie réellement. C'est un conseil utile pour quiconque utilise ces outils gratuits.

L'essentiel

Ce document est une « étude de faisabilité », ce qui est une façon élégante de dire : « Nous avons essayé, et voici exactement où cela fonctionne et où cela échoue. » La conclusion principale est qu'il est possible d'utiliser une IA pour réparer des conceptions de puces avec une preuve mathématique de correction, mais seulement si vous utilisez des outils open-source et si le problème n'est pas trop complexe.

L'auteur est honnête quant aux limites : le système est excellent pour réparer des erreurs de logique simples et immédiates (comme la calculatrice), mais il éprouve actuellement des difficultés avec les problèmes de synchronisation complexes, les états de mémoire profonds ou les conceptions avec des règles conflictuelles. Il ne prétend pas avoir résolu le problème de la réparation de puces ; il a plutôt tracé une carte claire montant la « zone de sécurité » où l'IA fonctionne et la « zone de danger » où elle se perd. En utilisant uniquement des outils gratuits, ils espèrent abaisser le coût d'entrée pour ce type de recherche, prouvant que vous n'avez pas besoin d'un budget d'un million de dollars pour commencer à construire l'avenir de la conception de matériel fiable.