TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?

Dit paper introduceert TaoBench, een nieuw benchmark dat de beperkte generalisatie van geautomatiseerde stellingbewijzers naar niet-standaard wiskundige definities blootlegt, waarbij de prestaties van state-of-the-art modellen gemiddeld met 26% dalen wanneer ze worden getest op een zelfstandig opgebouwd raamwerk uit Terence Tao's Analysis I in plaats van op de gebruikelijke MathLib-bibliotheek.

De kern

Stel je voor dat je een superintelligente robot hebt die is getraind om wiskundeproblemen op te lossen. Deze robot is een meester geworden in het oplossen van puzzels, maar alleen als die puzzels zijn geschreven in een heel specifiek taalboek: het MathLib-handboek. Dit handboek is de "standaard" voor wiskundigen die werken met computers. De robot kan de moeilijkste opgaven uit dit boek met gemak oplossen.

Maar wat gebeurt er als je de robot een probleem geeft dat is geschreven in een ander handboek? Een handboek dat dezelfde wiskundige ideeën bevat, maar de definities, de namen van de dingen en de regels anders heeft opgeschreven?

Dat is precies wat dit onderzoek, genaamd TAOBENCH, heeft onderzocht.

De Verhaal: Twee Verschillende Dialecten

De onderzoekers hebben gekeken naar een beroemde wiskundige, Terence Tao. Hij heeft een boek geschreven over analyse (een deel van de hogere wiskunde) waarin hij de basisbegrippen, zoals getallen en verzamelingen, vanaf nul uitlegt. Hij doet dit op een heel eigen, specifieke manier, alsof hij zijn eigen dialect van wiskunde creëert.

De robot (de AI) is echter getraind op de standaardversie (MathLib). Het is alsof de robot alleen maar Engels heeft geleerd, en je hem nu een tekst geeft in een heel specifiek dialect van het Engels dat alleen in één dorp wordt gesproken.

Het Experiment: De "Tao-Test"

De onderzoekers hebben 150 wiskundige opgaven uit Tao's boek genomen. Ze hebben deze opgaven op twee manieren aan de robot voorgelegd:

1. De Tao-versie: De opgave zoals Tao die heeft geschreven (met zijn eigen definities).
2. De MathLib-versie: Dezelfde opgave, maar vertaald naar de standaardtaal die de robot kent.

Het doel was om te zien of de robot de wiskunde begrijpt, of dat hij alleen maar de woorden uit zijn training kent.

Wat Vonden Ze? (De Verbluffende Resultaten)

Het resultaat was een grote verrassing voor de wetenschap:

• In de standaardtaal (MathLib): De robot deed het fantastisch. Hij kon ongeveer 70% van de problemen oplossen. Hij was een ster.
• In de Tao-taal: Zodra ze dezelfde problemen in Tao's eigen dialect gaven, zakte de prestatie van de robot dramatisch in. Hij kon gemiddeld 26% minder problemen oplossen.

De Metafoor:
Stel je voor dat je een auto hebt die perfect rijdt op een asfaltweg (MathLib). Je vraagt de bestuurder: "Kun je ook rijden op een grindweg?" De bestuurder zegt: "Natuurlijk, het is toch ook een weg?" Maar zodra de auto op het grind komt, blijft hij steken.

Het probleem is niet dat de grindweg (de wiskunde) moeilijker is. Het probleem is dat de auto (de AI) niet weet hoe hij moet omgaan met de andere ondergrond. Hij is te gespecialiseerd op de asfaltweg. Hij heeft niet geleerd om wiskunde te doen, maar alleen om MathLib-wiskunde te doen.

Waarom is dit belangrijk?

In de echte wereld van wiskundig onderzoek zijn mensen vaak aan het experimenteren. Ze bouwen nieuwe concepten op en gebruiken definities die nog niet in de grote standaardboeken staan. Ze werken in "proeflaboratoria" met hun eigen regels.

Deze studie laat zien dat de huidige slimste AI's niet flexibel genoeg zijn voor die echte, exploratieve wetenschap. Ze zijn als een student die alleen maar uit het hoofd heeft geleerd hoe je een som oplost in het standaardboek, maar als je de som een beetje anders formuleert, raakt hij in paniek.

De Oplossing: TAOBENCH

De onderzoekers hebben een nieuwe testomgeving gecreëerd, TAOBENCH. Dit is als een "fitnesscentrum" voor AI's, maar dan speciaal ontworpen om te testen of ze kunnen omgaan met nieuwe, onbekende regels.

Ze hebben ook een slimme manier bedacht om automatisch de benodigde "context" (de uitleg van de regels) bij elke opgave te verzamelen, zodat de AI niet in de war raakt door te veel of te weinig informatie.

Conclusie in Eenvoudige Woorden

De boodschap van dit papier is simpel: Onze slimme wiskundige AI's zijn momenteel te star. Ze zijn goed in het herhalen van wat ze hebben geleerd, maar slecht in het aanpassen aan nieuwe manieren van denken.

Als we AI's echt willen gebruiken om de grenzen van de wiskunde te verleggen (zoals echte onderzoekers doen), moeten we ze niet alleen trainen op de standaardboeken, maar ze ook leren om te denken in nieuwe, creatieve dialecten. TAOBENCH is de eerste stap om dat te testen en te verbeteren.

Technische samenvatting

1. Probleemstelling

Automatische stellingbewijzers (ATP) gebaseerd op Large Language Models (LLMs) hebben recente successen geboekt op benchmarks zoals MiniF2F en PutnamBench. Echter, deze benchmarks en de bijbehorende trainingsdata zijn bijna uitsluitend gebaseerd op MathLib, de de facto standaardbibliotheek voor Lean 4.

Het paper stelt dat wiskundig onderzoek vaak exploratief is en afhankelijk van op maat gemaakte definities en constructies die afwijken van standaardbibliotheken. Er bestaat een "distributieverandering" (distribution shift) tussen de definitiesystemen waarop modellen worden getraind (MathLib) en de systemen waarin ze in de praktijk moeten worden toegepast (nieuwe, onderzoeksgerichte formalisaties). De centrale vraag is: Generaliseren ATP-modellen effectief naar nieuwe definitiesystemen, of zijn ze slechts overgefit op de MathLib-structuur?

2. Methodologie: TAOBENCH

Om dit te testen, introduceren de auteurs TAOBENCH, een benchmark gebaseerd op 150 oefeningen uit Terence Tao's Analysis I, die volledig in Lean is geformaliseerd.

A. De Definitiesystemen

TAOBENCH vergelijkt twee versies van dezelfde wiskundige problemen:

1. TAOBENCH (Tao's Framework): Problemen geformaliseerd volgens Tao's eigen aanpak. Hierbij worden kernconcepten (zoals natuurlijke getallen, verzamelingen, reële getallen) van scratch opgebouwd met aangepaste inductieve types, notaties en namespaces. Dit weerspiegelt een "onbekend" definitiesysteem voor modellen die op MathLib zijn getraind.
2. TAOBENCHMATHLIB: Een wiskundig equivalente vertaling van dezelfde problemen naar het standaard MathLib-definitiesysteem. Dit dient als controlegroep om de wiskundige moeilijkheid te isoleren van de moeilijkheid van het definitiesysteem.

B. Agente Data-Constructie Pipeline

Een grote technische uitdaging was het creëren van zelfstandige, compileerbare Lean-bestanden voor elk probleem zonder externe afhankelijkheden. De auteurs ontwikkelden een agente pipeline met de volgende stappen:

• Context Extractie: Gebruikmakend van het statische analyse-tool JiXia en een file-lookup tool, identificeert een agent (GPT-5) de minimale set van definities, lemmata en notaties die nodig zijn om een specifieke oefening te compileren.
• Iteratieve Compilatie: De agent bouwt een lokaal Lean-omgeving en gebruikt een compilatie-tool om fouten te detecteren en op te lossen totdat de code compileert. Dit voorkomt dat het model hallucinaties introduceert of de intentie van het probleem verandert.
• Vertaling en Validatie: Voor TAOBENCHMATHLIB wordt een tweetrapsproces gebruikt:
  1. Rewriting: Een model herschrijft de Tao-variant naar MathLib-syntax, met web-search voor toegang tot MathLib-documentatie.
  2. Equivalence Checking: Een tweede stap controleert of de doelstellingen (proof states) van de Tao- en MathLib-versies wiskundig equivalent zijn.
  3. Expert Verificatie: Menselijke experts (met ervaring in Lean en analyse) verifiëren de equivalentie en corrigeren subtiele fouten.

3. Belangrijkste Bijdragen

1. TAOBENCH: De eerste benchmark die specifiek is ontworpen om de robuustheid van ATP-modellen te testen buiten het MathLib-ecosysteem, met een focus op generalisatie naar nieuwe definitiesystemen.
2. TAOBENCHMATHLIB: Een gepaarde dataset van wiskundig equivalente problemen in MathLib-syntax, waarmee de impact van het definitiesysteem kan worden geïsoleerd.
3. Agente Pipelines: Een reproduceerbaar framework voor het automatisch extraheren van zelfstandige, compileerbare contexten uit grote formele projecten en het genereren van equivalente vertalingen.

4. Resultaten

De auteurs hebben vier state-of-the-art ATP-modellen geëvalueerd (DeepSeek-Prover-V2, Goedel-Prover-V2, Kimina-Prover) en frontier foundation modellen (GPT-5.1, Gemini 3 Pro).

• Prestatiedaling: Hoewel modellen goed presteren op TAOBENCHMATHLIB (vaak >65% tot >70% pass rate), daalt de prestatie op TAOBENCH (Tao's framework) gemiddeld met ongeveer 26%.
  • Voorbeeld: Goedel-Prover-V2-32B scoort 72,67% op MathLib, maar slechts 49,33% op Tao's framework.
• Invloed van Contextlengte: De prestatiekloof wordt groter naarmate het aantal lokale definities in de context toeneemt.
  • Bij $n=0$ (geen extra lokale definities) is er nauwelijks verschil.
  • Bij $n \ge 10$ lokale definities daalt de pass rate op TAOBENCH naar slechts 6,37%, terwijl deze op TAOBENCHMATHLIB stabiel blijft rond 53%.
• Frontier Modellen: Algemene foundation modellen (zoals GPT-5.1) presteren beter op de Tao-variant dan gespecialiseerde ATP-modellen, wat suggereert dat hun vermogen om contextuele voorbeelden te gebruiken (in-context learning) cruciaal is, maar dat gespecialiseerde ATP-modellen te afhankelijk zijn van hun trainingsdistributie (MathLib).
• Case Studies:
  • Nat.backwards_induction: Modellen falen volledig op de Tao-variant (0%) omdat ze de op maat gemaakte inductieve structuur en orde-relaties niet kunnen integreren, terwijl ze de MathLib-versie (64%) succesvol oplossen met standaard lemmata.
  • Convergesto.squeeze: Hier toont een model juist betere prestaties op de Tao-variant (die een expliciete $\epsilon$-$\delta$ definitie gebruikt) dan op de MathLib-variant (die abstracte filters gebruikt), wat aantoont dat de richting van de prestatiedaling afhankelijk is van de specifieke definitie-afwijking.

5. Betekenis en Conclusie

Het paper concludeert dat de huidige staat van de kunst (SOTA) ATP-modellen geen robuuste generalisatie vertonen naar nieuwe definitiesystemen, zelfs niet wanneer de onderliggende wiskunde identiek is.

• De Bottleneck: Het probleem ligt niet in de wiskundige moeilijkheid, maar in de generalisatie over definitiesystemen. Modellen zijn getraind om te redeneren binnen de specifieke "dialect" van MathLib en falen wanneer ze geconfronteerd worden met een ander, maar wiskundig equivalent, formalisme.
• Implicatie voor Onderzoek: Bestaande benchmarks (zoals MiniF2F) meten meer de bekwaamheid om een specifiek formalisme te gebruiken dan de algemene wiskundige redeneerkracht. Dit vormt een grote barrière voor het toepassen van ATP's in echt wetenschappelijk onderzoek, waar nieuwe definities vaak noodzakelijk zijn.
• Toekomst: TAOBENCH biedt een concrete testomgeving om toekomstige modellen te trainen en evalueren op hun vermogen om zich aan te passen aan diverse formele ecosystemen, wat essentieel is voor de integratie van AI in de voortbrenging van nieuwe wiskunde.