FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?

Dit artikel presenteert FormalProofBench, een privé-benchmark die de prestaties van geavanceerde AI-modellen evalueert bij het genereren van formeel geverifieerde wiskundige bewijzen op afgestudeerdenniveau in Lean 4, waarbij de beste modellen een nauwkeurigheid van 33,5% bereiken.

De kern

Stel je voor dat wiskundigen al eeuwenlang in een enorme bibliotheek werken. Soms schrijven ze een bewijs op een kladblaadje (in gewone taal) en zeggen: "Kijk, dit klopt wel." Maar in die wereld van de geavanceerde wiskunde is "het klinkt wel logisch" niet genoeg. Een klein foutje, een gemiste uitzondering of een onbestaande regel kan het hele bewijs doen instorten.

Tot nu toe moesten mensen die bewijzen handmatig nakijken, wat traag is en fouten kan missen. Maar nu komen er slimme computers (AI) die kunnen "denken". De vraag is: kunnen deze computers niet alleen een verhaal schrijven dat klinkt als een wiskundig bewijs, maar ook een bewijs dat onweerlegbaar klopt volgens de strenge regels van de wiskunde?

Dit is precies wat het nieuwe onderzoek "FormalProofBench" onderzoekt. Hier is een uitleg in simpele taal, met wat creatieve vergelijkingen.

1. De Proef: Een Striktest voor AI

De onderzoekers hebben een speciale test ontwikkeld, een soort "rijbewijstest" voor wiskundige AI's.

• Het probleem: Ze geven de AI een moeilijke wiskundevraag uit een universitair vak (zoals analyse, algebra of kansrekening).
• De opdracht: De AI moet het antwoord niet in gewone taal schrijven, maar in een speciale programmeertaal genaamd Lean 4.
• De scheidsrechter: Er is geen menselijke jury die oordeelt of het "klinkt goed". Er is een computerprogramma (de Lean-kernel) dat als een onverbiddelijke scheidsrechter fungeert. Als het bewijs ook maar één klein foutje bevat, zegt de computer: "FAIL". Als het perfect is, zegt hij: "PASS".

Het is alsof je een architect vraagt om een brug te ontwerpen. Bij de oude manier keek een mens naar de tekening en zei: "Ja, dat ziet er stevig uit." Bij deze nieuwe manier moet de AI de brug in de computer bouwen. Als de brug ook maar één balkje verkeerd staat, stort hij in de simulatie in. Dan is het bewijs niet geldig.

2. De Testomgeving: Een Werkplaats met Hulpmiddelen

De AI's kregen niet alleen de vraag, maar ook een gereedschapskist:

• Een zoekmachine: Om te kijken of er al bewezen regels zijn die ze kunnen gebruiken (zoals een naslagwerk).
• Een testbaan: Om stukjes code uit te voeren en te zien of ze werken.
• 40 rondes: Ze hadden 40 keer de kans om te proberen, te falen, te leren van de fout en het opnieuw te proberen.

3. De Resultaten: De Top is goed, maar de rest hinkt

De onderzoekers lieten de slimste AI's ter wereld (zoals die van Anthropic, OpenAI en Google) deze test doen.

• De winnaar: De beste AI (Claude Opus 4.5) slaagde voor 33,5% van de vragen. Dat klinkt misschien niet als 100%, maar in de wereld van geformaliseerde wiskunde is dat een enorme prestatie. Het betekent dat de AI al een kwart van de zeer moeilijke universiteitsopgaven volledig foutloos kon oplossen.
• De val: Na die ene top viel de prestatie van de andere AI's snel af. De meeste haalden minder dan 15%.

De belangrijkste les: De AI's die het beste deden, waren niet degene die het hardst zochten in de boeken. De winnaars waren degene die vaak testten. Ze bouwden een stukje, keken of het crashte, pasten het aan, en bouwden weer. Het was meer "probeer-en-fout" dan "alleen maar nadenken".

4. Waarom is dit belangrijk?

Stel je voor dat wiskundigen in de toekomst een assistent hebben die niet alleen helpt met het bedenken van ideeën, maar ook direct controleert of die ideeën wiskundig waterdicht zijn.

• Geen meer "schijnbewijzen": Vaak zeggen mensen dat iets waar is, maar blijkt later dat er een gat in zit. Een AI die Lean 4 spreekt, kan die gaten direct zien.
• Snelheid: Wat nu maanden duurt om te controleren, kan binnen enkele uren gebeuren.
• Toekomst: Hoewel de AI's nu nog "studenten" zijn die soms struikelen, laat deze test zien dat we dichtbij een punt zitten waar computers echt nuttige hulpmiddelen worden voor de geavanceerde wetenschap.

Samenvattend

Dit onderzoek is als een grote examenwedstrijd voor AI's. Ze kregen de opdracht: "Bouw een brug die perfect staat volgens de wetten van de natuurkunde." De beste AI's konden dat voor een derde van de opdrachten. Het laat zien dat AI's niet alleen kunnen "kletsen" over wiskunde, maar dat ze langzaam maar zeker leren om de taal van de wiskunde echt te spreken en te controleren. Het is een eerste stap naar een toekomst waarin computers onze wiskundige ontdekkingen helpen verifiëren.

Technische samenvatting

Titel: FormalProofBench: Kunnen modellen graduate-niveau wiskundige bewijzen schrijven die formeel geverifieerd zijn?

Publicatie: ICLR 2026 (Conference Paper)
Auteurs: Nikil Ravi et al. (Vals AI, EPFL, MIPT, Indiana University, Independent Researcher)

---

1. Het Probleem

Hoewel grote taalmodellen (LLM's) aanzienlijke vooruitgang hebben geboekt in wiskundig redeneren op benchmarks zoals MATH en AIME, blijven deze systemen beperkt tot informele, natuurlijke taaloplossingen. Deze oplossingen kunnen subtiele logische fouten bevatten die moeilijk te detecteren zijn, zelfs voor menselijke experts of andere AI-systemen. Een model kan een plausibel klinkend argument geven dat een kritiek geval mist of een niet-bestaand lemma aanroept.

Er is een behoefte aan een evaluatiemethode die objectieve, machine-verifieerbare correctheid garandeert. Bestaande formele benchmarks richten zich vaak op olympiade-niveau of undergraduate-stof, of evalueren modellen in één enkele doorloop zonder interactie. Er ontbreekt een robuuste benchmark voor graduate-niveau wiskunde die gebruikmaakt van een agentische omgeving (meerdere interactierondes) om te testen of modellen complexe, machine-controleerbare bewijzen kunnen genereren.

2. Methodologie

De Benchmark: FormalProofBench

FormalProofBench is een gesloten (private) benchmark ontworpen om de capaciteit van AI-modellen te evalueren om formeel geverifieerde bewijzen te produceren voor problemen op het niveau van geavanceerde bachelor- en masteropleidingen.

• Data: De benchmark bestaat uit 200 problemen afkomstig uit kwalificatie-examens en standaardhandboeken.
• Domeinen: De problemen dekken een breed spectrum: maattheorie, reële en functionele analyse, algebra, algebraïsche meetkunde, getaltheorie, kansrekening/stochastische analyse en logica.
• Formalisatie: Elk probleem bestaat uit een informele tekst en een bijbehorende formele statement in Lean 4 (met het Mathlib-bibliotheek). Alle formalisaties zijn geschreven door ervaren Lean-gebruikers (PhD-studenten en experts) en hebben een tweedegraads review-proces ondergaan om misformalisaties te voorkomen.
• Validatie: Correctheid is binair en volledig geautomatiseerd: een bewijs is alleen correct als het compileert en wordt geaccepteerd door de Lean 4-kernel. Er wordt geen credit gegeven voor plausibel maar foutief redeneren.

Evalueringsomgeving (Agent Harness)

In tegenstelling tot eerdere benchmarks die vaak een "single-shot" aanpak gebruiken, evalueren de auteurs modellen in een agentische lus:

• Input: Het model krijgt de informele probleemstelling, de formele Lean-statement, headers en context.
• Tools: Het model heeft toegang tot:
  • lean_loogle: Zoeken in Mathlib voor theorema's en definities.
  • lean_run_code: Uitvoeren van Lean-code om feedback te krijgen over fouten, type-mismatches, onopgeloste doelen, etc.
  • submit_proof: Inleveren van het definitieve bewijs.
• Interactie: Per probleem heeft het model maximaal 40 beurten (turns). Elke beurt kan meerdere tool-aanroepen bevatten.
• Beperkingen: Het gebruik van sorry (placeholders) of axioma's om het verifiëren te omzeilen wordt geweigerd.

3. Belangrijkste Bijdragen

1. Nieuwe Benchmark: Introduceert FormalProofBench, een uitdagende, deterministisch te evalueren benchmark voor graduate-niveau formele theorema-bewijzen, vrij van data-contaminatie.
2. Gedetailleerde Evaluatie: Biedt een uitgebreide analyse van state-of-the-art foundation modellen op 200 zorgvuldig geformaliseerde problemen.
3. Tool-gebruik Analyse: Onderzoekt de kosten, latentie en strategieën van modellen in een realistische multi-turn omgeving met zoek- en uitvoertools.
4. Empirische Bevindingen: Ontdekt dat frequente iteratie via code-uitvoering sterk correleert met succes, terwijl excessief zoeken zonder uitvoeren vaak leidt tot falen.
5. Prestatiebenchmark: Vaststellen dat zelfs de beste modellen momenteel slechts een beperkt succespercentage halen, wat de complexiteit van het domein onderstreept.

4. Resultaten

De auteurs hebben een reeks frontier-modellen geëvalueerd (OpenAI, Anthropic, xAI, Google, DeepSeek, Zhipu AI).

• Top Prestatie: Claude Opus 4.5 (Thinking) behaalde de hoogste nauwkeurigheid van 33,5%.
• Afname: De prestaties dalen snel na de top. De tweede beste (Gemini 3 Pro) haalde 18,5%, en de meeste andere modellen bleven onder de 15%.
• Kosten en Latentie: De evaluatie is kostbaar en tijdrovend. De gemiddelde kosten per test variëren van $0,10 tot $1,34. De latentie is aanzienlijk; modellen nemen gemiddeld meer dan een uur (tot wel 11.000 seconden) om tot een definitieve inzending te komen, voornamelijk door de iteratieve aard van het proces.

Tool-gebruik Patronen:

• Code-uitvoering: Modellen die vaker lean_run_code gebruiken om feedback te krijgen en hun bewijzen te itereren, presteren significant beter.
• Zoekgedrag: Een veelvoorkomende faalmodus is "spiraalvormig" zoeken (lean_loogle) naar niet-bestaande lemma's zonder daadwerkelijke code-uitvoering. Succesvolle modellen gebruiken zoeken strategisch om gaten op te vullen, maar vertrouwen primair op uitvoering voor validatie.

5. Betekenis en Toekomstperspectief

• Brug tussen Informeel en Formeel: De benchmark blootlegt dat er nog een groot gat bestaat tussen informeel wiskundig vermogen en formeel bewijsvoering. Hoewel AI-systemen snel verbeteren, is de formalisatie nog steeds een bottleneck.
• Praktische Toepassing: De snelle vooruitgang suggereert dat we een drempel naderen waarbij AI-systemen praktische hulpmiddelen kunnen worden voor werkende wiskundigen. Succesvolle formele verificatie kan de exploratie van bewijsstrategieën versnellen en de toegang tot formele methoden democratiseren.
• Toekomstige Richtingen: De auteurs stellen voor om de tool-configuratie te verbeteren (bijv. semantische zoekopdrachten), de invloed van de informele probleemstelling te ablaten, de dataset uit te breiden naar meer domeinen, en uiteindelijk te evolueren naar het evalueren van bewijzen op het niveau van actueel wetenschappelijk onderzoek (research-level).

Conclusie: FormalProofBench biedt een rigoureuze, onafhankelijke maatstaf voor de voortgang van AI in wiskunde. Hoewel de huidige beste modellen slechts ongeveer een derde van de problemen correct kunnen oplossen, toont het onderzoek aan dat interactieve, tool-gebaseerde agenten de meest veelbelovende route zijn naar het overwinnen van de complexiteit van graduate-niveau wiskundige bewijzen.