🤖 AI

P $^{3}$ : Joint Program-and-Proof Planning for Verified Code Generation

Het artikel introduceert $P^3$ , een op LLM gebaseerde agentische workflow die programma's en hun formele bewijzen gezamenlijk plant om de inefficiënties van sequentiële generatie te overwinnen, waarbij het staat-van-de-kunst prestaties en aanzienlijke kostenreducties bereikt op benchmarks voor geverifieerde codegeneratie, inclusief een nieuwe, uit een repository afgeleide dataset genaamd Lean4Commit0.

Oorspronkelijke auteurs: Zenan Li, Ziran Yang, Peiyang Song, Zhaoyu Li, Kaiyu Yang

Gepubliceerd 2026-08-11

📖 7 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Zenan Li, Ziran Yang, Peiyang Song, Zhaoyu Li, Kaiyu Yang

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

Stel je voor dat je een superintelligente robot leert om een verhaal te schrijven. Je geeft de robot een prompt, en de robot spuugt een verhaal uit. Maar hier is de crux: je wilt niet zomaar een verhaal; je wilt een verhaal dat wiskundig gegarandeerd waar is, zonder plotgaten, zonder magie die de wetten van de natuurkunde breekt, en zonder personages die zonder uitleg verdwijnen. Dit is de wereld van geverifieerde codegeneratie. Het is een hoek van de informatica waar we AI niet alleen vragen om software te schrijven, maar om software te schrijven die gepaard gaat met zijn eigen "bewijs van correctheid"—een wiskundig certificaat dat zegt: "Ik beloof dat deze code precies zal doen wat ik heb gezegd, voor elke mogelijke situatie."

Lange tijd was de standaardmanier om dit te doen als een tweetalige dans: eerst schrijft de robot de code (het verhaal), en dan probeert een apart team van robot-proeflezers te controleren of het verhaal wel logisch is. Als de proeflezers een plotgat vinden, sturen ze het verhaal terug naar de schrijver om het te repareren. De schrijver past het verhaal aan, stuurt het terug, en de cyclus herhaalt zich. De auteurs van dit artikel stellen dat deze "schrijf-dan-controleer"-dans vaak lomp en inefficiënt is. Het is alsof je een brug bouwt en er pas na voltooiing achter komt dat je de steunbalken bent vergeten, waardoor je de hele brug moet afbreken en opnieuw moet opbouwen. De auteurs van dit artikel stellen een nieuwe manier voor: in plaats van de code en het bewijs apart te schrijven, moet de robot de volledige brug plannen—zowel de weg als de steunbalken—tegelijkertijd, zodat ze vanaf de eerste schets al perfect bij elkaar passen.

Het Probleem: De "Schrijf-dan-Controleer"-valstrik

Het artikel, getiteld "Joint Program-and-Proof Planning for Verified Code Generation," pakt een frustrerende bottleneck aan in de manier waarop AI geverifieerde software schrijft. Momenteel volgen de meeste systemen een "programma-dan-bewijs"-workflow. Het is alsof je een chef-kok vraagt om een complex gerecht te koken en hem dan, nadat het eten op tafel staat, een voedselcriticus vraagt om te bewijzen dat de ingrediënten vers waren en de bereidingswijze veilig was. Als de criticus een probleem vindt (zoals halfgare kip), moet de chef teruggaan, het gerecht opnieuw bereiden en hopen dat de criticus het deze keer wel goedkeurt.

De auteurs betogen dat deze sequentiële aanpak gebrekkig is. Wanneer de AI zich eerst vastlegt op het schrijven van de code, kan de AI een structuur kiezen die aan de oppervlakte prima lijkt, maar een nachtmerrie is om te bewijzen. Stel je voor dat de AI een programma schrijft om het grootste getal in een lijst te vinden. De AI kan een methode kiezen die kort en bondig is om te schrijven, maar die een ongelooflijk complexe, verborgen wiskundige regel vereist om te bewijzen dat het werkt. Zodra de code is geschreven, zit de AI vast: de AI moet ofwel een supermoeilijk bewijs verzinnen dat past bij die specifieke code, of de code verscheuren en opnieuw beginnen. Dit leidt tot veel verspilde tijd, geld en "reparatielussen" waarbij de AI de code en het bewijs blijft patchen, maar ze nooit echt op elkaar aansluiten.

De Oplossing: P3 (De "Hand-in-Hand" Planner)

Om dit op te lossen, introduceren de onderzoekers P3, een nieuwe workflow waarbij de AI optreedt als een meesterarchitect die de blauwdruk voor zowel het gebouw als de veiligheidsinspectie tekent voordat er ook maar één baksteen wordt gelegd.

In plaats van direct in de code te duiken, maakt P3 eerst een verenigd plan. Dit plan is een hoogwaardige schets die twee vragen tegelijk beantwoordt:

Hoe zal de code werken? (De "Programma-schets")
Hoe zullen we bewijzen dat het werkt? (De "Bewijs-schets")

Het plan bepaalt de structuur van de oplossing. Het kiest de juiste "vorm" voor de code (zoals te kiezen tussen een recursieve lus of een fold) en kiest tegelijkertijd de bijbehorende wiskundige regels (invarianten) die nodig zijn om te bewijzen dat die vorm veilig is. Het is als beslissen: "We gaan een brug bouwen met ophangkabels, dus ons bewijsplan moet ook het controleren van de spanning in die kabels bevatten."

Zodra dit gedeelde plan is vastgelegd, "elaboreert" de AI de details. De AI schrijft de werkelijke code en het werkelijke bewijs, maar het is slechts het invullen van de blanco ruimtes in een vooraf overeengekomen blauwdruk. Als het bewijs faalt, weet de AI precies waar hij moet kijken, omdat de structuur al was beslist. Als het plan zelf slecht is (bijv. het brugontwerp is onmogelijk), gaat de AI terug naar de planningsfase om de blauwdruk opnieuw te tekenen, in plaats van wanhopig de afgebouwde brug te blijven patchen.

Het Nieuwe Testveld: Lean4Commit0

De auteurs realiseerden zich dat eerdere tests voor deze AI-systemen te makkelijk waren, zoals het vragen aan een robot om wiskundige puzzels uit een tekstboek op te lossen. Software in de echte wereld is rommeliger. Om hun nieuwe methode goed te testen, hebben ze een nieuwe benchmark gebouwd genaamd Lean4Commit0.

Ze hebben 108 real-world open-source softwarebibliotheken (geschreven in Python, Rust, C/C++ en Java) gescraped en de kernfuncties daarvan omgezet in uitdagingen voor "geverifieerde code". In plaats van eenvoudige taken zoals "tel twee getallen bij elkaar op", bevatten deze uitdagingen complexe relaties tussen verschillende onderdelen van een programma. Bijvoorbeeld, in een configuratiesysteem zouden ze de AI kunnen vragen te bewijzen dat "als je een instelling op 'Hoog' zet en later op 'Laag', het systeem de instelling 'Laag' correct onthoudt." Deze taken vereisen dat de AI begrijpt hoe verschillende functies met elkaar communiceren, wat ze veel moeilijker maakt dan tekstboekproblemen.

Wat Ze Vonden: Slimmer Plannen Wint

Het team heeft P3 getest tegen vier van de krachtigste beschikbare AI-modellen (waaronder versies van Codex, Gemini en Claude) over drie verschillende benchmarks: Verina, AlgoVeri en hun nieuwe Lean4Commit0.

De resultaten waren duidelijk: Samen plannen werkt beter dan apart schrijven.

Succespercentage: P3 loste meer taken op dan welke andere methode dan ook in elke enkele test. Op de moeilijkste taken verbeterde het succespercentage met 4,6 tot 11,2 procentpunten vergeleken met de beste bestaande methoden.
Efficiëntie: Het ging niet alleen om het oplossen van meer problemen; het was ook sneller en goedkoper. Bij moeilijke taken verminderde P3 de kosten van API-aanroepen met wel 40% en verkortte de tijd die nodig was met wel 37%. Dit komt omdat de AI geen tijd verspilde aan het proberen te bewijzen van onmogelijke zaken of het herschrijven van code die structureel fout was.
Het "Gezamenlijke" Voordeel: Om te bewijzen dat het "gezamenlijk plannen" het geheime ingrediënt was, voerden ze een test uit waarbij de AI de code plande maar het bewijs niet vooraf plande. Deze "alleen-code-planning"-methode presteerde slechter dan P3, wat bevestigde dat het denken over het bewijs terwijl men de code plant, het verschil maakt.

Een Praktijkvoorbeeld: De Red-Black Tree

Om te laten zien hoe dit in de praktijk werkt, keken de auteurs naar een klassiek informaticaprobleem: het verwijderen van een knoop uit een "red-black tree" (een complexe datastructuur die wordt gebruikt om gegevens efficiënt te organiseren).

De Oude Manier (Programma-dan-Bewijs): De AI legde zich vast op een specifieke manier om de knoop te verwijderen. Het bleek dat deze manier structureel zo rommelig was dat het bewijs meer dan 6.300 regels code vereiste om de gaten te dichten, of het faalde volledig.
De P3-Manier: De AI plande eerst de verwijdering. De AI realiseerde zich dat een andere structurele aanpak makkelijker te bewijzen zou zijn. De AI hield zich aan dat plan en loste het probleem op in slechts 1.105 regels.

Waarom Dit Belangrijk Is

Dit artikel suggereert dat als we willen dat AI echt betrouwbare software schrijft, we moeten stoppen met het behandelen van de "code" en het "bewijs" als twee aparte taken. Door de AI te dwingen om na te denken over de wiskundige veiligheid van de code terwijl hij de code zelf ontwerpt, krijgen we software die niet alleen correct is door constructie, maar ook goedkoper en sneller te produceren is. Het is een verschuiving van "repareer het later" naar "bouw het in één keer goed", wat ervoor zorgt dat de software waarop we vertrouwen net zo solide is als de wiskunde die bewijst dat het werkt.

Technische Samenvatting: P3 – Gezamenlijke Programma-en-Bewijsplanning voor Geverifieerde Codegeneratie

1. Probleemstelling

Het artikel behandelt geverifieerde codegeneratie, een taak waarbij een Large Language Model (LLM) zowel een uitvoerbaar programma ( $\pi$ ) als een machine-controleerbaar bewijs ( $\kappa$ ) moet synthetiseren dat aantoont dat het programma voldoet aan een formele specificatie ( $\sigma = (P, Q)$ ). In tegen tegenstelling tot testgebaseerde generatie moet de correctheid gelden voor alle toegestane inputs, niet slechts voor een eindige set voorbeelden.

De auteurs identificeren een kritieke bottleneck in de huidige de facto workflow, die een sequentieel "programma-dan-bewijs" schema volgt:

De LLM committeert zich aan een concrete implementatie.
Een aparte bewijsfase probeert bewijsverplichtingen te vervullen.
Indien verificatie faalt, gaat het systeem in een broze "patch-and-retry" lus, waarbij afwisselend wordt geprobeerd de code en het bewijs te herstellen.

Deze sequentiële aanpak lijdt onder twee hoofdzaken:

Effectiviteit: Een programma dat gegenereerd is zonder rekening te houden met het bewijs, kan de noodzakelijke structurele eigenschappen missen (bijv. specifieke inductieve invarianten of decompositiestrategieën). Lokale reparaties falen vaak om een bewijs-vriendelijke structuur te herstellen die nooit gepland was.
Efficiëntie: Aanzienlijke computationele middelen (tokens en tijd) worden verspild aan het verkennen van reparaties voor implementaties die structureel incompatibel zijn met de bewijsvereisten van de specificatie.

Het artikel put inspiratie uit het principe van Dijkstra dat programma's en hun correctheidsargumenten "hand in hand" ontwikkeld moeten worden, en betoogt dat de implementatie en de bewijsstructuur elkaar wederzijds beperken.

2. Methodologie: Het P3-framework

De auteurs stellen P3 voor, een agentic workflow die planning ontkoppelt van elaboratie om structurele consistentie tussen het programma en het bewijs te waarborgen voordat een van beide volledig gerealiseerd is.

2.1 Gezamenlijke Programma-en-Bewijsplanning

In de eerste fase genereert de LLM-agent een geünificeerd plan ( $\rho$ ) op basis van de specificatie $\sigma$ . Dit plan is niet louter code; het is een hoogwaardige schets die vier specifieke commitments bevat:

Formeel Contract: Algoritmische instructies en asymptotische beperkingen.
Programmadecompositie: De recursievariabele, vertakkingsstructuur, datarepresentatie en terminatiemaatstaven.
Library Dependencies: Concrete functies en bestaande lemma's die gebruikt zullen worden.
Bewijsverplichtingen: De brugpredicaat (bridging predicate), inductie-/case-structuur en verklaringen van noodzakelijke hulp-lemma's.

De agent valideert deze kandidaat-plannen op het niveau van de schets. Een plan wordt afgewezen als de programma-schets de instructies schendt, de decompositie de brugpredicaat niet behoudt, of als het predicaat de postconditie niet impliceert. De agent selecteert het plan dat de verwachte bewijslast minimaliseert.

2.2 Plan-gestuurde Elaboratie

Zodra een plan $\rho$ is geselecteerd, gaat de agent de elaboratiefase in:

Implementatie: De agent schrijft de code ( $\pi$ ) strikt volgens de decompositie en structuur die in $\rho$ zijn vastgelegd.
Bewijs-scaffold: De agent schrijft een bewijs-skelet ( $\kappa$ ) dat de structuur van het plan spiegelt (bijv. specifieke inductieprincipes of case splits), waarbij lokale hiaten (gerepresenteerd als sorry) worden achtergelaten voor gedetailleerde tactieken.
Verfijning: De agent gebruikt Lean 4-feedback (via LSP/MCP) om deze hiaten in te vullen. Cruciaal is dat als lokale reparaties herhaaldelijk falen of als de brugpredicaat te zwak blijkt te zijn, de agent dit identificeert als een plan-niveau fout. In plaats van te blijven rondhangen tussen code- en bewijs-edits, keert de agent terug naar de planningsfase om $\rho$ te herzien.

Deze scheiding maakt het mogelijk voor de agent om onderscheid te maken tussen elaboratie-niveau fouten (lokaal herstelbaar) en plan-niveau fouten (vereisen een structurele heroverweging), wat de zoekruimte aanzienlijk verkleint.

3. Benchmark: Lean4Commit0

Om geverifieerde codegeneratie te evalueren in realistische settings die verder gaan dan tekstboekalgoritmen, introduceren de auteurs Lean4Commit0.

Bron: Afgeleid van 108 real-world open-source bibliotheken in Python, Rust, C/C++ en Java.
Scope: Het extraheert kern-API's en codeert hun gedrag als Lean-taken, inclusioneel van relationele specificaties die het gezamenlijke gedrag van meerdere functies beperken (bijv. consistentie tussen set en get operaties).
Kwaliteitscontrole: Een driestaps-pipeline waarborgt de kwaliteit van de specificaties:
1. Referentie-satisfactie: Verifieert dat de originele bibliotheekimplementatie voldoet aan de Lean-specificatie.
2. Mutatie-afwijzing: Zorgt ervoor dat de specificatie gedragsveranderende mutanten afwijst (voorkomt onder-geconstraineerde specificaties).
3. LLM Review: Vlagt triviale of irrelevante specificaties.
Schaal: De uiteindelijke benchmark bevat 511 implementatie-placeholders en 519 theorem-placeholders.

4. Experimentele Resultaten

De auteurs hebben P3 geëvalueerd tegen twee baselines — een PLAIN agent (geen specifieke strategie) en een SEQ (programma-dan-bewijs) agent — met gebruik van vier frontier LLM backends (Codex-GPT-5.5, Gemini-3-Pro, Claude-Sonnet-4.6, Claude-Opus-4.7) over drie benchmarks: Verina, AlgoVeri, en Lean4Commit0.

Oplossingspercentages: P3 behaalde het hoogste oplossingspercentage in elke (benchmark, model) configuratie.
- Vergeleken met de sterkere baseline verbeterde P3 de oplossingspercentages met 4,6–11,2 procentpunt.
- Op de moeilijke subset van benchmarks verminderde P3 de API-kosten per taak met tot wel ~40% en de wandkloktijd met tot wel ~37%.
Ablatie-studie: Een vergelijking met PLAN-SEQ (die implementatiekeuzes plant maar geen bewijsstructuur) toonde aan dat gezamenlijke planning specifiek bijdraagt aan een extra winst van 3,3–8,3 procentpunt. Dit isoleert het voordeel van het anticiperen op de bewijsstructuur tijdens de planningsfase.
Casestudy: In een taak betreffende de verwijdering uit een left-leaning red-black tree, faalde de programma-dan-bewijs baseline of slaagde zij slechts met redundante rebuild-invarianten (1.176 regels) na het genereren van 6.344 regels code. P3 loste de taak op in 1.105 regels door plannen te vergelijken voordat er een commitment werd gedaan.

5. Betekenis en Claims

Het artikel claimt dat P3 aantoont dat geverifieerde codegeneratie effectiever en efficiënter kan worden gemaakt door het programma en het bewijs te behandelen als co-ontworpen artefacten in plaats van sequentiële outputs.

Structurele Consistentie: Door een gedeeld structureel plan vast te stellen, zorgt P3 ervoor dat de implementatie en het bewijs "by construction" consistent zijn, waardoor post-hoc reconciliatie wordt voorkomen.
Schaalbaarheid naar Real-World Code: De introductie van Lean4Commit0 overbrugt de kloof tussen academische benchmarks (tekstboekalgoritmen) en productiesoftware (relationele API-constraints), wat aantoont dat gezamenlijke planning bijzonder voordelig is voor complexe, bibliotheek-niveau taken.
Efficiëntie: Het framework vermindert het "thrashing" gedrag dat gebruikelijk is bij iteratieve reparatielussen, wat leidt tot aanzienlijke besparingen in computationele middelen en tijd.

De auteurs concluderen dat hoewel de verifieerder (Lean 4) de uiteindelijke autoriteit blijft, het vermogen van de agent om het programma en het bewijs gezamenlijk te plannen de kans aanzienlijk vergroot om een geverifieerde oplossing te produceren binnen praktische middelen.