SorryDB: Can AI Provers Complete Real-World Lean Theorems?

Dit artikel introduceert SorryDB, een dynamisch benchmark voor Lean-formalisaties dat is opgezet om AI-provers te evalueren aan de hand van real-world taken, waarbij blijkt dat huidige benaderingen complementair zijn en geen enkele methode alle andere volledig overtreft.

De kern

Stel je voor dat wiskundigen een gigantische, complexe bouwplaat aan het samenstellen zijn. Ze gebruiken een speciale taal (Lean) om hun ideeën zo precies mogelijk op te schrijven, zodat een computer kan controleren of er geen foutjes in zitten. Maar vaak laten ze stukken van de bouwplaat nog even open, met een post-it erop waarop staat: "Hier moet ik nog even aan werken" of "Ik weet het nu nog niet, maar ik kom er later op terug." In de programmeertaal van Lean noemen ze deze open plekken "sorry".

Dit paper introduceert SorryDB, een nieuw en slim systeem om te testen hoe goed kunstmatige intelligentie (AI) deze open plekken kan opvullen.

Hier is de uitleg, vertaald naar alledaags taalgebruik:

1. Het Probleem: De "Olympiade" is te makkelijk

Tot nu toe werden AI's getest op wiskundepuzzels die leken op die van de Internationale Wiskunde Olympiade (zoals miniF2F of PutnamBench).

• De analogie: Dit is alsof je een AI traint door hem alleen maar te laten racen op een perfect geasfalteerde racecircuit. Hij wordt heel snel, maar als je hem daarna de echte wereld in stuurt (met modder, gaten en onverwachte obstakels), faalt hij.
• Het probleem: Die oude tests zijn "verzadigd". De AI's hebben de antwoorden waarschijnlijk al in hun geheugen opgeslagen (geleerd uit hun trainingsdata). Ze kunnen de puzzels oplossen, maar ze begrijpen niet hoe ze in een echt, chaotisch project moeten werken.

2. De Oplossing: SorryDB (De "Live" Werkplek)

In plaats van oude puzzels te gebruiken, heeft het team SorryDB bedacht.

• Hoe het werkt: Ze kijken naar 78 echte, levende projecten op GitHub waar wiskundigen momenteel aan werken. Ze zoeken naar alle plekken waar een "sorry" staat.
• De analogie: In plaats van een AI te laten racen op een circuit, zetten we hem in een actieve bouwput. De AI moet niet een oude, bekende puzzel oplossen, maar een echte, nog onopgeloste klus klaren waar een menselijke bouwvakker net even de tijd voor heeft genomen om later terug te komen.
• Het voordeel: Omdat deze projecten elke dag veranderen en nieuwe "sorry's" toevoegen, kan de AI het antwoord niet simpelweg "uit het hoofd leren". Het is een levend benchmark: zodra AI's slimmer worden, worden de taken moeilijker, omdat de makkelijkste "sorry's" al zijn opgelost.

3. De Test: Wat kan de AI?

De auteurs hebben verschillende soorten AI's getest om te zien wie de "sorry's" het beste kon opvullen:

• De "Alleskenners" (Grote Taalmodellen): Modellen zoals Gemini, Claude en GPT. Dit zijn de brede denkers.
• De "Specialisten": AI's die specifiek zijn getraind op wiskunde (zoals Goedel Prover).
• De "Agenten": AI's die niet alleen een antwoord geven, maar ook zelf kunnen zoeken in bibliotheken, fouten kunnen zien en het proberen te verbeteren (zoals een mens die "probeer maar eens, oh foutje, probeer het anders").
• De "Automaten": Simpele, vaste regels (tactics) die alleen heel simpele dingen kunnen.

4. De Resultaten: Samenwerking is de sleutel

De resultaten waren verrassend en leerzaam:

• Geen enkele winnaar: Er was geen enkele AI die alles kon. De "specialisten" waren goed in specifieke wiskundige puzzels, maar faalden in de echte, rommelige projecten. De "alleskenners" waren beter, maar misten soms de diepte.
• De kracht van feedback: De winnaars waren de AI's die iteratief werkten. Ze gaven een antwoord, keken of de computer een foutmelding gaf, en probeerden het opnieuw.
  • Analogie: Het is alsof je een auto rijdt. Als je alleen maar naar de kaart kijkt (één keer een antwoord geven), kom je vast te zitten. Maar als je naar de GPS kijkt, ziet dat je een afslag mist, en dan de route opnieuw berekent, kom je wel aan. AI's die dit deden, presteerden veel beter.
• Complementair: De beste AI's vullen elkaar aan. Wat de ene niet kan, kan de andere wel. Als je ze allemaal samen gebruikt, kun je veel meer "sorry's" oplossen dan met één model.

5. Waarom is dit belangrijk?

Dit paper zegt eigenlijk: "Stop met het testen van AI's op oude, verzadigde puzzels. Laten we ze testen op de echte, moeilijke klussen die wiskundigen nu doen."

• Voor wiskundigen: Het betekent dat we binnenkort AI-assistenten kunnen krijgen die echt helpen bij het bouwen van nieuwe wiskundige theorieën, in plaats van alleen maar oude examenvragen op te lossen.
• Voor de toekomst: SorryDB blijft groeien en veranderen. Het is een "bewegend doelwit" dat meegroeit met de technologie. Zodra AI's slimmer worden, wordt de benchmark zwaarder, zodat we altijd weten wat de echte grenzen zijn.

Kortom: SorryDB is de eerste "live test" om te zien of AI's echt kunnen helpen bij het bouwen van de toekomst van de wiskunde, in plaats van alleen maar te racen op een oude racebaan.

Technische samenvatting

Probleemstelling

Huidige benchmarks voor geautomatiseerd wiskundig redeneren (zoals miniF2F, PutnamBench en IMO-gerelateerde datasets) vertonen drie fundamentele tekortkomingen:

1. Misalignering met de praktijk: Deze benchmarks bestaan voornamelijk uit competitiewiskunde (olympiade-niveau). Ze missen de complexiteit van echte formalisatieprojecten, zoals afhankelijkheden van specifieke projectdefinities, grotere context en de "rommeligheid" van real-world code.
2. Verzadiging en data-contaminatie: Bestaande datasets zijn vaak verzadigd; modellen hebben de oplossingen mogelijk al gezien tijdens het trainen, wat het onderscheid tussen memorisatie en echt redeneren onmogelijk maakt.
3. Beperkte evaluatie van praktische bruikbaarheid: Modellen die goed presteren op competitieproblemen, falen vaak bij het invullen van ontbrekende bewijzen in lopende, open-source Lean-projecten, waar lokale context en bestaande bibliotheken cruciaal zijn.

Er is behoefte aan een dynamische benchmark die de dagelijkse werking van een Lean-ontwikkelaar nabootst en continu nieuwe, onopgeloste taken aanbiedt.

Methodologie: SorryDB

De auteurs introduceren SorryDB, een dynamisch, continu-updatend benchmark-systeem dat is afgeleid van open-source Lean-projecten op GitHub.

• Dataverzameling: Het systeem scant 78 actieve Lean-repositories (uit het Lean Reservoir package registry) die recent commits hebben ontvangen. Het identificeert alle sorry-keywords. In Lean fungeert sorry als een tijdelijke placeholder voor een nog niet bewezen stelling of stap in een bewijs.
• Taakdefinitie: De evaluatietaak is "fill-in-the-sorry": geef de code die de sorry-placeholder vervangt zodat het specifieke bewijsdoel wordt bereikt en het project compileert zonder sorry.
• Validatie: Een geautomatiseerde pijplijn kloon het specifieke repository, vervangt de sorry door het voorstel van het model, en controleert of het project succesvol compileert zonder resterende sorry-termen. Dit is strikter dan alleen syntactische validatie.
• Dataset: Voor de experimenten werd een statische snapshot gebruikt (SorryDB-2601) met een cutoff van januari 2026, bestaande uit 5.663 taken. Voor de evaluatie werd een representatieve subset van 1.000 recente taken geselecteerd om diversiteit te maximaliseren.

Belangrijkste Bijdragen

1. De SorryDB Dataset: Een dynamische dataset die is opgebouwd uit onopgeloste bewijsverplichtingen uit echte, lopende projecten. Dit zorgt voor een benchmark die meegroeit met de staat van de kunst en niet verzadigd raakt.
2. Evaluatiekader: Een robuust mechanisme om oplossingen deterministisch te valideren via compilatie en het controleren van de bewijstoestand, zonder de noodzaak van handmatig gelabelde "ground truth" oplossingen.
3. Uitgebreide Evaluatie: Een analyse van diverse benaderingen (deterministische tactieken, algemene LLM's, gespecialiseerde modellen en agentische systemen) op deze realistische dataset.

Resultaten

De auteurs evalueerden verschillende modellen op de 1.000-taken subset. De belangrijkste bevindingen zijn:

• Complementariteit: Geen enkel model lost alle taken op. De resultaten tonen aan dat verschillende benaderingen complementair zijn; elk model slaagt op een andere subset van problemen. Een gecombineerde aanpak (waarbij de beste oplossing van alle modellen wordt genomen) bereikte een succespercentage van 35,7%, wat aanzienlijk hoger is dan elk individueel model.
• Iteratie en Feedback is Cruciaal:
  • Self-correcting en Agentische benaderingen presteerden aanzienlijk beter dan "one-shot" (pass@1) benaderingen.
  • Modellen die gebruikmaken van iteratieve feedback (waarbij foutmeldingen van de compiler worden gebruikt om het bewijs te corrigeren) behaalden successen van rond de 27-30%.
  • Zelfs met een beperkt aantal calls (16 iteraties) overtroffen iteratieve methoden parallelle sampling (pass@32) van statische modellen. Dit benadrukt dat toegang tot de projectomgeving en compilatie-feedback belangrijker is dan alleen een groter redeneerbudget.
• Prestatieverschillen per Categorie:
  • Taken uit pedagogische repositories waren het makkelijkst op te lossen.
  • Taken uit formalisatieprojecten (zoals Fermat's Last Theorem of Carleson's theorem) waren het moeilijkst.
  • Gespecialiseerde modellen (zoals Goedel Prover) presteerden relatief goed op benchmark-datasets, maar minder goed op andere projecttypes, waarschijnlijk door training op oudere Lean-versies of een focus op competitiewiskunde.
• Rol van Tools: Agentische modellen die zoektools gebruikten (zoals LeanSearch) faalden soms omdat ze te afhankelijk werden van het zoeken naar bestaande lemmata in plaats van zelf een nieuw bewijs te construeren. In sommige gevallen presteerde een model zonder tools (die direct het bewijs construeerde) beter.

Significantie

SorryDB markeert een verschuiving in de evaluatie van AI voor wiskundig redeneren:

• Van Competitie naar Praktijk: Het verplaatst de focus van het oplossen van geïsoleerde olympiade-problemen naar het bijdragen aan levende, complexe wiskundige projecten.
• Robuustheid: Door continu nieuwe taken toe te voegen, wordt het risico op data-contaminatie geminimaliseerd en blijft de benchmark relevant naarmate AI-modellen verbeteren.
• Inzicht in Grenzen: De studie toont aan dat huidige state-of-the-art modellen nog niet in staat zijn om de meerderheid van de real-world bewijzen te voltooien, maar dat iteratieve, agentische systemen met feedback het meest veelbelovend zijn. Het benadrukt dat succes in de praktijk vaak vraagt om een combinatie van het construeren van nieuwe argumenten en het slim benutten van bestaande bibliotheken.

Kortom, SorryDB biedt een noodzakelijke, realistische testomgeving om de daadwerkelijke bruikbaarheid van AI-assistenten voor wiskundigen te meten, in plaats van alleen hun vermogen om competitieproblemen op te lossen.