Wanneer AI de code schrijft, wie bewijst dan dat het werkt?

Wat is formele verificatie?

Voor iemand die gewend is aan code-reviews, QA en testen, is formele verificatie een fundamenteel andere benadering. Lean is zowel een programmeertaal als een proof assistant. Hiermee kan men niet alleen code schrijven, maar ook eigenschappen definiëren waaraan die code moet voldoen. Men kan openstaande wiskundige conjectures formuleren en bewijzen leveren voor deze claims.

Het cruciale verschil is dat het bewijs niet informeel is, maar geschreven in de Lean-taal en door een machine wordt gecontroleerd (machine-checked). Om een resultaat te vertrouwen dat met Lean is bewezen, hoeft men enkel de 'kernel' te vertrouwen—het onderdeel waar het bewijs daadwerkelijk wordt gecontroleerd.

Verificatie versus traditioneel testen

Traditioneel testen is zeer nuttig voor het vinden van bugs, maar het is niet in staat om te bewijzen dat er geen bugs zijn. Testing toont de aanwezigheid van fouten aan, niet de afwezigheid ervan.

Met formele verificatie begint men bij de eigenschappen. Men kan AI vragen om code te implementeren die aan specifieke eigenschappen voldoet en om een Lean-bewijs te leveren dat dit aantoont. Een voorbeeld hiervan is het porten van zlib (een compressiebibliotheek) naar Lean. Hierbij is een eigenschap bewezen die stelt dat wanneer data wordt gecomprimeerd en vervolgens gedecomprimeerd, de oorspronkelijke data exact terugkomt zonder verlies of corruptie.

AI en de versnelling van formele verificatie

Autoformalisatie

Een belangrijke ontwikkeling is autoformalisatie: het vermogen van frontier-modellen om code of wiskundige teksten (bestaande uit woorden en symbolen) te vertalen naar Lean. Dit stelt ontwikkelaars in staat om bestaande code in elke wislige taal om te zetten naar een Lean-model voor verificatie.

Voor Rust-code bestaat er een specifieke tool genaamd Aeneas, die wordt gebruikt door teams zoals het SymCrypt-team bij Microsoft om cryptografische bibliotheken te verifiëren.

Schaalbaarheid en AI-bewijzen

De schaal van bewijzen is door AI explosief gegroeid. De menselijke wiskundige bibliotheek voor Lean, Mathlib, telt 2,5 miljoen regels en deed er tien jaar over om te worden opgebouwd. Inmiddels zijn er AI-gegenereerde bewijzen van 50 miljoen regels. Het bewijs voor de Laatste Stelling van Fermat, geschreven door de AI van Anthropic, bevat bijvoorbeeld 13 miljoen regels.

De betrouwbaarheid van AI-modellen

Bij het gebruik van AI om een model van software in Lean te maken, rijst de vraag: is dit model getrouw (faithful) aan de oorspronkelijke code?

Om dit te controleren, wordt gebruikgemaakt van differential testing, waarbij het Lean-model en het daadwerkelijke programma naast elkaar worden gedraaid om discrepanties te vinden. Er zijn al gevallen bekend waarbij AI (zoals Claude) werd gevraagd om bugs in zijn eigen code (Claude Code) te vinden via Lean, wat leidde tot echte bugfixes.

De Navier-Stokes casus

Een voorbeeld van de subtiliteit van dit proces is het bewijs voor de Navier-Stokes-vergelijkingen. Er ontstond controverse omdat het informele bewijs in natuurlijke taal en het formele bewijs in Lean niet volledig overeenkwamen (bijvoorbeeld over het gebruik van een vierde versus een vijfde afgeleide).

Om dit soort mismatches te voorkomen, is er de tool Verso Blueprint. Deze maakt het mogelijk om natuurlijke taal en LaTeX te mengen met Lean, waardoor de presentatie en het formele bewijs beter op elkaar afgestemd kunnen worden.

De toekomst van Software Engineering

De focus van de software engineer verschuift van het schrijven van code naar het definiëren van requirements en specificaties. Er ontstaan twee kritieke kloven:

1. De requirement-kloof: Het verschil tussen wat men wil en wat men kan opschrijven.
2. De model-kloof: De vraag of de testomstandigheden representatief zijn voor de productieomgeving.

De geverifieerde softwarestack

De visie van de "verified stack" richt zich op kritieke softwarecomponenten:

• Besturingssystemen;
• Compilers;
• Communicatielagen (zoals TCP/IP).

Wanneer een leverancier claimt dat software "formeel geverifieerd" is, zijn de belangrijkste vragen om de validiteit te controleren:

• Welke specificaties en eigenschappen zijn precies geverifieerd?
• Welke proof checker kernel is gebruikt?
• Hoe groot is de trusted codebase?

AI-Agents en beveiliging

Voor autonome agenten betekent verificatie vooral het creëren van betrouwbare sandboxes en het handhaven van strikte policies. Omdat agenten zeer goed zijn in het vinden van kwetsbaarheden, is het essentieel dat de code die deze policies afdwingt formeel geverifieerd is. Om te voorkomen dat een agent een fout in één specifieke kernel exploiteert, kan men gebruikmaken van meerdere, onafhankelijk geïmplementeerde kernels (bijvoorbeeld in Rust, C#, Haskell of zelfs TeX).

Impact op Wiskunde en Natuurkunde

Wiskunde is het ideale domein voor formele verificatie omdat definities er inherent precies zijn. Met Mathlib kunnen wiskundigen nu op een schaal werken die voorheen onmogelijk was. Terence Tao heeft bijvoorbeeld projecten opgezet waarbij hij als architect fungeerde en anderen (of AI) de "gaten" in het bewijs vulden, waarbij Lean zorgde voor de verificatie van de bijdragen.

Theoretische Natuurkunde

In de theoretische natuurkunde begint dit proces ook vorm te krijgen via Physlib. Hoewel natuurkunde modellen van de echte wereld gebruikt (die inherent onprecies zijn), kunnen de wiskundige modellen binnen die theorieën wel formeel geverifieerd worden. Er zijn al gevallen bekend waarbij formele verificatie bugs in belangrijke natuurkundige papers heeft blootgelegd.

De verschuiving van IQ naar Compute

Er vindt een verschuiving plaats in wie "wint" in de academische wereld. Waar voorheen rauwe intelligentie en het vermogen om mentale pijn te verdragen (het moeizame proces van bewijzen) doorslaggevend waren, wordt toegang tot rekenkracht (compute) steeds belangrijker. De persoon met het grootste cluster kan meer bewijzen genereren en verifiëren dan iemand zonder die middelen.

Toepassingen in andere domeinen

Naast wiskunde en software engineering is er interesse in andere velden:

• Financiën: Het formaliseren van handelsalgoritmen en de wiskundige achtergrond van financiële instrumenten.
• Chemie en Biologie: Het bouwen van libraries voor wetenschappelijke precisie.
• Recht: Hoewel recht vaak subjectief is, zijn bepaalde delen, zoals civiele procedures, zeer formulaic en bijna als een programma te beschouwen, wat ze geschikt maakt voor formalisatie.
• Accountancy: Het vertalen van algemeen aanvaarde boekhoudprincipes (GAAP) en belastingwetgeving naar formele regels.