🤖 AI

NoTB: Oracle-Free Triage of LLM-Generated RTL via Cross-Model Formal Consensus

L'article présente NoTB, un cadre sans oracle qui exploite la vérification d'équivalence séquentielle à travers de multiples conceptions RTL générées par des LLM pour établir un signal de consensus formel, permettant un triage de haute précision de la correction fonctionnelle sans dépendre de bancs de test ou de références de référence.

Auteurs originaux : Elisavet Lydia Alvanaki, Je Yang, Biruk Seyoum, Luca P. Carloni

Publié 2026-08-25

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Elisavet Lydia Alvanaki, Je Yang, Biruk Seyoum, Luca P. Carloni

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Dans le monde de la conception de puces informatiques, les ingénieurs écrivent traditionnellement du code qui décrit comment l'électricité doit circuler à travers un circuit. Ce code, connu sous le nom de niveau de transfert de registres ou RTL (register-transfer level), sert de plan pour le matériel physique. Depuis des décennies, la création de ce code est un processus méticuleux, piloté par l'humain, où chaque ligne est vérifiée par rapport à une référence de confiance pour garantir que la puce fonctionnera correctement. Récemment, l'intelligence artificielle a commencé à écrire ce code pour nous. Les grands modèles de langage, le même type de technologie capable d'écrire des histoires ou de répondre à des questions, sont désormais sollicités pour générer ces plans de matériel complexes à partir de simples descriptions textuelles. Bien que ces modèles puissent produire de nombreuses versions d'une conception rapidement, un problème critique subsiste : comment les ingénieurs peuvent-ils savoir laquelle de ces conceptions générées par l'IA est réellement fonctionnelle ? Par le passé, la réponse consistait à comparer la production de l'IA à une référence humaine parfaite ou à la soumettre à un test de simulation. Cependant, la création de ces références parfaites est coûteuse et chronophage, et les tests eux-mêmes peuvent parfois manquer des erreurs cachées.

Une équipe de chercheurs de l'Université Columbia a introduit une nouvelle façon de trier ces conceptions générées par l'IA sans avoir besoin d'une référence parfaite ou d'un test pré-écrit. Ils appellent leur système NoTB. Au lieu de s'appuyer sur un juge unique pour décider si une conception est bonne, ou de lancer une simulation qui pourrait manquer une faille critique, NoTB demande à plusieurs modèles d'IA différents d'écrire la même conception de manière indépendante. Il utilise ensuite un outil mathématique rigoureux appelé vérification d'équivalence séquentielle pour voir si les différentes versions se comportent exactement de la même manière sous toutes les conditions possibles. L'idée centrale est que si plusieurs modèles d'IA différents, qui ont été entraînés de manières différentes, arrivent exactement au même comportement, il est hautement probable qu'ils aient trouvé la solution correcte. Cette approche permet aux ingénieurs d'identifier les conceptions les plus fiables tôt dans le processus, économisant ainsi du temps et des ressources avant de s'engager dans la fabrication réelle de la puce.

Les chercheurs ont testé cette méthode sur soixante-dix-huit tâches de conception de matériel différentes. Ils ont utilisé quatre familles distinctes de grands modèles de langage pour générer plusieurs versions de chaque conception. Pour chaque tâche, ils ont comparé les résultats pour voir lesquels étaient mathématiquement identiques. Ils ont constaté que lorsque les conceptions de quatre familles d'IA différentes s'accordaient sur le même comportement, le système était correct près de quatre-vingt-quinze pour cent du temps. Ce haut niveau de confiance s'accompagnait d'un compromis : le système n'a émis une prédiction pour environ vingt-sept pour cent des tâches. Cependant, en abaissant l'exigence à seulement trois familles en accord, le système pouvait couvrir trente-trois pour cent des tâches tout en maintenant un taux de précision de quatre-vingt-sept pour cent. Cela offre aux concepteurs un outil flexible : ils peuvent choisir d'être extrêmement prudents et de n'accepter que les conceptions les plus certaines, ou d'accepter un risque légèrement plus élevé pour faire approuver plus de conceptions pour des tests ultérieurs.

L'étude a également révélé pourquoi les anciennes méthodes de vérification des conceptions d'IA étaient peu fiables. Une approche courante consistait à demander à un second modèle d'IA d'agir comme juge et de prédire si une conception était correcte. Les chercheurs ont constaté que cette méthode était incohérente ; une même conception pouvait être marquée comme correcte par un juge et incorrecte par un autre, selon le modèle d'IA effectuant le jugement. Une autre méthode consistait à soumettre les conceptions à un test créé par une IA. Les chercheurs ont découvert que la qualité des résultats dépendait entièrement de la qualité de ce test. Si le test était faible, il pouvait ne pas détecter les erreurs, amenant le système à croire qu'une conception défectueuse était en fait correcte. En revanche, la nouvelle méthode ne repose ni sur un test ni sur un juge. Elle repose sur le fait que les conceptions sont prouvées identiques sur toute la plage des entrées possibles, faisant de l'accord une propriété de la conception plutôt que de l'outil utilisé pour la vérifier.

Pour rendre ce processus efficace, le système utilise une technique de filtrage intelligente. Au lieu de comparer chaque paire de conceptions, ce qui prendrait beaucoup de temps, il supprime d'abord les doublons exacts et regroupe ensuite les conceptions qui ont déjà été prouvées identiques. Cela réduit considérablement le nombre de comparaisons nécessaires. L'ensemble du processus, de la génération des conceptions à la vérification, prend en moyenne entre une et seize minutes par tâche, selon le nombre de versions générées. Le coût de fonctionnement de ce système est également gérable, car il évite le besoin d'appels répétés et coûteux aux modèles d'IA pour agir comme juges. Les chercheurs soulignent que cette méthode ne remplace pas la nécessité d'une vérification finale. Elle agit plutôt comme un système de triage, une façon de trier la pile de conceptions générées par l'IA afin que les plus prometteuses puissent progresser avec confiance, tandis que les plus incertaines sont mises de côté pour une vérification plus traditionnelle et approfondie.

Les conclusions suggèrent que la diversité des modèles d'IA utilisés est la clé du succès du système. Les chercheurs ont testé ce qui se passerait si l'on retirait une des quatre familles d'IA de l'ensemble. Ils ont constaté que le système restait robuste et précis même lorsqu'un modèle manquait, prouvant que le signal de confiance provient de l'accord collectif du groupe plutôt que de la dépendance à un seul modèle. Cela rend l'approche pratique pour une utilisation réelle, où l'accès à des modèles d'IA spécifiques peut varier. L'étude conclut qu'en déplaçant l'attention des tests simulés vers la preuve mathématique formelle de l'accord, les ingénieurs peuvent construire un pipeline plus fiable pour l'utilisation de l'intelligence artificielle dans la conception de matériel. Cela permet à l'industrie de tirer parti de la vitesse de génération de l'IA tout en maintenant les normes de sécurité rigoureuses requises pour les puces complexes qui alimentent la technologie moderne.

Résumé Technique : NoTB – Tri sans oracle de RTL généré par LLM via le consensus formel inter-modèles

Énoncé du Problème
Les grands modèles de langage (LLM) sont de plus en plus capables de générer des conceptions de registres de transfert de données (RTL) synthétisables à partir de spécifications en langage naturel. Cependant, un goulot d'étranglement critique subsiste : évaluer la correction fonctionnelle de ces conceptions générées tôt dans le processus sans accès à un « oracle » de confiance (tel qu'un banc de test de référence ou un modèle RTL doré). La construction de tels oracles est coûteuse et sujette à l'erreur, et ils sont souvent indisponibles au début d'une tâche de conception.

Les approches existantes sans oracle souffrent de limitations fondamentales :

LLM-as-a-Judge (Le LLM comme juge) : Remplace l'exécution par une prédiction basée sur le modèle, mais manque de garanties formelles et présente un biais fort dépendant du modèle, entraînant des taux de faux positifs incohérents (variant jusqu'à 45 % selon les modèles).
Auto-cohérence basée sur la simulation : Repose sur l'accord comportemental sous des bancs de test générés par LLM. Cette approche suppose que le banc de test couvre l'espace d'entrée pertinent et que les implémentations incorrectes divergent les unes des autres. En pratique, des bancs de test faibles peuvent manquer des entrées critiques, permettant à des conceptions incorrectes de former un « faux consensus », tandis que des modes d'erreur partagés peuvent amener plusieurs modèles à converger vers le même comportement erroné.

Méthodologie : Le cadre NoTB
Les auteurs introduisent NoTB, un cadre qui remplace l'accord heuristique par un consensus formel inter-modèles. L'idée centrale est que si des implémentations produites par des familles de LLM formées de manière indépendante sont prouvées équivalentes sur l'intégralité de l'espace d'entrée via la vérification d'équivalence séquentielle (SEC), leur accord est une propriété des conceptions elles-mêmes, et non d'un ensemble fini de vecteurs de test.

Le flux de travail NoTB se compose de quatre étapes :

Génération de RTL multi-modèles : Pour une spécification donnée, le système échantillonne plusieurs implémentations RTL à partir de $M$ familles de LLM entraînées indépendamment (ex: Claude, GPT, Gemini, Qwen). Chaque modèle génère $K$ candidats, créant un ensemble de candidats diversifié $D(s)$ .
Clustering d'équivalence formelle : NoTB construit un graphe où les nœuds sont des implémentations candidates et les arêtes représentent une équivalence prouvée. Il utilise un outil formel (Cadence JasperGold) pour effectuer une vérification d'équivalence séquentielle (SEC) sur des paires de conceptions.
- Deux conceptions sont connectées uniquement si l'outil prouve qu'elles produisent des sorties identiques pour toutes les séquences d'entrées.
- Les résultats inconcluants ou les discordances d'interface ne créent pas d'arêtes.
- Les composantes connexes dans ce graphe forment des clusters d'équivalence.
Élagage incrémental : Pour gérer le coût computationnel ( $O(|D|^2)$ $O (∣ D ∣^{2})$ ), NoTB emploie un élagage léger :
- Les fichiers syntaxiquement identiques sont fusionnés via hachage avant la SEC.
- Une structure de données union-find suit les composantes d'équivalence ; une fois qu'une paire est prouvée équivalente, les comparaisons futures au sein de cette composante sont ignorées.
- Les non-équivalences prouvées entre les représentants de composantes empêchent les vérifications redondantes entre les composantes.
Score de confiance via la diversité des modèles : Le système identifie le plus grand cluster d'équivalence ( $C^*$ $C^{*}$ ) pour une spécification. Le score de confiance est défini par le nombre de modèles : le nombre de familles de LLM distinctes représentées dans ce cluster.
- Un nombre de modèles plus élevé indique que des modèles indépendants avec des biais inductifs différents ont convergé vers un même comportement formellement prouvé.
- Les concepteurs peuvent fixer un seuil $\tau$ (ex: $\tau=4$ ) pour n'accepter que les spécifications où le cluster dominant contient des implémentations provenant d'au moins $\tau$ familles distinctes. Cela crée un compromis ajustable entre précision (confiance) et couverture (nombre de spécifications acceptées).

Contributions Clés

Démonstration de la dépendance aux bancs de test : L'article montre que le triage sans oracle basé sur la simulation est hautement sensible au générateur de banc de test. Sur un pool de candidats fixe, la précision d'un consensus de quatre voies variait de 43 % à 84 % uniquement en fonction du LLM générant le banc de test.
Introduction de NoTB : Un cadre novateur qui substitue l'accord appris ou par simulation par un consensus formel inter-modèles. Il clustérise les candidats par SEC et les évalue par la diversité des familles de LLM dans le cluster.
Signal de correction calibré : Des preuves empiriques démontrent que le nombre de modèles est un signal calibré pour la correction. Le système démontre une relation monotone : un accord formel inter-modèles plus fort est corrélé à des taux d'erreur empiriques plus faibles.

Résultats Expérimentaux
Évalué sur 78 tâches de génération de RTL du benchmark NVIDIA CVDP en utilisant quatre familles de LLM (Claude 3.7, GPT-OSS-120B, Gemini 2.5, Qwen 3) avec 5 échantillons chacune :

Consensus de quatre familles ( $\tau=4$ ) : A atteint 94,7 % de précision à 27 % de couverture.
Consensus de trois familles ( $\tau=3$ ) : A atteint 87 % de précision à 33 % de couverture.
Comparaison aux bases de référence :
- LLM-as-a-Judge : A montré une grande instabilité ; les taux de faux positifs variaient considérablement selon le générateur et le modèle juge.
- Clustering basé sur la simulation : La précision fluctuait énormement (43 %–84 %) selon le générateur de banc de test, alors que la SEC formelle restait stable à environ 95 %.
Robustesse : Des études d'ablation "leave-one-out" ont confirmé que le signal de haute précision ne dépend pas d'une seule famille de modèles spécifique ; la haute précision était maintenue même lorsqu'une famille était retirée.
Coût : Bien que la SEC nécessite un temps de calcul important (médiane de 1 à 16 minutes par spécification selon les échantillons), elle évite les coûts de jetons massifs associés à l'exécution de milliers d'appels de "juge" ou à la génération de multiples bancs de test pour chaque candidat.

Signification et Revendications
L'article affirme que NoTB fournit une base fiable et sans oracle pour un triage de haute confiance dans les premières étapes de la conception matérielle. En exploitant les garanties formelles plutôt que les heuristiques apprises ou les vecteurs de test finis, NoTB permet aux concepteurs de certifier sélectivement un sous-ensemble de conceptions RTL générées qui sont probablement correctes, permettant ainsi de contourner les vérifications précoces ou de les prioriser pour la vérification finale. Les auteurs soulignent que NoTB ne remplace pas le besoin d'un oracle de confiance ou d'un flux de vérification complet ; il agit plutôt comme un filtre pour identifier les candidats de haute confiance avant qu'une référence dorée ne soit disponible. La méthode est présentée comme une solution pratique au problème du "triage", offrant un contrôle explicite sur le compromis risque-couverture sans nécessiter d'oracles dépendants des modèles.

Articles similaires