LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)

Dit paper introduceert LeanCat, een uitdagende benchmark voor formeel categorietheorie in Lean die aantoont dat de huidige staat van de kunst een groot abstractieprobleem heeft, maar dat een agent met ophaal- en verificatiemechanismen (LeanBridge) de prestaties kan verdubbelen door iteratieve verfijning en dynamische bibliotheekretrieval.

De kern

LeanCat: Een Nieuwe Test voor AI's Wiskundige Brein

Stel je voor dat wiskunde een enorme bibliotheek is vol met boeken. De meeste AI-modellen (zoals de slimme chatbots die we vandaag kennen) zijn getraind om korte, slimme raadsels op te lossen, zoals olympiade-vraagstukken. Ze zijn goed in het vinden van een snelle, slimme truc om een probleem op te lossen. Maar echte wiskundigen werken niet zo. Ze bouwen aan enorme, complexe gebouwen waar elke steen perfect past in een groter, abstract raamwerk.

Dit paper introduceert LeanCat, een nieuwe test die precies kijkt of AI's die grote, abstracte gebouwen kunnen bouwen, in plaats van alleen raadsels op te lossen.

Hier is een eenvoudige uitleg van wat ze hebben gedaan, met behulp van een paar creatieve vergelijkingen:

1. Het Probleem: De "Abstractie-Gap"

Stel je voor dat je een AI vraagt om een huis te bouwen.

• De oude tests (zoals miniF2F) vragen: "Hoeveel bakstenen heb je nodig voor een muur van 2 meter?" Dit is een rekensom.
• De nieuwe test (LeanCat) vraagt: "Bouw een compleet stelsel van kanalen en afvoeren dat werkt volgens de wetten van de stroming, zonder dat je de blauwdrukken hoeft te tekenen, maar alleen door te verwijzen naar de bestaande bouwvoorschriften in de bibliotheek."

De auteurs ontdekten dat de slimste AI's momenteel vastlopen bij dit soort vragen. Ze kunnen de simpele rekensommen maken, maar zodra het gaat om complexe, abstracte concepten (in dit geval: Categorietheorie, een soort "taal van de taal" in de wiskunde), zakken ze door de vloer.

• Op makkelijke vragen scoren ze redelijk goed (55%).
• Op moeilijke, abstracte vragen scoren ze 0%.

Dit noemen ze de "Abstractie-Gap". De AI's zijn te goed in het raden van het antwoord, maar te slecht in het begrijpen van de diepe structuur en het gebruik van de juiste gereedschappen uit de bibliotheek.

2. De Oplossing: LeanBridge (De Slimme Boekhouder)

Om dit op te lossen, hebben de onderzoekers een nieuwe manier bedacht om de AI te laten werken, genaamd LeanBridge.

Stel je voor dat de AI niet alleen een slimme student is, maar een onderzoeker met een team.

• De oude manier (Statische AI): De student zit alleen in een kamer, mag geen boeken pakken en moet het antwoord uit zijn hoofd raden. Als hij het niet weet, probeert hij het gewoon opnieuw met een ander gokje.
• De nieuwe manier (LeanBridge): De onderzoeker mag boeken halen.
  1. Zoeken: Hij kijkt eerst in de bibliotheek (de wiskundige software-bibliotheek) om te zien welke definities en regels er al bestaan.
  2. Proberen: Hij probeert het probleem op te lossen met die informatie.
  3. Controleren: Als het niet lukt, kijkt hij naar de foutmelding (de "rekenmachine" zegt: "Dit klopt niet").
  4. Herhalen: Hij zoekt opnieuw, past zijn plan aan en probeert het opnieuw.

Dit noemen ze een "Zoek-Genereer-Verifieer" lus. Het is alsof je een puzzel oplost, maar elke keer als je vastloopt, mag je even in de handleiding kijken in plaats van blindelings te gissen.

3. De Resultaten: Een Groot Sprongje Voorwaarts

De resultaten van deze nieuwe test zijn verbluffend, maar ook een beetje teleurstellend voor de huidige stand van de techniek:

• De "Gewone" AI's: Zelfs de allerbeste modellen (zoals GPT-5 of Claude) konden maar 12% van de moeilijke problemen oplossen. Ze bleven steken bij de abstracte concepten.
• De "LeanBridge" AI: Door de AI de mogelijkheid te geven om actief in de bibliotheek te zoeken en fouten te analyseren, verdubbelde het succespercentage naar 24%.
• Het Grootste Succes: Voor het eerst in de geschiedenis slaagde een AI erin om een moeilijk probleem in deze categorie volledig op te lossen.

4. Waarom is dit belangrijk?

Dit paper laat zien dat we AI's niet alleen slimmer moeten maken door ze meer data te geven (meer "hersenen"), maar dat we ze slimmere hulpmiddelen moeten geven.

• Voor de AI-wereld: Het bewijst dat voor complexe taken (zoals wiskundig onderzoek of software-ontwikkeling) het niet genoeg is om alleen te "gokken". De AI moet actief kunnen zoeken, fouten analyseren en zijn kennis updaten.
• Voor de Wiskunde: Het helpt wiskundigen te zien waar hun eigen "bibliotheek" (de software die ze gebruiken om wiskunde te bewijzen) nog hiaten heeft. Als de AI vastloopt, is het misschien niet omdat de AI dom is, maar omdat er een belangrijk stukje in de bibliotheek ontbreekt.

Samenvatting in één zin

LeanCat is een nieuwe, zeer moeilijke test die laat zien dat AI's momenteel vastlopen in abstracte wiskunde, maar dat ze een enorme sprong vooruit maken als we ze toestaan om actief in de "bibliotheek" te zoeken en hun fouten te leren analyseren, net als een echte menselijke onderzoeker.

Technische samenvatting

Probleemstelling

Hoewel grote taalmodellen (LLMs) indrukwekkende prestaties leveren in formeel stellingenbewijzen, falen huidige benchmarks (zoals miniF2F of ProofNet) om library-grounded abstraction adequaat te meten. Dit is het vermogen om te redeneren met hoge-niveau interfaces en herbruikbare structuren, wat centraal staat in moderne wiskunde en software-engineering.

• De "Abstraction Gap": Bestaande datasets focussen vaak op olympiade-stijl problemen of berekeningen die korte, slimme trucs belonen. Ze testen niet het vermogen om langdurig te werken binnen rijke, abstracte kaders.
• De Uitdaging: Categorietheorie fungeert als de "interface-taal" van de moderne wiskunde (functoren, natuurlijke transformaties, adjuncties, limieten). Bewijzen hierin vereisen vaak diagrammatisch redeneren en het handhaven van universele eigenschappen, wat een strenge stress-test is voor de structurele redeneercapaciteit van AI.
• Huidige Beperkingen: State-of-the-art modellen tonen een drastische prestatiedaling naarmate de moeilijkheidsgraad toeneemt (van 55% op makkelijke taken naar 0% op moeilijke taken), wat aantoont dat ze worstelen met compositional generalization binnen complexe bibliotheken.

Methodologie

1. De LeanCat Benchmark

De auteurs introduceren LeanCat, een benchmark van 100 volledig geformaliseerde categorietheorie-taken in Lean 4 (met Mathlib).

• Structuur: De taken zijn verdeeld over acht thematische clusters: Basis eigenschappen, Adjuncties, Reflectieve subcategorieën, Concrete categorieën, Limieten/Colimieten, Cocompleties, Abelse categorieën en Monaden.
• Bronnen: Taken zijn afkomstig uit standaardhandboeken (bijv. Riehl, Mac Lane), ongepubliceerde collegeaantekeningen en onderzoekspapers.
• Ontwerp: Het is een "statement-level" benchmark. De modellen moeten een bewijs leveren voor een zelfstandige stelling zonder tussenstappen of hints, wat het vermogen test om definities te beheren en abstracties te navigeren.
• Moeilijkheidsgradatie: Een hybride annotatie-pipeline combineert LLM-schattingen (gebaseerd op succespercentages van meerdere modellen) en menselijke expert-judgment om taken te classificeren als Easy, Medium of High. De verdeling is bewust scheef (20 Easy, 40 Medium, 40 High) om te voorkomen dat huidige modellen te snel verzadigen.

2. Evaluatie-protocollen

De auteurs evalueren twee benaderingen:

• Statische Baselines (Parallel Sampling): Toepassing van state-of-the-art modellen (GPT-5.2, Claude-Opus-4.5, DeepSeek-Prover-V2, etc.) via pass@k sampling. Modellen zien alleen de formele Lean-stelling en moeten het bewijs direct genereren.
• LeanBridge (Agente Benadering): Een retrieval-augmented agent die een retrieve–generate–verify lus implementeert.
  • De agent gebruikt LeanExplore om dynamisch definities en lemma's uit de Mathlib-bibliotheek op te halen.
  • Het proces verloopt sequentieel: zoeken, genereren, verifiëren, en bij fouten de zoekopdracht verfijnen of het bewijs aanpassen.
  • Er worden twee input-instellingen getest: alleen natuurlijke taal (NL) en natuurlijke taal + formele stelling (NL+Statement).

Kernbijdragen

1. LeanCat Benchmark: De eerste suite van 100 problemen in categorietheorie, specifiek ontworpen om de kloof tussen "toy problems" en research-level formalisatie te dichten.
2. Hybride Moeilijkheidsannotatie: Een gestructureerde pipeline die LLM-prestaties en menselijke expertise combineert om betrouwbare labels (Easy/Medium/High) toe te kennen.
3. LeanBridge Agent: Een bewijsstelsel dat dynamische bibliotheekretrieval integreert, wat essentieel blijkt voor abstracte domeinen.
4. Empirische Validatie van Retrieval: Het paper levert bewijs dat iteratieve verfijning en dynamische tool-gebruik geen optionele optimalisaties zijn, maar strikte noodzaak voor neuro-symbolisch redeneren in abstracte domeinen.

Resultaten

• Prestatie van Statische Baselines:

  • De beste modellen (Claude-Opus-4.5) bereiken slechts 12,0% succes op pass@4.
  • Er is een catastrofale daling in prestaties: van 55% op makkelijke taken naar 0,0% op moeilijke taken. Dit bevestigt het bestaan van een grote "abstraction gap".
  • Gespecialiseerde bewijzers (zoals DeepSeek-Prover-V2) presteren zelfs slechter op medium/moeilijke taken, wat wijst op overfitting op trainingsdata met een lagere abstractieniveau.

• Prestatie van LeanBridge:

  • LeanBridge verdubbelt de succesratio van de beste statische baseline tot 24,0% (met GPT-5.2 en NL+Statement input).
  • Het is het enige systeem dat succesvolle bewijzen levert op High-difficulty taken (2,5% succes), terwijl alle statische baselines hier volledig falen.
  • Impact van Retrieval: Een ablatiestudie toont aan dat de agent zonder zoekfunctie ("No-Search") vastloopt op moeilijkere taken (0% op High). Dynamische retrieval is cruciaal om kennishopen te overbruggen.
  • Impact van Formele Grounding: Het toevoegen van de formele Lean-stelling aan de input (naast de natuurlijke taal) is doorslaggevend voor het oplossen van medium en moeilijke taken.

• Foutanalyse:

  • Veelvoorkomende fouten zijn niet alleen syntax, maar vooral semantisch: wiskundige strategie-fouten, hallucinatie van niet-bestaande lemma's, "lazy" fouten (waarbij de AI placeholder's gebruikt in plaats van bewijzen), en het vermijden van het definiëren van noodzakelijke tussenstappen.

Betekenis en Toekomstperspectief

• Voor AI-onderzoek: LeanCat demonstreert dat voor complexe wiskunde niet alleen meer sampling (test-time scaling) nodig is, maar wel agente workflows met actieve kennisretrieval. Het benadrukt de noodzaak van "abstraction-aware planning".
• Voor de Wiskundegemeenschap: De benchmark fungeert als een testbed om te identificeren welke delen van abstracte redenering nog ontbreken in bestaande bibliotheken (Mathlib), wat menselijke inspanningen kan sturen.
• Roadmap: LeanCat is het eerste deel van een serie. De auteurs plannen uitbreiding naar monoidale categorieën en hogere-categorische structuren (2-categorieën), met als doel een virtuele cyclus te creëren tussen AI-oplossingen en de uitbreiding van formele wiskundige bibliotheken.

Kortom, dit paper stelt dat het overbruggen van de "abstraction gap" in formeel bewijzen niet zal gebeuren door simpelweg grotere modellen te trainen, maar door systemen te ontwikkelen die dynamisch kunnen navigeren in grote kennisbanken en complexe abstracties kunnen samenstellen.