🤖 machine learning

Reward-Weighted On-Policy Distillation with an Open Property-Equivalence Verifier for NL-to-SVA Generation

Ce document présente la distillation en ligne pondérée par la récompense (RWOPD), une méthode d'entraînement novatrice qui exploite un vérificateur formel d'équivalence de propriétés pour guider un modèle étudiant de 7 milliards de paramètres dans la génération d'assertions SystemVerilog, atteignant ainsi de nouvelles performances de pointe en privilégiant la correction sémantique plutôt que l'imitation au niveau des jetons.

Auteurs originaux : Qingyun Zou, Yingze Li, Tianen Liu, Bingsheng He, Weng-Fai Wong

Publié 2026-05-14

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Qingyun Zou, Yingze Li, Tianen Liu, Bingsheng He, Weng-Fai Wong

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

Imaginez que vous essayiez d'enseigner à un apprenti talentueux mais inexpérimenté (une IA de 7 milliards de paramètres) comment rédiger des contrats juridiques complexes pour des puces électroniques. Ces contrats sont appelés SystemVerilog Assertions (SVA). Ce sont les règles qui indiquent à une puce : « Si ceci se produit, alors cela doit se produire dans les 3 secondes », ou « Ce signal ne doit jamais être à l'état haut ».

Pendant longtemps, les experts ont pensé que les meilleurs modèles d'IA avaient déjà maîtrisé cette tâche, atteignant environ 76 % de précision. Mais les auteurs de cet article ont découvert un défaut caché : l'IA était bonne pour donner l'impression de connaître les règles, mais elle se contentait en réalité de mémoriser quelques structures de phrases simples. Face à des règles de temporisation complexes, elle « s'effondrait » vers un modèle générique par défaut qui semblait correct mais était juridiquement erroné.

Voici comment l'article résout ce problème, en utilisant des analogies simples :

1. Le Problème : L'Imitation contre la Compréhension

L'ancienne méthode d'entraînement de ces IA consistait à faire en sorte qu'un élève copie mot pour mot les devoirs de son professeur. L'élève reçoit une note basée sur la proximité de son orthographe et de sa grammaire avec la réponse du professeur.

Le Défaut : Dans ce domaine, deux phrases peuvent sembler complètement différentes mais signifier exactement la même chose (équivalentes). Inversement, deux phrases peuvent sembler presque identiques mais avoir des sens opposés. L'ancienne méthode récompensait l'élève pour la copie des mots, et non pour la compréhension de la logique.

2. La Solution : La « Distillation Pondérée par la Récompense On-Policy » (RWOPD)

Les auteurs ont créé une nouvelle méthode d'entraînement appelée RWOPD. Imaginez-la comme un processus de coaching en trois étapes impliquant un Élève, un Maître Professeur et un Juge strict.

Étape A : L'Élève s'entraîne (On-Policy)

Au lieu de simplement copier le professeur, l'IA Élève est invitée à rédiger ses propres contrats (appelés « rollouts ») à partir d'une consigne. Elle tente d'abord de résoudre le problème par elle-même.

Étape B : Le Juge Strict (Le Vérificateur Ouvert d'Équivalence de Propriété)

C'est l'ingrédient secret de l'article. Les auteurs ont construit un « Juge » open-source (en utilisant des outils appelés SymbiYosys et Z3) qui ne vérifie pas seulement si la grammaire est correcte. Il vérifie la logique.

L'Analogie : Imaginez que le Juge est un avocat qui prend le contrat de l'Élève et le contrat de Référence et les soumet à une simulation.
Le Verdict : Le Juge demande : « Ces deux contrats sont-ils juridiquement équivalents ? »
- Si le contrat de l'Élève est logiquement équivalent à la référence, le Juge dit « Réussi ».
- S'il est légèrement plus strict ou plus laxiste, le Juge donne un « Réussi partiel ».
- S'il est faux, le Juge dit « Échec ».
Point Crucial : Le Juge ignore la réponse de l'Élève si elle est logiquement erronée. Il agit comme un filtre, ne laissant passer que les tentatives « bonnes ».

Étape C : Le Maître Professeur (Distillation)

C'est ici que la magie opère. L'Élève n'apprend pas seulement à partir du score « Réussi/Échec » du Juge.

Le Maître Professeur (une IA beaucoup plus grande, de 14 milliards de paramètres, déjà très performante) examine les tentatives réussies de l'Élève.
Le Professeur dit : « D'accord, vous avez compris la logique. Maintenant, regardez exactement comment j'aurais rédigé ces mots spécifiques. Je vais vous montrer la probabilité de chaque mot que j'aurais choisi. »
L'Élève met alors à jour son cerveau pour correspondre au style du Professeur, mais uniquement sur les tentatives approuvées par le Juge.

Pourquoi est-ce mieux ?

Ancienne Méthode : L'Élève apprend de toutes les tentatives, même des mauvaises, en essayant de deviner les bons mots.
Nouvelle Méthode (RWOPD) : L'Élève n'apprend que des tentatives « gagnantes », et il apprend la logique profonde de la manière dont un Maître formulerait ces réponses gagnantes. C'est comme un élève qui n'étudie que les essais ayant remporté le prix, mais en apprenant du commentaire d'un lauréat du prix Nobel sur pourquoi ces essais étaient bons.

3. Les Résultats : Battre les Géants

Les auteurs ont testé cette méthode sur un modèle de 7 milliards de paramètres (l'Élève).

La Compétition : Ils l'ont comparé au meilleur modèle spécialisé précédent (une IA de 14 milliards de paramètres) et même à des modèles généralistes massifs (671 milliards de paramètres).
Le Résultat : Le petit Élève de 7 milliards de paramètres, utilisant cette nouvelle méthode de coaching, a battu tout le monde. Il a atteint la précision la plus élevée sur les benchmarks, surpassant des modèles 100 fois plus grands.
Le « Creux Caché » Résolu : L'article montre que l'Élève s'est spécifiquement beaucoup amélioré sur les types de règles les plus difficiles (ceux impliquant du temps et des délais), là où les modèles précédents échouaient.

Résumé

L'article soutient que pour enseigner à une IA une logique complexe, il ne faut pas simplement lui faire mémoriser des réponses. Au lieu de cela, vous devriez :

Lui permettre d'essayer de résoudre le problème.
Utiliser un vérificateur de logique strict pour filtrer les mauvaises réponses.
Demander à un Maître Professeur de montrer à l'Élève exactement comment formuler les réponses correctes.

En combinant un vérificateur de logique avec un Maître Professeur, une petite IA peut apprendre à penser comme un géant, résolvant un problème que l'on pensait auparavant presque « saturé » (résolu).

Résumé technique : Distillation en ligne pondérée par la récompense pour la génération de NL vers SVA

Énoncé du problème
La génération d'assertions SystemVerilog (SVA) à partir de spécifications en langage naturel (NL) utilisant des modèles de langage de grande taille (LLM) a atteint un plateau de performance, les modèles spécialisés les plus performants (par exemple CodeV-SVA-14B) obtenant environ 76 % de précision sur le benchmark NL2SVA-Human. Cependant, ce score agrégé masque un « écart temporel » critique. Bien que les modèles performent bien sur la logique combinatoire (C1), ils échouent fréquemment sur les spécifications à délai borné (C2) et de vivacité (C3). Le mode d'échec dominant est l'« effondrement du modèle », où les modèles se rabattent sur un petit ensemble de modèles d'implication (par exemple |->) indépendamment des exigences temporelles spécifiques de la spécification.

La cause racine identifiée réside dans l'objectif d'entraînement. Les systèmes existants reposent sur un ajustement fin supervisé (SFT) sur des paires NL/SVA, qui optimise l'imitation au niveau des jetons d'une seule assertion de référence. Cette approche échoue à capturer la nature sémantique de la correction SVA, où deux assertions peuvent être syntaxiquement éloignées mais sémantiquement équivalentes, ou syntaxiquement similaires mais sémantiquement opposées. De plus, l'apprentissage par renforcement (RL) standard avec rétroaction de vérificateur s'est avéré inefficace dans ce contexte ; les récompenses éparses au niveau des déroulements ne fournissent pas un signal suffisant pour les modèles à petits paramètres (7B) avec des budgets d'adaptation limités (LoRA), échouant souvent à surpasser la ligne de base SFT.

Méthodologie : Distillation en ligne pondérée par la récompense (RWOPD)
L'article propose la Distillation en ligne pondérée par la récompense (RWOPD), une méthode qui intègre un vérificateur formel dans le processus de distillation pour guider un modèle étudiant vers un comportement équivalent aux propriétés. Le pipeline se compose de quatre composants clés :

SFT de curriculum stratifié : Avant la distillation, un modèle étudiant de 7B (Qwen2.5-Coder-7B-Instruct) subit un SFT basé sur un curriculum. Cette étape traite le biais vers les classes temporelles plus faciles en entraînant en trois étapes (C1, C2, C3) avec un tampon de replay pour éviter l'oubli catastrophique. Crucialement, elle emploie une perte d'entropie croisée pondérée par les jetons d'opérateur, qui surpondère les jetons d'opérateurs temporels (par exemple |->, s_eventually) pour s'assurer que le modèle apprend l'importance structurelle de ces jetons.
Vérificateur de propriété d'équivalence ouvert (PEC) : Pour éviter le coût et le caractère propriétaire d'outils industriels comme Cadence JasperGold pendant l'entraînement, les auteurs introduisent un vérificateur open-source construit sur SymbiYosys et Z3. Ce vérificateur effectue une vérification de modèle bornée (BMC) sur les fragments C1 et C2. Il émet des verdicts tels que EQUIVALENT, IMPLIES_REF_TO_LM, IMPLIES_LM_TO_REF, NOT_EQUIVALENT, ou UNSUPPORTED (pour les cas de vivacité hors BMC). Le PEC est sain : tout verdict EQUIVALENT qu'il produit est garanti correct, bien qu'il puisse s'abstenir sur des propriétés de vivacité complexes.
Boucle d'entraînement RWOPD :
- L'étudiant échantillonne $K$ déroulements pour un prompt donné.
- Le PEC ouvert filtre ces déroulements, rejetant ceux qui sont syntaxiquement brisés ou sémantiquement incorrects (NOT_EQUIVALENT).
- Les déroulements restants se voient attribuer un poids de récompense basé sur le verdict PEC (par exemple 1,0 pour EQUIVALENT, 0,6/0,4 pour les implications unilatérales).
- Un modèle enseignant figé de 14B (CodeV-SVA-14B) fournit une cible dense de divergence Kullback-Leibler (KL) avant sur les déroulements conservés.
- L'étudiant est mis à jour en utilisant une moyenne pondérée par la récompense de ces pertes KL. Cela garantit que la supervision est dense au niveau des jetons mais ancrée dans un comportement équivalent aux propriétés.
Protocole d'évaluation : Bien que l'entraînement repose sur le PEC ouvert pour le filtrage et la mise en forme des récompenses, l'évaluation finale utilise le vérificateur prop_eq_checker de niveau industriel Cadence JasperGold pour assurer l'exhaustivité et la cohérence avec les benchmarks précédents.

Contributions clés

Algorithme RWOPD : Une méthode de distillation novatrice qui restreint et pondère par la récompense la supervision dense de l'enseignant en utilisant un vérificateur d'équivalence de propriétés. Cela combine le signal dense au niveau des jetons de la distillation avec l'ancrage sémantique de la vérification formelle.
PEC ouvert SymbiYosys+Z3 : Un vérificateur sain et sans licence pour le fragment de vérification de modèle borné de SVA. Il fournit un signal de vérification reproductible à l'échelle de la seconde pour le filtrage pendant l'entraînement, le distinguant des oracles propriétaires utilisés dans les travaux antérieurs.
État de l'art empirique : La méthode établit de nouveaux records sur les benchmarks NL2SVA-Human et NL2SVA-Machine.

Résultats
Les auteurs ont évalué un modèle étudiant de 7B avec LoRA (0,53 % de paramètres entraînables) par rapport à des modèles spécialisés de 14B et à des bases générales de 671B.

Performance : RWOPD a obtenu les scores pass@1, pass@5 et pass@10 les plus élevés sur les deux benchmarks. Sur NL2SVA-Machine, il a surpassé l'ancien SOTA spécialisé (CodeV-SVA-14B) de 2 à 4 points de pourcentage (pp) et les modèles de 671B (DeepSeek-R1, GPT-5) de 4 à 7 pp sur pass@1.
Décomposition temporelle : Les gains étaient concentrés sur les tranches temporellement non triviales. RWOPD a amélioré C2 (délai borné) de 7,5 pp et C3 (vivacité) de 11,5 pp par rapport à l'enseignant de 14B, tandis que la performance C1 est restée saturée.
Études d'ablation :
- Distillation vs RL : L'optimisation de récompense éparse (GRPO, IPO) utilisant le même signal PEC n'a pas réussi à dépasser la ligne de base SFT, confirmant que la KL dense de l'enseignant est le principal moteur de performance.
- Filtre vs Enseignant : Un SFT par échantillonnage de rejet (filtrage des déroulements sans l'enseignant) n'a apporté que des gains marginaux (~2,5 pp), isolant la supervision dense de l'enseignant comme la principale valeur ajoutée.
- Précision du filtre : RWOPD (utilisant à la fois EQUIVALENT et les implications unilatérales) a surpassé le filtrage strict uniquement EQUIVALENT, équilibrant la disponibilité du gradient avec la correction sémantique.

Signification et revendications
L'article affirme que pour le régime spécifique des modèles de 7B avec adaptation LoRA, le vérificateur est plus efficace non pas comme signal de récompense autonome pour le RL, mais comme un filtre mis en forme par la récompense pour la supervision dense de l'enseignant. Les auteurs soutiennent que le « écart temporel caché » dans la génération de NL vers SVA n'est pas dû à un manque de données ou à la taille du modèle, mais plutôt au désalignement des objectifs d'entraînement (imitation de jetons vs équivalence de propriétés). En ancrant le signal dense de distillation dans l'équivalence formelle de propriétés, RWOPD permet à des modèles plus petits et efficaces de surpasser à la fois des modèles spécialisés plus grands et des LLM massifs à usage général dans la génération d'assertions matérielles sémantiquement correctes.

Le travail est présenté comme une « déclaration de régime » : à l'échelle 7B+LoRA, la combinaison d'un vérificateur ouvert sain et d'un enseignant puissant via une distillation en ligne est une utilisation plus efficace des signaux de vérification que l'apprentissage par renforcement éparse. Les auteurs reconnaissent les limites, notamment le mécanisme indirect pour l'apprentissage C3 (reposant sur la graine du curriculum plutôt que sur une rétroaction directe du vérificateur) et la dépendance à JasperGold pour l'évaluation finale en raison de l'incomplétude du PEC ouvert sur les propriétés de vivacité.