💻 computer science

KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base

KBSpec est un cadre piloté par les LLM qui génère des spécifications formelles en exploitant une base de connaissances auto-évolutive de documentation externe et de retours de vérificateurs internes, atteignant ainsi des améliorations significatives des taux de réussite de la vérification sans nécessiter de réglage de paramètres ni de données d'entraînement étiquetées.

Auteurs originaux : Wenhan Wang, Zeyu Sun

Publié 2026-06-23

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Wenhan Wang, Zeyu Sun

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

La vue d'ensemble : Apprendre à un robot à rédiger des contrats juridiques pour le code

Imaginez que vous avez un robot très intelligent et créatif (un grand modèle de langage, ou LLM) qui est excellent pour écrire des histoires et du code. Cependant, vous voulez que ce robot rédige des spécifications formelles — qui sont comme des contrats juridiques stricts, mathématiques, prouvant qu'un logiciel ne plantera jamais et ne se comportera pas mal.

Le problème est que le robot n'a jamais lu beaucoup de ces « contrats juridiques ». Dans le monde réel, la plupart des programmeurs n'en écrivent pas ; ils se contentent d'écrire du code. Ainsi, quand vous demandez au robot d'en rédiger un, il fait souvent des erreurs : il utilise une mauvaise grammaire, oublie des règles de sécurité importantes, ou écrit quelque chose qui semble correct mais qui est mathématiquement impossible à prouver.

KBSpec est un nouveau système conçu pour corriger cela. Il donne au robot un « carnet de notes intelligent » qui l'aide à apprendre comment rédiger ces contrats correctement, sans avoir besoin de réentraîner le cerveau du robot.

Le système de connaissances à deux sources

Le papier soutient que pour corriger le robot, vous avez besoin de deux types d'informations, comme un étudiant étudiant pour un examen difficile :

Le manuel scolaire (Connaissance externe) : C'est le manuel officiel écrit par les experts qui ont créé le langage. Il indique au robot les règles de base et la grammaire.
- Analogie : Imaginez donner au robot un dictionnaire et un livre de grammaire. Il connaît les mots, mais il ne sait pas comment les utiliser dans des situations délicates.
Les notes du coach (Connaissance interne) : C'est la partie la plus unique de KBSpec. Elle provient de l'observation du robot qui essaie, échoue, se fait corriger, puis réessaie.
- Analogie : Imaginez que le robot essaie d'écrire un contrat, et qu'un arbitre strict (un Vérificateur Formel) siffle et dit : « Erreur ! Vous ne pouvez pas faire ça ! ». Le robot essaie alors de nouveau, corrige l'erreur et réussit. KBSpec sauvegarde cette « histoire de succès » dans le carnet de notes. La fois suivante, le robot peut consulter le carnet et dire : « Oh, je me souviens ! Quand j'ai essayé de faire X, l'arbitre s'est fâché, mais si je fais Y à la place, ça fonctionne. »

Comment fonctionne KBSpec (Le pipeline en 3 étapes)

Le papier décrit un processus en trois étapes pour construire ce système :

Étape 1 : La configuration initiale (Remplir le carnet)
Les chercheurs commencent par placer les manuels officiels et les exemples dans le « carnet de notes » (Base de Connaissances) du robot. Cela donne au robot un point de départ de base.

Étape 2 : La boucle d'apprentissage (Apprendre en faisant)
C'est là que la magie opère. Le système exécute une boucle de nombreuses fois :

Le robot essaie d'écrire une spécification pour un morceau de code.
Le Vérificateur (l'arbitre) vérifie la spécification.
Si elle réussit : Le système sauvegarde la « recette » de la réussite dans le carnet de notes.
Si elle échoue : Le système regarde le message d'erreur, demande de l'aide au carnet de notes et essaie de corriger l'erreur. Si la correction fonctionne, cette « recette de réparation » est également sauvegardée.
Le Filtre : Le carnet de notes n'est pas juste un tas de papiers. Le système vérifie constamment : « Est-ce que ce conseil nous a réellement aidés à réussir le test ? ». Si un conseil issu du manuel officiel mène à un échec, il est déclassé. Si une nouvelle astuce apprise lors d'une réparation fonctionne, elle est promue.

Étape 3 : L'examen final (Inférence)
Lorsqu'un nouveau morceau de code inconnu se présente au robot, celui-ci ne devine pas. Il cherche les « recettes » les plus pertinentes dans son carnet de notes en constante évolution pour l'aider à écrire la spécification. Il utilise les leçons tirées des échecs passés pour éviter de commettre les mêmes erreurs.

Pourquoi est-ce spécial ?

Le papier souligne quelques points clés qui rendent KBSpec différent des autres méthodes :

Pas de chirurgie cérébrale : Habituellement, pour améliorer une IA, il faut effectuer un « fine-tuning », ce qui revient à pratiquer une chirurgie cérébrale coûteuse sur le modèle. KBSpec ne touche pas du tout au cerveau du robot. Il met simplement à jour le carnet de notes. Cela rend le système peu coûteux et facile à utiliser avec n'importe quel robot.
Le carnet de notes « auto-évolutif » : Le carnet de notes n'est pas statique. Il devient plus intelligent chaque fois que le robot s'entraîne. Il apprend quels éléments du manuel officiel sont réellement utiles et lesquels sont trop complexes à gérer pour l'arbitre.
De meilleurs résultats : Lorsqu'ils ont testé cela sur du code Java (en utilisant un benchmark appelé FormalBench), KBSpec a aidé le robot à réussir les tests de vérification 10 % à 25 % de plus souvent que les meilleures méthodes précédentes. Il a également produit plus de spécifications qui n'étaient pas seulement « correctes », mais aussi « complètes » (couvrant tous les détails nécessaires).

Le revers de la médaille (Ce que le papier a découvert)

Les chercheurs ont remarqué quelque chose d'intéressant concernant la « complétude » des contrats. Parfois, pour que le robot réussisse le test, le système doit rendre le contrat légèrement moins strict (par exemple, « Ceci fonctionne pour la plupart des nombres » au lieu de « Ceci fonctionne pour chaque nombre »).

Analogie : C'est comme un avocat qui réalise : « Si je promets la lune au client, je serai poursuivi. Mais si je lui promets un très grand jardin très sûr, je peux prouver que c'est vrai. »
Le papier a trouvé que bien que la rigueur moyenne ait légèrement diminué, le système générait plus de contrats qui étaient réellement utiles et vérifiables. Il a échangé un petit peu de perfection contre beaucoup plus de succès.

Résumé

KBSpec est comme donner à un étudiant un manuel scolaire et un tuteur personnel qui tient un journal de chaque erreur d'examen et de la manière dont elle a été corrigée. En mettant constamment à jour ce journal grâce aux retours d'un correcteur strict, l'étudiant apprend à réussir ses examens beaucoup plus souvent, sans avoir besoin de changer sa façon de penser — il lui suffit de lui donner de meilleures notes pour étudier.

Résumé Technique : KBSpec

Énoncé du Problème

La génération automatisée de spécifications formelles est une étape critique pour la compréhension des programmes et la vérification formelle. Bien que les modèles de langage étendus (LLM) aient montré des promesses dans la génération de code, leur application à la spécification formelle (par exemple, le Java Modeling Language, JML) se heurte à un obstacle majeur : la rareté des corpus de spécifications formelles dans les données d'entraînement. Ce statut de « faible ressource » entraîne de fréquentes erreurs syntaxiques et des échecs sémantiques (par exemple, l'absence de vérifications de limites, des invariants incorrects).

Les tentatives existantes visant à augmenter les LLM avec des connaissances externes (par exemple, la documentation officielle) sont insuffisantes car les ressources de spécification formelle sont souvent incomplètes, manquent de couverture sur divers modèles de vérification, ou contiennent des fonctionnalités expérimentales non entièrement supportées par les vérificateurs. De plus, s'appuyer uniquement sur des connaissances externes statiques ne permet pas de capturer les contraintes nuancées, spécifiques au vérificateur, nécessaires pour une vérification réussie.

Méthodologie : KBSpec

Les auteurs proposent KBSpec (Knowledge Base-Augmented Specification Generation), un cadre qui augmente les LLM avec une base de connaissances à double source et auto-évolutive. Le système fonctionne sans modifier les paramètres du LLM ni nécessiter de données de vérité terrain étiquetées, en s'appuyant plutôt sur le retour d'expérience des vérificateurs formels.

Le pipeline KBSpec se compose de trois étapes principales :

1. Initialisation de la Base de Connaissances

Le système initialise une base de connaissances de spécification ( $M$ ) en utilisant des connaissances externes provenant de la documentation officielle (par exemple, tutoriels OpenJML, exemples et exercices) et de directives de réparation écrites par des humains. Chaque élément de connaissance est structuré sous la forme d'un triplet : contenu original ( $c_i$ ), un résumé ( $s_i$ ) et des mots-clés ( $k_i$ ), générés par un LLM pour faciliter la recherche.

2. Évolution de la Base de Connaissances (Phase d'Entraînement)

C'est l'innovation centrale. La base de connaissances est mise à jour dynamiquement via un pipeline de génération et de réparation exécuté sur un corpus d'entraînement de programmes Java.

Génération : Pour un programme donné, le LLM génère une spécification de base. Il extrait ensuite les éléments de connaissance pertinents et génère de nouvelles spécifications basées sur différentes combinações de connaissances extraites.
Vérification et Notation : Les spécifications générées sont vérifiées à l'aide d'un vérificateur formel (OpenJML). Un score d'utilité est attribué à chaque élément de connaissance extrait en fonction de son aide au LLM pour réussir la vérification lorsqu'il avait précédemment échoué, ou de sa responsabilité d'échec lorsqu'il avait précédemment réussi.
Réparation Itérative : Pour les spécifications qui échouent, le système effectue jusqu'à trois cycles de réparation. Le LLM utilise la spécification originale, le message d'erreur du vérificateur et la connaissance extraite pour générer une version corrigée. L'utilité des éléments extraits est mise à jour en fonction de la réduction des erreurs ou de la réussite de la vérification.
Mise à jour et Filtrage : Après chaque époque, la base de connaissances est mise à jour. Les éléments ayant de faibles scores d'utilité sont filtrés, et de nouvelles trajectoires réussies (génération ou réparation) sont ajoutées. La redondance est gérée via des contrôles de similitude.

3. Inférence Augmentée par la Connaissance

Lors de la phase d'évaluation, KBSpec utilise la base de connaissances évoluée pour assister la génération de spécifications. Contra\text{à} la phase d'entraînement, qui utilise un échantillonnage aléatoire de groupes de connaissances, l'étape d'inférence emploie un sélecteur basé sur le LLM. Le LLM choisit de manière autonome les éléments de connaissance les plus pertinents (jusqu'à 3) parmi l'ensemble extrait pour guider la génération et la réparation ultérieure des spécifications.

Contributions Clés

Cadre KBSpec : Une approche novatrice, sans paramètre, pour la génération de spécifications formelles qui intègre une base de connaissances auto-évolutive pilotée par le retour d'expérience du vérificateur.
Connaissance à Double Source : L'identification et la validation que la combinaison de la documentation externe (pour la compréhension initiale du langage) avec la connaissance interne (distillée à partir du feedback du vérificateur sur les trajectoires de génération/réparation) est essentielle pour surmonter les limites des LLM en spécification formelle.
Validation Empirique : Une évaluation complète sur le benchmark FormalBench (génération de spécification JML) démontrant que KBSpec surpasse significativement les meilleures approches de référence actuelles, incluant SpecGen et diverses stratégies de prompting (Few-shot, Least-to-Most, Self-repair).

Résultats

Les expériences ont été menées avec trois backends LLM : GPT-5.2, GPT-5-mini et DeepSeek-v3.2.

Amélioration du Taux de Réussite : KBSpec a amélioré les taux de réussite de vérification de 10 à 25 % par rapport aux approches basées sur les LLM les plus performantes (ex: SpecGen). Sur GPT-5.2, le taux de réussite est passé de 43,35 % (SpecGen) à 58,94 %.
Réduction des Échecs : Le cadre a considérablement réduit les taux d'échec (réduisant par exemple le taux d'échec pour GPT-5.2 à 20,6 %).
Complétude : Bien que les scores de complétude moyenne aient montré une certaine variance, KBSpec a produit le plus grand nombre de spécifications de haute complétude (complétude $\ge$ 0,5). L'analyse des programmes vérifiés mutuellement a montré que KBSpec maintenait ou améliorait la complétude par rapport à SpecGen, indiquant que les gains de taux de réussite n'ont pas été obtenus en générant des contrats trivialement faibles.
Étude d'Ablation : L'étude a confirmé que le mécanisme d'évolution de la base de connaissances (connaissance interne) était la composante la plus critique, contribuant davantage à la performance que la documentation externe initiale. La réparation itérative a également été identifiée comme un moteur majeur de succès.

Signification et Revendications

L'article affirme que KBSpec répond à la nature de « faible ressource » des langages de spécification formelle en créant une boucle d'auto-amélioration où le système apprend de ses propres succès et échecs via le feedback du vérificateur.

Indépendant du Modèle : L'approche est légère et peut être appliquée à n'importe quel LLM sans ajustement fin (fine-tuning).
Généralisabilité : Bien qu'évalué sur JML, les auteurs affirment que la conception est indépendante du langage et peut être adaptée à tout langage de spécification doté d'un vérificateur automatisé.
Ingénierie Pragmatique : L'analyse des connaissances apprises révèle que le système apprend efficacement des stratégies de réparation pragmatiques (par exemple, la gestion des dépassements de capacité arithmétique, la suppression de constructions non supportées) plutôt que de simplement affaiblir les spécifications pour réussir la vérification.

Les auteurs concluent que l'intégration des connaissances dérivées de la documentation avec une évolution de la mémoire ancrée dans le vérificateur améliore substantiellement la capacité des LLM à générer des spécifications formelles syntaxiquement correctes et sémantiquement vérifiables.