FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning

Dit paper introduceert FM-Agent, het eerste framework dat grote, door LLM's gegenereerde softwaresystemen automatisch verifieert door compositional reasoning te combineren met het genereren van functionele specificaties op basis van natuurlijke taal en het automatisch opsporen van 522 nieuwe, kritieke bugs.

De kern

Stel je voor dat je een gigantische stad bouwt, niet met de hand, maar met een super-snelle, maar soms wat dromerige robot. Deze robot (een AI) kan in een mum van tijd miljoenen straten, gebouwen en riolen ontwerpen. Maar omdat de robot soms hallucineert (dingen bedenkt die niet bestaan), kunnen er gevaarlijke gaten in de weg zitten of kunnen bruggen instorten.

Het probleem is: hoe controleer je of zo'n enorme stad veilig is?

Vroeger deden mensen dit door elke brug en elk gebouw één voor één te inspecteren met een strenge checklist. Maar bij een stad van 143.000 gebouwen (regels code) is dat ondoenlijk. Het duurt te lang en kost te veel geld.

FM-Agent is de oplossing die in dit onderzoek wordt voorgesteld. Het is als een slimme, geautomatiseerde inspecteur die de stad in één dag kan doorzoeken, zonder dat hij eerst een menselijke expert nodig heeft om te vertellen wat er precies moet gebeuren.

Hier is hoe het werkt, vertaald in alledaagse termen:

1. Het oude probleem: De "Schrijver" vs. De "Bouwer"

Stel je voor dat je een bouwplan (de specificatie) moet maken voor een robot die een huis bouwt.

• Het oude probleem: Je moet als mens eerst een heel gedetailleerd plan schrijven: "De muur moet 3 meter hoog zijn, het dak moet waterdicht zijn." Maar als de robot het huis al heeft gebouwd (en misschien met fouten), is het heel moeilijk om terug te denken wat het bedoelde plan was. Je kijkt dan naar het gebouw en probeert het plan te raden, maar als het gebouw scheef staat, denk je misschien dat het plan ook scheef was.
• De oplossing van FM-Agent: In plaats van naar het gebouw te kijken, kijkt FM-Agent naar wie er om het gebouw vraagt.
  • Analogie: Stel je voor dat je een kok bent. In plaats van te kijken of het eten op het bord er goed uitziet (wat soms mislukt), kijkt je naar de bestelling van de klant. Als de klant zegt: "Ik wil een hete soep", en de kok levert koude soep, dan is er een probleem, ook al zag de soep er misschien nog wel lekker uit.
  • FM-Agent kijkt naar de "bestellingen" (de code die de robot gebruikt om de functie aan te roepen) en zegt: "Oké, de klant verwacht hete soep. Laten we controleren of de kok dat levert." Zo ontdekt hij fouten die de robot zelf heeft gemaakt, zonder dat een mens het plan hoeft te schrijven.

2. De "Top-Down" Methode: Van de Hoofdstraat naar de Steegjes

Oude methoden probeerden vaak van onderop te werken: eerst de fundering controleren, dan de muren, dan het dak. Dat is traag.

• FM-Agent werkt anders: Het begint bij de hoofdstraat (de ingang van het systeem).
  • Het zegt: "Oké, de hoofdingang moet een auto kunnen ontvangen."
  • Vervolgens vraagt het de robot: "Welke wegen leiden naar de garage?"
  • Dan vraagt het: "Welke wegen leiden naar de slaapkamer?"
  • Zo werkt het zich stap voor stap naar beneden, van de grote ingang naar de kleine kamers. Omdat het systeem uit verschillende losse delen bestaat, kan FM-Agent veel kamers tegelijkertijd controleren (zoals een team van inspecteurs dat elke straat tegelijk afloopt). Dit maakt het enorm snel.

3. Het "Taal" Probleem: Mensen spreken mensentaal, computers spreken wiskunde

Tot nu toe moesten inspecteurs hun regels opschrijven in een heel moeilijke wiskundige taal (formele logica). Mensen denken echter in gewoon taal: "Dit mag niet kapot gaan" of "Dit moet snel zijn".

• De innovatie: FM-Agent is slim genoeg om gewone taal te begrijpen.
  • Analogie: Een oude inspecteur had een vertaler nodig om te begrijpen wat de klant zei. FM-Agent is de vertaler én de inspecteur in één. Hij leest de bestelling in gewoon Nederlands ("Laat de deur niet open als het regent") en controleert of de code dat doet. Hij hoeft geen wiskundige formules te schrijven; hij "denkt" gewoon mee in mensentaal.

4. De "Proef" (Bug Validator): Niet alleen praten, maar doen

Soms kan een AI zeggen: "Ik denk dat er een fout is," maar dat is nog geen bewijs. Het kan zijn dat de AI droomt (hallucineert).

• De oplossing: FM-Agent is niet alleen een denker, maar ook een proefknipper.
  • Als hij denkt dat er een gat in de weg zit, bouwt hij direct een kleine auto (een test) en rijdt die eroverheen.
  • Als de auto erin valt, is het bewijs: "Ja, hier is een gat!"
  • Als de auto veilig blijft, zegt hij: "Oké, het was een verkeerde alarm."
  • Dit zorgt ervoor dat de fouten die hij vindt, echt bestaan en niet alleen in zijn hoofd.

Wat hebben ze gevonden?

In hun test hebben ze FM-Agent losgelaten op vier enorme projecten die volledig door AI-robots waren gebouwd:

1. Een C-compiler (een vertaler voor programmeurs).
2. Een Deep Learning framework (voor kunstmatige intelligentie).
3. Een Besturingssysteem (zoals Windows of Linux).
4. Een Database (voor het opslaan van data).

Ook al hadden de bouwers deze systemen al getest, FM-Agent vond 522 nieuwe, ernstige fouten.

• Sommige fouten zorgden dat het systeem crashte (instortte).
• Andere fouten zorgden dat de resultaten verkeerd waren (bijvoorbeeld: een berekening die 100 opleverde in plaats van 99).
• Dit is alsof je een stad bouwt, de politie het al heeft gecontroleerd, en dan komt er een nieuwe inspecteur die 500 nieuwe, gevaarlijke gaten in de wegen vindt die niemand zag.

Conclusie

FM-Agent is als een super-snelle, slimme inspecteur die:

1. Kijkt naar wat de klant wil (in gewoon taal), niet naar wat de bouwer heeft gemaakt.
2. De hele stad in kleine stukjes verdeelt en die tegelijkertijd controleert.
3. Direct proefjes doet om te bewijzen dat er echt iets mis is.

Het is een game-changer voor de toekomst, waar AI steeds meer software bouwt. Het zorgt ervoor dat we niet hoeven te wachten tot de brug instort voordat we weten dat hij niet veilig is.

Technische samenvatting

Probleemstelling

Het gebruik van Large Language Models (LLMs) voor softwareontwikkeling neemt toe en kan complexe systemen genereren (bijv. compilers met meer dan 100.000 regels code). Een kritiek punt is echter de correctheid van deze gegenereerde code, die vaak fouten bevat door "hallucinaties" van de LLM.

Traditionele methoden voor geautomatiseerd redeneren (zoals symbolische uitvoering of semi-automatische verifiers) schalen slecht naar grote systemen vanwege:

1. Complexiteit: Systemen hebben complexe controleflows, staatmanipulatie en diepe inter-procedurele afhankelijkheden.
2. Specificatie-vereisten: Methoden gebaseerd op Hoare-logica vereisen formele specificaties (voor- en post-condities) voor elke functie. Het handmatig schrijven van deze specificaties is een zware menselijke last.
3. Het LLM-dilemma: Wanneer code door LLMs wordt gegenereerd, hebben ontwikkelaars vaak geen diepgaand inzicht in de verwachte gedragingen van elke functie, waardoor het schrijven van accurate specificaties nog moeilijker wordt. Bestaande methoden die specificaties afleiden uit de implementatie, falen omdat de implementatie zelf defecten kan bevatten.

Methodologie: FM-Agent

FM-Agent is het eerste framework dat geautomatiseerde compositieel redenering mogelijk maakt voor grote systemen door LLMs te combineren met Hoare-logica. Het framework bestaat uit drie hoofdcomponenten en lost drie uitdagingen op via drie kerninzichten:

1. Specificatie Generator (Top-Down Paradigma)

• Uitdaging: Bestaande methoden genereren specificaties vanuit de implementatie (bottom-up), wat fouten kan versterken.
• Oplossing: FM-Agent gebruikt een top-down benadering. In plaats van naar de implementatie te kijken, analyseert de LLM hoe de aanroepende functies (callers) de functie verwachten te gebruiken.
• Concept: De "verwachte specificatie" wordt afgeleid uit de context van de caller (argumenten voor pre-condities, gebruik van de return-waarde voor post-condities). Als een functie door meerdere callers wordt aangeroepen, worden deze verwachtingen samengevoegd (disjunctie voor pre-condities, conjunctie voor post-condities).
• Schaalbaarheid: Het systeem bepaalt een generatievolgorde gebaseerd op een gecomprimeerde call-graph (SCCs en topologische sortering), waardoor specificaties voor onafhankelijke functies of lagen parallel kunnen worden gegenereerd.

2. Code Reasoner (Hoare-Style Redenering in Natuurlijke Taal)

• Uitdaging: Bestaande verifiers werken alleen met formele logica, terwijl ontwikkelaars intenties in natuurlijke taal uitdrukken.
• Oplossing: FM-Agent generaliseert Hoare-logica inferentieregels om direct te redeneren over natuurlijke taal specificaties.
• Methode: De LLM inferreert iteratief de post-condities van codeblokken (statements) op basis van de pre-conditie. Als de post-conditie van een uitvoeringspad niet impliceert wat de specificatie vereist, wordt een potentiële bug gemeld.
• Inzicht: LLMs kunnen de uitvoeringsresultaten van kleine codeblokken zeer nauwkeurig voorspellen (98,6% nauwkeurigheid in tests), wat deze stapsgewijze redenering mogelijk maakt zonder dure SMT-oplossers voor elke stap.

3. Bug Validator (Testgeneratie)

• Uitdaging: Als verificatie faalt, is het moeilijk om de oorzaak van de bug te bepalen of te bevestigen of het een echte bug is (om hallucinaties van de LLM te filteren).
• Oplossing: FM-Agent genereert automatisch testgevallen op systeemniveau (in plaats van op functieniveau) die de potentiële bug triggeren.
• Methode: De LLM gebruikt de redeneerprocessen om een input te construeren die de specifieke fout veroorzaakt. Het systeem voert deze test uit en vergelijkt het resultaat met een referentie-implementatie of de verwachte uitkomst. Alleen bevestigde bugs worden gerapporteerd.

Kernbijdragen

1. Eerste Framework voor Geautomatiseerde Compositieel Redenering: FM-Agent is het eerste systeem dat volledige compositieel verificatie (onafhankelijke verificatie van functies die samen een systeem garanderen) automatiseert voor grote systemen.
2. Top-Down Specificatiegeneratie: Een nieuw paradigma dat specificaties afleidt uit de intentie van de caller, waardoor het robuust is tegen defecte implementaties.
3. Redeneren in Natuurlijke Taal: Generalisatie van Hoare-logica om direct te werken met natuurlijke taal specificaties, wat de kloof tussen menselijke intentie en formele verificatie overbrugt.
4. Systeemniveau Bug Validatie: Een mechanisme om potentiële bugs te bevestigen door automatisch testgevallen te genereren die de root-cause blootleggen.

Resultaten

FM-Agent werd geëvalueerd op vier grote, door LLM-agenten gegenereerde systemen (tot 143.000 regels code), waaronder een C-compiler (CCC), een ML-framework (VibeTensor), een besturingssysteem (VibeOS) en een database (Bespoke OLAP).

• Schalingsvermogen: Het systeem slaagde erin om binnen 2 dagen volledige compositieel redenering uit te voeren op systemen tot 143k LoC.
• Bug Detectie: Ondanks dat deze systemen al uitgebreid waren getest door hun ontwikkelaars (unit tests, integratietests, multi-agent reviews), vond FM-Agent 522 nieuwe, eerder onontdekte bugs.
  • CCC: 339 bugs (o.a. incorrecte IR-generatie, crashes).
  • VibeTensor: 141 bugs (o.a. geheugenlekken, incorrecte tensorwaarden).
  • VibeOS: 23 bugs (o.a. stack overflow, oneindige loops).
  • Bespoke OLAP: 19 bugs (o.a. verkeerde query-resultaten).
• Ablatie-studie: Een versie zonder het top-down paradigma en zonder Hoare-style redenering vond slechts 57 bugs in dezelfde compiler, wat aantoont dat de kernmethodes essentieel zijn voor succes.

Betekenis

Dit paper markeert een belangrijke stap in de betrouwbaarheid van software die door AI wordt gegenereerd.

• Complementair aan Formele Verificatie: FM-Agent vervangt geen traditionele formele verifiers (die geluidheid garanderen), maar biedt een schaalbaar alternatief voor systemen waar handmatige specificaties onhaalbaar zijn.
• Paradigmaverschuiving: Het verschuift de focus van het handmatig schrijven van formele contracten naar het automatisch afleiden van intenties uit de context van het systeem.
• Praktische Impact: Het biedt een haalbare route om de kwaliteit van complexe, AI-genererde systemen te waarborgen, wat essentieel is voor de adoptie van AI-assisted software engineering in kritieke domeinen.