💻 computer science

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

KBSpec is een door LLM gedreven framework dat formele specificaties genereert door gebruik te maken van een zelf evoluerende kennisbank van externe documentatie en interne verifieerder-feedback, waarmee significante verbeteringen in verificatie-succespercentages worden bereikt zonder dat parametertuning of gelabelde trainingsdata vereist zijn.

Oorspronkelijke auteurs: Wenhan Wang, Zeyu Sun

Gepubliceerd 2026-06-23

📖 6 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Wenhan Wang, Zeyu Sun

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Het Grote Plaatje: Een Robot Leren Juridische Contracten voor Code te Schrijven

Stel je voor dat je een zeer slimme, creatieve robot hebt (een Large Language Model, of LLM) die erg goed is in het schrijven van verhalen en code. Je wilt echter dat deze robot formele specificaties schrijft—die zijn als strikte, wiskundige juridische contracten die bewijzen dat een stuk software nooit zal crashen of slecht zal gedrag vertonen.

Het probleem is dat de robot niet veel van deze "juridische contracten" heeft gelezen. In de echte wereld schrijven de meeste programmeurs ze niet; ze schrijven gewoon code. Dus wanneer je de robot vraagt om er een te schrijven, maakt hij vaak fouten: hij gebruikt de verkeerde grammatica, vergeet belangrijke veiligheidsregels, of schrijft iets dat goed klinkt maar wiskundig gezien onmogelijk te bewijzen is.

KBSpec is een nieuw systeem dat is ontworpen om dit op te lossen. Het geeft de robot een "slim notitieblok" dat hem helpt om deze contracten correct te schrijven, zonder dat de hersenen van de robot opnieuw getraind hoeven te worden.

Het Systeem met Twee Bronnen van Kennis

Het paper stelt dat je twee soorten informatie nodig hebt om de robot te verbeteren, zoals een student die studeert voor een moeilijk examen:

Het Handboek (Externe Kennis): Dit is de officiële handleiding geschreven door de experts die de taal hebben gemaakt. Het vertelt de robot de basisregels en de grammatica.
- Analogie: Stel je voor dat je de robot een woordenboek en een grammaticaboek geeft. Hij kent de woorden, maar hij weet niet hoe hij ze in lastige situaties moet gebruiken.
De Notities van de Coach (Interne Kennis): Dit is het meest unieke deel van KBSpec. Dit komt voort uit het observeren van de robot terwijl hij probeert, faalt, gecorrigeerd wordt en het opnieuw probeert.
- Analogie: Stel je voor dat de robot een contract probeert te schrijven, en een strenge scheidsrechter (een Formal Verifier) blaast op zijn fluitje en zegt: "Fout! Dat mag je niet doen!" De robot probeert het daarna opnieuw, herstelt de fout, en slaagt. KBSpec slaat dit "succesverhaal" op in het notitieblok. De volgende keer kan de robot in het notitieblok kijken en zeggen: "Oh, ik herinner het me! Toen ik X probeerde te doen, werd de scheidsrechter boos, maar als ik in plaats daarvan Y doe, werkt het wel."

Hoe KBSpec Werkt (De 3-Stappen Pipeline)

Het paper beschrijft een driestappenproces om dit systeem te bouwen:

Stap 1: De Initiële Opzet (Het Notitieblok Vullen)
Onderzoekers beginnen met het plaatsen van de officiële handleidingen en voorbeelden in het "notitieblok" (de Knowledge Base) van de robot. Dit geeft de robot een basis startpunt.

Stap 2: De Trainingslus (Leren door te Doen)
Dit is waar de magie gebeurt. Het systeem draait een lus vele malen:

De robot probeert een specificatie voor een stuk code te schrijven.
De Verifier (de scheidsrechter) controleert deze.
Als het slaagt: Het systeem slaat het "recept" van hoe het is geslaagd op in het notitieblok.
Als het faalt: Het systeem kijkt naar de foutmelding, vraagt hulp aan het notitieblok, en probeert de fout te herstellen. Als de reparatie werkt, wordt dat "reparatierecept" ook opgeslagen.
Het Filter: Het notitieblok is niet zomaar een stapel papier. Het systeem controleert constant: "Heeft dit advies ons daadwerkelijk geholpen om de test te halen?" Als een stuk advies uit de officiële handleiding tot een fout leidt, wordt het lager ingedeeld. Als een nieuwe truc die geleerd is tijdens een reparatie werkt, wordt deze gepromoveerd.

Stap 3: Het Eindexamen (Inference)
Wanneer de robot geconfronteerd wordt met een nieuwe, onbekende stuk code, gokt hij niet zomaar wat. Hij zoekt naar de meest relevante "recepten" in zijn evoluerende notitieblok om hem te helpen de specificatie te schrijven. Hij gebruikt de lessen geleerd van eerdere fouten om dezelfde fouten niet opnieuw te maken.

Waarom Dit Speciaal Is

Het paper benadrukt een paar belangrijke punten die KBSpec anders maken dan andere methoden:

Geen Hersenchirurgie: Normaal gesproken moet je een AI verbeteren door middel van "fine-tuning", wat lijkt op een dure hersenoperatie aan het model. KBSpec raakt de hersenen van de robot helemaal niet aan. Het werkt alleen het notitieblok bij. Dit maakt het goedkoop en gemakkelijk te gebruiken met elke robot.
Het "Zelf-Evoluerende" Notitieblok: Het notitieblok is niet statisch. Het wordt slimmer telkens wanneer de robot oefent. Het leert welke regels uit de officiële handleiding daadwerkelijk nuttig zijn en welke te complex zijn voor de scheidsrechter om te verwerken.
Betere Resultaten: Toen ze dit testten op Java-code (met een benchmark genaamd FormalBench), hielp KBSpec de robot om de verificatietests 10% tot 25% vaker te halen dan de beste eerdere methoden. Het produceerde ook meer specificaties die niet alleen "correct" waren, maar ook "compleet" (ze dekken alle noodzakelijke details).

De Addertjes onder het Gras (Wat het Paper Vond)

De onderzoekers merkten iets interessants op over de "volledigheid" van de contracten. Soms, om de robot te laten slagen voor de test, moest het systeem het contract iets minder strikt maken (bijv. "Dit werkt voor de meeste getallen" in plaats van "Dit werkt voor elk getal").

Analogie: Het is alsoals een advocaat die beseft: "Als ik de klant de maan beloof, word ik aangeklaagd. Maar als ik hen een zeer grote, zeer veilige tuin beloof, kan ik bewijzen dat het waar is."
Het paper vond dat hoewel de gemiddelde striktheid iets daalde, het systeem meer contracten genereerde die daadwerkelijk nuttig en verifieerbaar waren. Het ruilde een klein beetje perfectie in voor veel meer succes.

Samenvatting

KBSpec is als het geven van een tekstboek én een persoonlijke tutor aan een student, waarbij de tutor een dagboek bijhoudt van elke fout tijdens een examen en hoe die fout werd hersteld. Door het dagboek constant bij te werken op basis van feedback van een strenge beoordelaar, leert de student om veel vaker het examen te halen, zonder dat de manier waarop de student denkt hoeft te veranderen—alleen door ze betere aantekeningen te geven om uit te leren.

Technische Samenvatting: KBSpec

Probleemstelling

Geautomatiseerde generatie van formele specificaties is een cruciale stap voor begrip van programma's en formele verificatie. Hoewel Large Language Models (LLM's) veelbelovend zijn gebleken bij codegeneratie, vormt hun toepassing op formele specificaties (bijv. Java Modeling Language, JML) een aanzienlijke hindernis: de schaarste aan corpora van formele specificaties in trainingsdata. Deze "low-resource" status leidt tot frequente syntactische fouten en semantische defecten (bijv. ontbrekende grenswaardecontroles, incorrecte invarianten).

Bestaande pogingen om LLM's aan te vullen met externe kennis (bijv. officiële documentatie) zijn onvoldoende omdat bronnen voor formele specificaties vaak incompleet zijn, een gebrek aan dekking hebben wat betreft diverse verificatiepatronen, of experimentele functies bevatten die niet volledig worden ondersteund door verifiers. Bovendien slaagt het louter vertrouwen op statische externe kennis er niet in om de genuanceerde, verifier-specifieke beperkingen te vatten die vereist zijn voor succesvolle verificatie.

Methodologie: KBSpec

De auteurs stellen KBSpec voor (Knowledge Base-Augmented Specification Generation), een framework dat LLM's aanvult met een duale, zelf-evoluerende kennisbank. Het systeem werkt zonder de parameters van de LLM aan te passen of gelabelde grondwaarheid (ground-truth) data te vereisen, en vertrouwt in plaats daarvan op feedback van formele verifiers.

De KBSpec-pipeline bestaat uit drie hoofdfasen:

1. Initialisatie van de Kennisbank

Het systeem initialiseert een kennisbank voor specificaties ( $M$ ) met behulp van externe kennis afkomstig uit officiële documentatie (bijv. OpenJML tutorials, voorbeelden en oefeningen) en door mensen geschreven reparatierichtlijnen. Elk kennisitem is gestructureerd als een triplet: de originele inhoud ( $c_i$ ), een samenvatting ( $s_i$ ) en trefwoorden ( $k_i$ ), gegenereerd door een LLM om retrieval te faciliteren.

2. Evolutie van de Kennisbank (Trainingsfase)

Dit is de kerninnovatie. De kennisbank wordt dynamisch bijgewerkt via een generatie-en-reparatie-pipeline die wordt uitgevoerd over een "trainingscorpus" van Java-programma's.

Generatie: Voor een gegeven programma genereert de LLM een basislijn-specificatie. Vervolgens haalt het relevante kennisitems op en genereert het nieuwe specificaties op basis van verschillende combinaties van de opgehaalde kennis.
Verificatie & Scoring: Gegenereerde specificaties worden geverifieerd met een formele verifier (OpenJML). Aan elk opgehaald kennisitem wordt een helpfulness score toegekend op basis van de vraag of het de LLM hielp om de verificatie te passeren wanneer deze eerder faalde, of dat het leidde tot falen wanneer deze eerder slaagde.
Iteratieve Reparatie: Voor specificaties die falen, voert het systeem maximaal drie rondes van reparatie uit. De LLM gebruikt de originele specificatie, de foutmelding van de verifier en de opgehaalde kennis om een gecorrigeerde versie te genereren. De effectiviteit (helpfulness) van de opgehaalde items wordt bijgewerkt op basis van de vermindering van fouten of succesvolle verificatie.
Update & Filtering: Na elke epoch wordt de kennisbank bijgewerkt. Items met lage helpfulness scores worden gefilterd en nieuwe succesvolle trajecten (generatie of reparatie) worden toegevoegd. Redundantie wordt beheerd via gelijkeniscontroles.

3. Kennis-geaugmenteerde Inferentie

Tijdens de evaluatiefase gebruikt KBSpec de geëvolueerde kennisbank om de generatie van specificaties te ondersteunen. In tegenstelling tot de trainingsfase, die gebruikmaakt van willekeurige bemonstering van kennisgroepen, maakt de inferentiefase gebruik van een LLM-gebaseerde selector. De LLM kiest autonoom de meest relevante kennisitems (tot maximaal 3) uit de opgehaalde set om de generatie en de daaropvolgende reparatie van specificaties te sturen.

Belangrijkste Bijdragen

KBSpec Framework: Een nieuw, parameter-vrij benadering voor formele specificatiegeneratie die een zelf-evoluerende kennisbank integreert die wordt gedreven door verifier-feedback.
Dual-Source Knowledge: De identificatie en validatie dat het combineren van externe documentatie (voor initiële taalbegrip) met interne kennis (gedestilleerd uit verifier-feedback op generatie/reparatie-trajecten) essentieel is om de beperkingen van LLM's in formele specificaties te overwinnen.
Empirische Validatie: Een uitgebreide evaluatie op de FormalBench benchmark (JML specificatiegeneratie) die aantoont dat KBSpec de state-of-the-art baselines, inclus $ief$ SpecGen en diverse prompting-strategieën (Few-shot, Least-to-Most, Self-repair), significant overtreft.

Resultaten

Experimenten werden uitgevoerd met drie LLM-backends: GPT-5.2, GPT-5-mini en DeepSeek-v3.2.

Verbetering Pass Rate: KBSpec verbeterde de verificatie-pass rates met 10–25% ten opzichte van state-of-the-art LLM-gebaseerde benaderingen (bijv. SpecGen). Op GPT-5.2 steeg de pass rate van 43,35% (SpecGen) naar 58,94%.
Reductie van Falen: Het framework reduceerde de failure rates substantieel (bijv. door de fail rate voor GPT-5.2 te verlagen naar 20,6%).
Volledigheid: Hoewel gemiddelde volledigheidsscores enige variatie vertoonden, produceerde KBSpec het grootste aantal specificaties met een hoge volledigheid (volledigheid $\ge$ 0,5). Analyse van wederzijds geverifieerde programma's toonde aan dat KBSpec de volledigheid behield of verbeterde vergeleken met SpecGen, wat aangeeft dat de winst in pass rate niet werd behaald door triviaal zwakke contracten te genereren.
Ablatieonderzoek: De studie bevestigde dat het mechanisme voor de evolutie van de kennisbank (interne kennis) de meest kritieke component was, die meer bijdroeg aan de prestaties dan de initiële externe documentatie. Iteratieve reparatie werd ook geïdentificeerd als een belangrijke drijfveer voor succes.

Betekenis en Claims

De paper claimt dat KBSpec de "low-resource" aard van formele specificationstalen aanpakt door een zelf-verbeterende lus te creëren waarbij het systeem leert van zijn eigen successen en fouten via verifier-feedback.

Model Agnostic: De benadering is lichtgewicht en kan op elke LLM worden toegepast zonder fine-tuning.
Generaliseerbaarheid: Hoewel geëvalueerd op JML, claimen de auteurs dat het ontwerp taal-agnostisch is en kan worden aangepast aan elke specificatietaal met een geautomatiseerde verifier.
Pragmatische Engineering: De analyse van de geleerde kennis laat zien dat het systeem effectief pragmatische reparatiestrategieën leert (bijv. het afhandelen van rekenkundige overflows, het verwijderen van niet-ondersteunde constructen) in plaats van simpelweg de specificaties te verzwakken om verificatie te passeren.

De auteurs concluderen dat het integreren van documentatie-afgeleide kennis met verifier-gegronde geheugen-evolutie de capaciteit van LLM's om syntactisch correcte en semantisch verifieerbare formele specificaties te genereren aanzienlijk versterkt.