💻 computer science

MathAtlas: A Benchmark for Autoformalization in the Wild

Dit artikel introduceert MathAtlas, de eerste grootschalige benchmark voor autoformalisatie die ongeveer 52.000 wiskundige concepten op doctoraatsniveau uit 103 leerboeken omvat, en die de extreme moeilijkheid blootlegt van huidige modellen bij het verwerken van complexe, afhankelijkheidsrijke onderzoekswiskunde.

Oorspronkelijke auteurs: Nilay Patel, Noah Arias, Davit Babayan, Victoria Cochran, Timothy Libman, Hafsah Mahmood, Liam McCarty, Soli Munoz, Laurel Willey, Jeffrey Flanigan

Gepubliceerd 2026-05-15

📖 4 min leestijd☕ Koffiepauze-leesvoer

CC BY 4.0

Oorspronkelijke auteurs: Nilay Patel, Noah Arias, Davit Babayan, Victoria Cochran, Timothy Libman, Hafsah Mahmood, Liam McCarty, Soli Munoz, Laurel Willey, Jeffrey Flanigan

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een briljante vertaler hebt die menselijke verhalen kan omzetten in een strikte, door computers leesbare taal genaamd "Lean". Lang is deze vertaler alleen getest op simpele verhalen – zoals middelbare school wiskundeproblemen of basispuzzels. De computer kon deze gemakkelijk vertalen omdat de regels eenvoudig waren en de computer dergelijke regels al eerder had gezien.

Maar wat gebeurt er als je deze vertaler vraagt om een complex, op doctoraatniveau geschreven onderzoeksartikel te vertalen? Dat is het probleem dat MathAtlas aanpakt.

Hier is een eenvoudige uiteenzetting van wat het artikel doet, met behulp van alledaagse analogieën:

1. Het Probleem: De "Bibliotheek" is Te Groot

Stel je voor dat je een huis (een formeel bewijs) probeert te bouwen op basis van een blauwdruk (een wiskundeleerboek).

Oude Benchmarks: Eerdere tests vroegen de vertaler alleen om een klein schuurtje te bouwen. Het materiaal lag allemaal in de gereedschapskist en de instructies waren kort.
De Realiteit: Gevorderde wiskunde is als het bouwen van een wolkenkrabber. Om de bovenste verdieping te bouwen, heb je de 50e verdieping nodig. Om de 50e verdieping te bouwen, heb je de 49e nodig, en zo verder, helemaal tot aan de fundering.
Het Probleem: In geavanceerde wiskunde is de "fundering" (definities en theorieën) vaak nog niet in de taal van de computer gebouwd. Als de vertaler de definitie van een "Lie-algebra" (een complex concept) niet kent, kan hij de stelling die het gebruikt niet vertalen.

2. De Oplossing: MathAtlas (De "Wilde" Kaart)

De auteurs hebben MathAtlas gecreëerd, een enorme nieuwe testset.

De Schaal: Ze hebben 103 wiskundige leerboeken op doctoraatniveau gescrapt. Het is alsof je een bibliotheek van 52.000 pagina's geavanceerde wiskunde hebt genomen en dit hebt omgezet in een digitale kaart.
Het "Afhankelijkheidsgrafiek": Dit is de superkracht van het artikel. Stel je een "Kies je Eigen Avontuur"-boek voor waarbij elke pagina pijlen heeft die verwijzen naar andere pagina's die je eerst moet lezen. MathAtlas tekent deze pijlen. Het toont dat je om Propositie 15 te begrijpen, eerst Dedekindringen moet begrijpen, die op hun beurt * priemidealen* nodig hebben.
Waarom dit belangrijk is: Het dwingt de AI niet alleen om één zin te vertalen, maar om uit te zoeken: "Heb ik de tools om dit te bouwen? Zo niet, kan ik dan eerst de tools vinden of bouwen?"

3. De Resultaten: De AI zit in de Modder

De auteurs hebben de slimste beschikbare AI-modellen getest op MathAtlas, en de resultaten waren vernederend.

De Score: Zelfs de beste AI haalde minder dan 10% van de stellingen correct. Voor definities was dit ongeveer 16%.
De "Diepte"-Valstrik: Hoe dieper de "afhankelijkheidsboom" (hoe meer stappen je terug moet om de definities te vinden), hoe slechter de AI presteerde.
- Analogie: Als de AI 10 eerdere concepten moet opzoeken om één zin te vertalen, raakt hij in de war en geeft het op. Bij de moeilijkste problemen (waar de afhankelijkheidsboom het diepst was), haalde de AI slechts 2,6% correct.
Het "Mathlib"-Effect: De AI deed het iets beter wanneer het concept dat hij moest vertalen al in een beroemde bibliotheek genaamd "Mathlib" zat (wat een soort vooraf gebouwd gereedschapskist is die de AI waarschijnlijk heeft bestudeerd). Als het concept nieuw was en niet in die bibliotheek zat, had de AI veel meer moeite.

4. De "Vertrouwen"-test (MA-Align)

Het artikel creëerde ook een nieuwe test genaamd MA-Align.

Het Probleem: Soms vertaalt een AI een zin in code die er perfect uitziet en zonder fouten draait, maar betekent het eigenlijk iets heel anders dan de oorspronkelijke wiskunde. Het is als "De kat zat op de mat" vertalen naar een computerprogramma dat zegt "De hond at de pizza". Het programma werkt, maar het is fout.
De Test: Ze vroegen AI-rechters om te controleren of de vertaling "trouw" was (waarheidsgetrouw aan de betekenis). Ze ontdekten dat zelfs de beste AI-rechters vaak werden misleid, vooral bij complexe definities op doctoraatniveau.

De Conclusie

Het artikel concludeert dat AI, hoewel het goed wordt in simpele wiskunde, momenteel vreselijk is in het vertalen van complexe, real-world wiskunde op doctoraatniveau. De belangrijkste bottleneck is niet alleen het vertalen van woorden; het is het begrijpen van het enorme web van verbindingen tussen ideeën en het weten hoe je de nodige "tools" (definities) bouwt voordat je het "huis" (stellingen) bouwt.

MathAtlas staat nu open voor iedereen om te gebruiken als een uitdaging om AI te helpen leren hoe het deze diepe, complexe afhankelijkheden moet hanteren.

Technische Samenvatting: MathAtlas: Een Benchmark voor Autoformalisatie in het Wild

Probleemstelling

Huidige benchmarks voor autoformalisatie richten zich voornamelijk op eenvoudigere domeinen, zoals olympiade- of universitaire wiskunde, waar het voorafgaande materiaal beperkt is en vaak al is geformaliseerd in bibliotheken zoals Mathlib. Echter, wiskunde op graduate-niveau en onderzoekswiskunde blijven onderbelicht. In deze geavanceerde domeinen is autoformalisatie aanzienlijk complexer omdat:

Diepte van Voorvereisten: Geavanceerde wiskunde is afhankelijk van uitgebreide theoretische voorvereisten, waarvan een groot deel nog niet is geformaliseerd. Een effectief systeem moet niet alleen de doelstelling formaliseren, maar ook de benodigde afhankelijke theorieën ophalen of synthetiseren.
Definitiegat: Bestaande benchmarks negeren grotendeels de formalisatie van wiskundige definities. Systemen die alleen stellingen kunnen verwerken, worden beperkt door de bestaande formele theorie; ze kunnen stellingen niet formaliseren die concepten bevatten waarvoor geen definities bestaan.
Gebrek aan Real-world Data: Er is een schaarste aan grootschalige, real-world benchmarks die de "in het wild"-complexiteit van wiskunde op graduate-niveau vastleggen, inclusief rijke contextuele afhankelijkheden en relaties tussen entiteiten.

Methodologie

Datasetconstructie: MathAtlas

De auteurs introduceren MathAtlas, de eerste grootschalige benchmark voor autoformalisatie van wiskunde op graduate-niveau.

Bronmateriaal: De dataset is ontleend aan 103 wiskundige handboeken op graduate-niveau die 87 verschillende vakgebieden bestrijken (bijvoorbeeld reële analyse, differentiaalmeetkunde, categorietheorie, kwantumgroepen).
Schaal en Samenstelling: MathAtlas bevat ongeveer 52.052 entiteiten, bestaande uit:
- ~18.000 stellingen
- ~10.000 oefeningen
- ~10.000 definities
- ~10.000 bewijzen
- ~5.000 voorbeelden
Afhankelijkheidsgrafiek: Een kernkenmerk is de verrijking van de dataset met een wiskundige afhankelijkheidsgrafiek met ongeveer 178.000 relaties. Deze grafiek koppelt entiteiten aan:
- Objectreferenties: Genoemde wiskundige concepten (bijvoorbeeld "Dedekind-ring") die externe definities vereisen.
- Entiteitsreferenties: Referenties naar andere specifieke stellingen of definities binnen de tekst.
- Lokale Variabele Referenties: Symbolen die worden gebruikt zonder expliciete lokale introductie.
- Afhankelijkheidsdiepte: De maximale hoogte van de afhankelijkheidsboom van een entiteit (gemiddelde diepte van 30, variërend tot 80), wat aanzienlijk verschilt per vakgebied (bijvoorbeeld hebben Lie-algebra's diepere bomen dan de verzamelingenleer).

Constructiepiplijn:

Conversie: PDF's worden omgezet naar Mathematical Markdown (MMD) met behulp van Nougat.
Extractie: Een few-shot geprompte LLM (gpt-oss-120b) extraheert entiteiten (definities, stellingen, etc.) en hun identificatoren.
Referentie-extractie: Een tweede model identificeert object-, entiteits- en lokale variabele-referenties binnen de geëxtraheerde tekst.
Relatie-extractie: Een systeem koppelt referenties aan doelentiteiten (met behulp van LeanSearch voor Mathlib-gronding en LLM's voor interne matching) om de afhankelijkheidsgrafiek te construeren.
Kwaliteitscontrole: Menselijke evaluatie op willekeurige steekproeven geeft 90,4% validiteit voor entiteitsextractie en een F1-score van 94,8% voor relatie-extractie.

Evaluatiemetrics

Het artikel evalueert de prestaties van autoformalisatie met behulp van een samengestelde metric genaamd Correctheid, die vereist dat een formalisatie aan twee voorwaarden voldoet:

Compilatie: De gegenereerde Lean 4-code moet succesvol compileren.
Semantische Trouw: De formele stelling moet semantisch equivalent zijn aan de informele bron.
- Om trouw te meten, introduceren de auteurs MA-Align, een binaire classificatiebenchmark van 200 entiteiten (stellingen en definities) uit MathAtlas, die zijn geannoteerd als "uitgelijnd" of "niet-uitgelijnd".
- Ze evalueren bestaande "LLM-as-judge"-systemen (zoals CriticLean) en constateren dat hoewel ze goed presteren op eerdere benchmarks (ConsistencyCheck, CriticLeanBench), hun nauwkeurigheid aanzienlijk daalt op MA-Align, wat een kloof in de evaluatie van definities op graduate-niveau benadrukt.

Experimentele Opstelling

De auteurs testten diverse baselines op MathAtlas, waaronder:

Geprompte Modellen: Zero-shot en few-shot prompting met gpt-oss-20b en gpt-oss-120b.
Fine-tuned Modellen: Herald, Kimina, ATLAS-L, Goedel en ReForm.
Ablatiestudies: Het testen van de impact van lokale context (de vorige 500 tokens), ontworpen prompts en specifieke trainingsvoorbeelden.
MA-Hard Subset: Een specifiek subset van ongeveer 700 entiteiten met de diepste afhankelijkheidsbomen (gemiddelde diepte >50) om de grenzen van huidige systemen te testen.

Belangrijkste Resultaten

Algemene Prestaties

MathAtlas blijkt een uiterst uitdagende benchmark te zijn. Sterke baselines bereiken lage correctheidspercentages:

Stellingen (Stellingen, Voorbeelden, Oefeningen): De beste baseline (ReForm 8B) bereikt slechts 9,8% correctheid.
Definities: De beste baseline (gpt-oss-120b met few-shot prompting) bereikt 16,7% correctheid.
Dispariteit: Er is een aanzienlijke kloof tussen compilatiepercentages en correctheid (bijvoorbeeld compiles Kimina 7B 27,3% van de stellingen, maar slechts 2,3% is trouw), wat aangeeft dat syntactisch succes geen semantische nauwkeurigheid garandeert.

Afhankelijkheidsdiepte en Moeilijkheidsgraad

De prestaties verslechteren aanzienlijk naarmate de afhankelijkheidsdiepte toeneemt:

Op MA-Hard (de 700 entiteiten met de diepste afhankelijkheidsbomen) bereikt het beste model slechts 2,6% correctheid.
Statistische analyse (Kolmogorov-Smirnov-test) bevestigt een significant verschil in correctheidsverdelingen tussen ondiepe en diepe afhankelijkheidsbomen ( $p < 0,001$ ).

Context en Gronding

Lokale Context: Het toevoegen van lokale context (de vorige 500 tokens) aan de prompt verlaagde de prestaties voor geprompte modellen (dalend van 20,3% naar 17,4% voor definities), wat suggereert dat huidige modellen moeite hebben om langeafstandscontext effectief te integreren.
Mathlib Gronding: Entiteiten die konden worden gegrond op bestaande formalisaties in Mathlib, hadden een aanzienlijk grotere kans om correct te worden geformaliseerd (27,9% versus 16,8% voor niet-gegronde definities), wat suggereert dat LLM's profiteren van eerdere blootstelling aan geformaliseerde theorie in hun trainingsdata.

Betekenis en Bijdragen

Het artikel claimt de volgende betekenis voor het vakgebied:

Eerste Benchmark op Graduate-niveau: MathAtlas is de eerste grootschalige, "in het wild"-benchmark voor wiskunde op graduate-niveau, die voorbij de beperkingen van olympiade- en universitaire datasets gaat.
Afhankelijkheidsbewuste Evaluatie: Het is de eerste benchmark die rijke afhankelijkheidsgrafieken en relaties tussen entiteiten omvat, waardoor systemen kunnen worden geëvalueerd die voorafgaande theorie en definitie-synthese moeten verwerken.
Benadrukking van het Definitiegat: De resultaten tonen aan dat huidige state-of-the-art-modellen aanzienlijk moeite hebben met definities en diepe afhankelijkheidsketens, wat een kritieke knelpunt blootlegt bij het schalen van autoformalisatie naar geavanceerde wiskunde.
Beperkingen van Trouw-metrics: De introductie van MA-Align en de daaropvolgende experimenten tonen aan dat bestaande semantische trouw-metrics (zoals CriticLean) zich niet goed generaliseren naar definities op graduate-niveau, wat nieuwe evaluatiebenaderingen noodzakelijk maakt.
Communityhulpbron: De auteurs publiceren MathAtlas, MA-Align en de experimentele code om toekomstig onderzoek naar afhankelijkheidsbewuste autoformalisatie en de formalisatie van geavanceerde wiskundige concepten te faciliteren.

De auteurs concluderen dat hoewel huidige systemen veelbelovend zijn, de kloof tussen bestaande capaciteiten en de eisen van wiskunde op graduate-niveau enorm blijft, met name wat betreft de synthese van voorafgaande theorie en de formalisatie van definities.