IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch

Dit paper introduceert IndiMathBench, een door mensen geverifieerd benchmark voor het evalueren van wiskundig redeneren in Lean 4, dat is samengesteld uit 312 problemen van Indiase wiskunde-olympiades via een AI-gestuurde, menselijk ondersteunde pipeline en aantoont dat geautomatiseerde formalisatie ondanks iteratieve verfijning nog steeds aanzienlijke uitdagingen kent.

De kern

🧱 De Bouwmeesters van de Wiskundige Wereld: Een Verhaal over IndiMathBench

Stel je voor dat wiskunde een enorme, ingewikkelde stad is. In deze stad wonen twee soorten mensen:

1. De Mensen: Ze praten over de stad in gewone taal, met zinnen als "Kijk, dat gebouw is recht" of "Die brug is te kort". Ze noemen dit informele wiskunde.
2. De Robots (De Theorema-Bewijzers): Deze robots kunnen alleen werken met een heel streng, digitaal taalgebruik. Als je een foutje maakt in een komma of een getal, stopt de robot en zegt hij: "Ik snap het niet." Dit noemen we formele wiskunde (in dit geval in een taal genaamd Lean).

Het probleem is dat we heel graag willen dat de robots de stad van de mensen begrijpen en kunnen bouwen. Maar tot nu toe is dat erg lastig.

🚧 Het Grote Probleem: Te weinig blauwdrukken

Om robots te leren bouwen, hebben we "blauwdrukken" nodig: paren van een menselijke zin en de perfecte robot-versie daarvan.

• Het probleem: Er zijn maar heel weinig van deze blauwdrukken beschikbaar.
• De oorzaak: Mensen die zowel wiskunde als robot-programmeren kunnen, zijn zeldzaam. Het kost jaren om één perfecte blauwdruk te maken.
• Het gevolg: De robots (zoals de slimste AI's van vandaag) oefenen maar op een paar honderd oude blauwdrukken. Ze hebben die al uit hun hoofd geleerd (ze "kijken in de cheat sheet" van het internet) en weten niet echt hoe ze moeten redeneren.

🇮🇳 De Oplossing: IndiMathBench

De auteurs van dit paper hebben een nieuwe, enorme verzameling blauwdrukken gemaakt, genaamd INDIMATHBENCH.

• De Bron: Ze hebben 312 moeilijke wiskundeproblemen genomen uit de Indiase Wiskunde Olympiade. Dit zijn problemen die heel anders zijn dan de standaard Amerikaanse of Europese problemen. Ze zijn vaak creatiever en vereisen slimme trucjes.
• De Mix: Ze hebben een slim systeem bedacht: Mens + AI.
  • De AI probeert eerst de menselijke zin om te zetten in robot-taal.
  • De AI krijgt direct feedback van de computer: "Fout! Je hebt een haakje vergeten."
  • De AI probeert het opnieuw.
  • Maar: Uiteindelijk kijkt een echte mens (een expert) naar het resultaat. Hij zegt: "De AI heeft de grammatica goed, maar hij heeft de betekenis van het probleem verkeerd begrepen." De mens maakt de laatste aanpassingen.

Het resultaat is een benchmark (een test) van 312 problemen die 100% betrouwbaar zijn.

🧪 De Test: Kunnen de Robots het echt?

De auteurs hebben de slimste AI's van de wereld (zoals GPT-5, Claude, en Gemini) op deze test laten werken. Het resultaat was verrassend en een beetje teleurstellend:

1. De "Grammatica" is goed, de "Betekenis" is slecht:
   Stel je voor dat je een robot vraagt om een huis te bouwen. De robot bouwt een perfect huis dat eruitziet als een huis (de code klopt), maar als je erin woont, valt het dak in omdat de muren te zwak zijn.

   • De AI's konden vaak code schrijven die compilatie (de bouwvergunning) haalde.
   • Maar als je vroeg: "Is dit huis veilig?" (is het bewijs correct?), faalden ze bijna altijd. Ze snapten de logica niet, alleen de woorden.

2. De "Geometrie" is de nachtmerrie:
   De AI's waren goed in algebra (rekenen met getallen), maar volledig vastgelopen bij meetkunde (figuren tekenen en ruimtelijk inzicht). Het was alsof je een robot vraagt om een 3D-puzzel op te lossen terwijl hij alleen in 2D kan denken.

3. De "Iteratie" (Herhalen) helpt, maar niet genoeg:
   Als je de AI 10 keer de kans geeft om het foutje te herstellen (net als een mens die een proefopgave maakt), wordt het een beetje beter. Maar zelfs dan losten ze maar ongeveer 11% van de problemen op. Dat betekent dat voor 9 van de 10 problemen de AI het niet kon.

🛠️ De Tool: Een Slim Werkblad

Om dit proces makkelijker te maken, hebben ze een speciaal VS Code-uitbreiding (een soort digitaal werkblad) gemaakt.

• Dit is als een kookplaat met een slimme assistent.
• De assistent (de AI) suggereert recepten (formules).
• De kok (de mens) ziet direct welke ingrediënten ontbreken of welke stap fout is.
• Dankzij dit systeem kon een mens een probleem in 4 minuten oplossen, terwijl het zonder hulp bijna 3 uur zou duren. Het is dus een krachtige hulpmiddel, maar de mens moet nog steeds de chef-kok zijn.

🎯 De Conclusie in Eén Zin

We hebben een nieuwe, eerlijke test (IndiMathBench) gemaakt die laat zien dat onze slimste AI's nog steeds niet echt "wiskundig kunnen denken". Ze kunnen goed nadoen hoe het eruit ziet, maar ze missen het diepe inzicht. We hebben dus nog veel menselijke hulp nodig om de brug te slaan tussen menselijke ideeën en robotische zekerheid.

Kortom: De robots zijn net leerlingen die de antwoorden uit hun hoofd hebben geleerd, maar als je ze een nieuw, lastig probleem geeft, zien ze erdoorheen. IndiMathBench is de nieuwe, eerlijke examenlijst die dat blootlegt.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "INDIMATHBENCH: AUTOFORMALIZING MATHEMATICAL REASONING PROBLEMS WITH A HUMAN TOUCH" in het Nederlands.

Probleemstelling

Het betrouwbaar automatisch formaliseren van wiskundige redeneringen (het vertalen van informele wiskunde naar machine-verifieerbare logica zoals Lean) blijft een grote uitdaging, zelfs in het tijdperk van Large Language Models (LLMs). De belangrijkste knelpunten zijn:

1. Schaarste aan hoogwaardige trainingsdata: Er is een gebrek aan grote, gepaarde datasets van informele wiskundige problemen en hun formele tegenhangers.
2. Hoge kosten voor annotatie: Het handmatig formaliseren, annoteren en verifiëren van problemen vereist diepgaande expertise in zowel wiskunde als theorem-proving, wat tijdrovend en duur is.
3. Beperkte bestaande benchmarks: Bestaande benchmarks zoals MINIF2F en PutnamBench zijn klein (rond de 1000 problemen), vertegenwoordigen voornamelijk westerse curricula, en missen vaak complexe domeinen zoals meetkunde en combinatoriek.
4. Semantische kloof: Hoewel LLMs de syntaxis van code steeds beter beheersen, blijft de semantische uitlijning met de intentie van de wiskundige stelling vaak ontoereikend. Bestaande benchmarks lijken bovendien vaak verontreinigd door data die in pre-training corpora is gebruikt.

Methodologie

De auteurs introduceren INDIMATHBENCH, een benchmark bestaande uit 312 door mensen geverifieerde Lean 4 theorema's, afgeleid van de Indiase Wiskunde Olympiade (RMO en INMO). De dataset omvat domeinen zoals meetkunde, algebra, getaltheorie en combinatoriek.

De kern van de aanpak is een mens-AI samenwerkingspipeline voor het genereren en valideren van formalisaties:

1. Categorie-gebaseerde Retrieval:

   • Problemen worden eerst gecategoriseerd (bijv. meetkunde, algebra).
   • Voor elke categorie wordt een statische context gegenereerd door een AI-agent die de Mathlib-bibliotheek verkent en relevante definities, notaties en voorbeelden extrahert. Dit voorkomt hallucinaties van niet-bestaande imports.

2. Iteratieve Refinement met Compiler Feedback:

   • LLMs genereren een eerste formalisatie gebaseerd op de natuurlijke taal en de context.
   • De output wordt gecompileerd in Lean 4. Fouten (syntax of type errors) worden geparseerd en als feedback teruggegeven aan het model.
   • Dit proces loopt maximaal zes iteraties, wat resulteert in syntactisch geldige code voor 95,3% van de problemen.

3. Multi-Model Ensemble:

   • Voor elk probleem worden 12 state-of-the-art modellen (o.a. Claude 4, GPT-5, Gemini 2.5 Pro) gebruikt om kandidaat-formalisaties te genereren.
   • Een samenvattende LLM (GPT-5) analyseert deze outputs, rangschikt ze op correctheid en identificeert gedeelde fouten of veelbelovende fragmenten.

4. Human-AI Dashboard (VS Code Extensie):

   • Experts gebruiken een interactief dashboard om de gegenereerde kandidaten te evalueren.
   • Het dashboard toont compilatie-informatie, foutmeldingen en AI-genereerde samenvattingen die experts helpen om zich te focussen op ambiguïteiten in plaats van routinecontroles.
   • Alle 312 theorema's zijn handmatig gecontroleerd en geverifieerd door twee experts om de "ground truth" te waarborgen.

Belangrijkste Bijdragen

• INDIMATHBENCH Dataset: Een nieuwe, mens-geverifieerde benchmark van 312 problemen uit de Indiase Olympiade, met een sterke focus op meetkunde en combinatoriek, domeinen die vaak ondervertegenwoordigd zijn in bestaande benchmarks.
• Scalable Formalization Pipeline: Een bewezen workflow die categorie-retrieval, iteratieve compiler-feedback en multi-model ensemble's combineert om de efficiëntie van menselijke annotatie aanzienlijk te verhogen.
• VS Code Extensie: Een open-source tool die de mens-AI samenwerking voor Lean-annotatie stroomlijnt, inclusief functies voor het samenvatten van modeloutput en het oplossen van fouten.
• Gedetailleerde Evaluatie: Een systematische analyse van de prestaties van frontier-modellen op zowel autoformalisatie als het daadwerkelijk oplossen van de theorema's.

Resultaten

De evaluatie toont aan dat autoformalisatie en theorem-proving nog steeds grote uitdagingen vormen:

• Autoformalisatie (Syntaxis vs. Semantiek):

  • Hoewel modellen zoals Claude Opus 4 en GPT-5 een hoge succesrate hebben bij het genereren van code die compileert (syntactisch correct), is de semantische correctheid (logische equivalentie met de menselijke ground truth) veel lager.
  • Bijvoorbeeld, Claude Opus 4 bereikte een compilatie-succes van 77,9%, maar slechts 21,5% semantische equivalentie (BEq-score).
  • Meetkundige problemen bleken het moeilijkst; van de 108 succesvolle BEq-formalisaties van de top-modellen kwamen er slechts 12 uit de meetkunde.

• Automated Theorem Proving (ATP):

  • In een "single-turn" setting (één poging) slaagden de modellen er nauwelijks in om een bewijs te voltooien; slechts één probleem werd opgelost door meerdere modellen (vaak gebaseerd op bestaande lemma's).
  • Met iteratieve refinements (10 rondes) met compiler-feedback steeg het succes van GPT-5 naar 11% (36/312) op INDIMATHBENCH en 4% op PutnamBench.
  • Geen enkel model slaagde erin om een enkel meetkundig probleem op te lossen, wat de enorme kloof in ruimtelijk redeneren en het gebruik van specifieke Mathlib-concepten benadrukt.

• Efficiëntie van Mens-AI Samenwerking:

  • Een gecontroleerde studie toonde aan dat de volledige systeem (met AI-samenvattingen en kandidaten) de annotatietijd per probleem reduceerde van gemiddeld 14 minuten (handmatig) naar 4 minuten. Dit is een versnelling van 3,5x ten opzichte van handmatig werken.

Betekenis en Conclusie

INDIMATHBench demonstreert dat, ondanks de snelle vooruitgang in LLM's, er nog een aanzienlijke kloof bestaat tussen het genereren van syntactisch correcte code en het begrijpen van de onderliggende wiskundige betekenis. De benchmark fungeert als een uitdagende testomgeving die aantoont dat huidige modellen moeite hebben met complexe, niet-triviale redeneringen, vooral in meetkunde.

De paper benadrukt dat mens-AI samenwerking de meest veelbelovende route is voor het creëren van hoogwaardige formele datasets. De gepresenteerde pipeline en tools bieden een schaalbare manier om de kosten van annotatie te verlagen terwijl de kwaliteit van de ground truth behouden blijft. De dataset en tools zijn open source beschikbaar gesteld om de ontwikkeling van neurale theorem-provers en autoformalisatie-systemen verder te stimuleren.