Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models

Deze paper introduceert OlymMATH, een uitdagend benchmark voor wiskundige redenering op Olympiade-niveau dat 350 problemen bevat met zowel natuurlijke taal- als formele Lean 4-verificatie, en dat de beperkingen van huidige grote taalmodellen blootlegt door middel van uitgebreide evaluaties en openbaarmaking van een groot aantal redeneertrajecten.

De kern

Stel je voor dat je een groep slimme robots (deze noemen we "Grote Taalmodellen" of AI's) wilt testen op hun wiskundekunsten. Tot nu toe waren de toetsen die we hen gaven, een beetje als een schoolproefwerk voor de middelbare school. De robots hebben die zo goed gemaakt dat ze bijna perfect scoren. Het is alsof je een schaakgrootmeester blijft uitdagen met een simpel schaakpuzzeltje uit een krant; het zegt je niets meer over hoe slim hij écht is.

De auteurs van dit paper, onderzoekers van de Renmin Universiteit in China, zeggen: "Tijd voor een echte uitdaging!" Ze hebben OlymMATH bedacht.

Hier is wat OlymMATH is, vertaald naar alledaags taal:

1. De "Olympische" Wiskundetoets

Stel je voor dat je in plaats van een gewone schooltoets, de robots moet laten deelnemen aan de Wiskundige Olympiade. Dit zijn de allerzwaarste, meest creatieve en lastigste problemen die je je kunt voorstellen.

• De inhoud: Ze hebben 350 van deze super-moeilijke problemen verzameld.
• Twee talen: Om eerlijk te zijn, hebben ze elk probleem in het Engels én het Chinees geschreven. Zo kunnen ze zien of de robots beter zijn in het ene taal dan het andere (net als een mens die misschien beter kan rekenen in zijn moedertaal dan in een vreemde taal).
• Geen "cheaten": Ze hebben deze problemen niet van internet gehaald (want dan zouden de robots ze misschien al kennen). Ze hebben ze handmatig uit oude, gedrukte boeken en tijdschriften gehaald. Het is alsof je een nieuwe, geheime toets maakt die niemand eerder heeft gezien.

2. Twee manieren om te controleren: Het Antwoordenboekje vs. De Bouwtekening

Dit is het slimste deel van hun idee. Normaal gesproken kijken we alleen of het antwoord klopt. Maar wat als de robot het juiste antwoord raadt, maar de weg ernaartoe volledig verkeerd is?

OlymMATH gebruikt twee verschillende methoden om dit te checken:

• De "Antwoorden-Check" (OlymMATH-EASY & HARD):
  Hierbij krijgt de robot een vraag en moet hij een getal als antwoord geven. Een computer kijkt dan simpelweg: "Klopt dit getal?"

  • Analogie: Dit is alsof je een puzzel oplost en alleen kijkt of het laatste stukje in de juiste gleuf past.

• De "Bouwtekening-Check" (OlymMATH-LEAN):
  Dit is het echte hoogtepunt. Hierbij moet de robot niet alleen het antwoord geven, maar zijn hele redenering schrijven in een speciale programmeertaal genaamd Lean. Lean is als een zeer strenge architect die elke stap van de bouw controleert.

  • Analogie: Stel je voor dat de robot een brug moet bouwen. Bij de eerste methode kijken we alleen of de brug staat. Bij deze tweede methode moet de robot de bouwtekeningen inleveren. Als er één boutje in de tekening niet logisch is, of als de brug op papier instort, dan faalt de robot, zelfs als hij het juiste antwoord had geraden.
  • Dit voorkomt dat robots "gokken" of slimme trucs gebruiken om het antwoord te raden zonder het echt te begrijpen.

3. Wat hebben ze ontdekt?

Toen ze de slimste robots ter wereld (zoals DeepSeek, Gemini en OpenAI's modellen) deze toets lieten doen, gebeurde er een paar interessante dingen:

• Ze zijn nog niet zo slim als we dachten: Zelfs de allerbeste robots haalden op de moeilijkste vragen (de "HARD" versie) vaak minder dan 60% goed. Dat is alsof een student die dacht dat hij een A+ verdiende, een 4 haalt. Het bewijst dat wiskundig redeneren nog steeds heel moeilijk is voor AI.
• Taal maakt uit: De robots deden het over het algemeen beter in het Engels dan in het Chinees. Het lijkt erop dat ze meer "oefening" hebben gehad in het Engels, net zoals een mens die meer boeken in het Engels heeft gelezen.
• De "Gok-Strategie": De onderzoekers zagen dat robots soms probeerden het antwoord te raden door te zeggen: "Het is waarschijnlijk symmetrisch, dus het antwoord moet X zijn." Ze deden alsof ze wisten wat ze deden, maar in werkelijkheid gokten ze. De "Bouwtekening-Check" (Lean) pakte deze trucs direct op en liet zien dat de brug eigenlijk instortte.

Waarom is dit belangrijk?

Voorheen konden we niet goed zien of een AI echt redeneert of dat hij gewoon slimme patronen heeft geleerd om het juiste antwoord te gissen. OlymMATH is als een onvervalst, onmogelijk te hacken examen.

Het dwingt de robots om hun werk te laten zien, stap voor stap, zonder ruimte voor trucs. Dit helpt onderzoekers om betere robots te bouwen die echt begrijpen waarom iets waar is, en niet alleen wat het antwoord is.

Kortom: De onderzoekers hebben een nieuwe, onmogelijke wiskundetoets gemaakt in twee talen, met een speciale controlekamer die elke stap van het denkproces checkt, om te zien welke AI's écht slim zijn en welke alleen maar doen alsof.

Technische samenvatting

Titel: Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models

Auteurs: Haoxiang Sun, Yingqian Min, Zhipeng Chen, Wayne Xin Zhao, Ji-Rong Wen (Renmin University of China)

---

1. Het Probleem

De snelle vooruitgang van grote redeneringsmodellen (Large Reasoning Models) heeft bestaande wiskundige benchmarks (zoals GSM8K en MATH) verzadigd. Moderne modellen presteren hier vaak al zeer goed, waardoor er een dringende behoefte is aan uitdagendere evaluatiekaders. Bestaande benchmarks lijden echter onder verschillende tekortkomingen:

• Data-verontreiniging: Veel benchmarks halen problemen van het internet (bijv. AoPS, IMO-lijsten), wat het risico op "data leakage" vergroot (modellen hebben de antwoorden al gezien tijdens training).
• Beperkte verificatie: Numerieke benchmarks gebruiken vaak regelgebaseerde verificatie (alleen het eindantwoord telt), wat geen inzicht geeft in de kwaliteit van het redeneringsproces. Formele bewijsbenchmarks (zoals Lean) zijn vaak enkel in het Engels en komen uit bekende competities, wat ook het verontreinigingsrisico verhoogt.
• Taalbias: De meeste benchmarks zijn Engelstalig, waardoor meertalige redeneercapaciteiten onvoldoende worden onderzocht.
• Heuristiek vs. Redenering: Modellen gebruiken soms "gokken" of heuristische kortkoppelingen om het juiste antwoord te krijgen zonder een rigoureus bewijs, wat door standaard benchmarks onopgemerkt blijft.

2. Methodologie: OlymMATH

Om deze gaten te dichten, stellen de auteurs OlymMATH voor: een zorgvuldig samengesteld, tweetalig (Engels en Chinees) benchmark voor Olympiade-niveau wiskunde.

Opbouw van de Dataset:
De dataset bevat 350 unieke problemen, verdeeld over drie niet-overlappende subsets:

1. OlymMATH-EASY & OlymMATH-HARD:
   • Bevat elk 100 computationele problemen (totaal 200).
   • Vereist precieze numerieke antwoorden.
   • Beschikbaar in zowel Engels als Chinees.
   • Verificatie: Rule-based verificatie via sympy (Python-bibliotheek) voor objectieve beoordeling van het eindantwoord.
   • Bron: Handmatig geselecteerd uit gedrukte publicaties (tijdschriften en leerboeken) om data-verontreiniging te minimaliseren.
2. OlymMATH-LEAN:
   • Bevat 150 problemen die zijn geformaliseerd in Lean 4.
   • Biedt naast de formele code ook tweetalige natuurlijke taal statements en oplossingen.
   • Verificatie: Volledig geautomatiseerde, wiskundig rigoureuze verificatie via de Lean-server. Dit eist een stap-voor-stap bewijs in plaats van alleen een eindantwoord.

Kwaliteitsborging:

• Contaminatie-analyse: De auteurs gebruiken een n-gram-meting om te bewijzen dat OlymMATH een lager risico op data-leakage heeft dan benchmarks die online worden gescraped (zoals PolyMath).
• Expertvalidatie: Problemen en oplossingen zijn gecontroleerd door experts, waaronder een zilveren medaillewinnaar van de Chinese Wiskunde Olympiade.
• Categorieën: De problemen dekken vier hoofdvelden: Algebra, Meetkunde, Getaltheorie en Combinatoriek. Meetkundige problemen zijn tekstueel herschreven om compatibel te zijn met LLM's.

3. Belangrijkste Bijdragen

• Unificatie van Paradigma's: OlymMATH is de eerste benchmark die natuurlijke taal-evaluatie (eindantwoord) en formeel theorem-proving (procesverificatie) binnen één tweetalige suite combineert.
• Tweetalige Evaluatie: Het biedt parallelle versies in het Engels en Chinees, wat unieke inzichten geeft in taalgebonden redeneerprestaties.
• Openbare Resources: De auteurs hebben 582.400 redeneertrajecten (van 28 modellen), een visualisatietool en expert-oplossingen open-source gemaakt om gemeenschapsonderzoek te faciliteren.
• Detectie van "Gokken": Door de combinatie van formele verificatie en natuurlijke taalanalyse kunnen ze gevallen identificeren waar modellen heuristische gokken gebruiken in plaats van logisch redeneren.

4. Resultaten en Analyse

Uitgebreide experimenten met state-of-the-art modellen (zoals DeepSeek-R1, o3-mini, Gemini 2.5 Pro) tonen aan:

• Uitdagendheid: OlymMATH-HARD is significant moeilijker dan bestaande benchmarks. Zelfs de beste modellen (Gemini 2.5 Pro) behalen slechts 58,4% nauwkeurigheid op de Engelse HARD-versie, terwijl hun prestaties op AIME 2024 boven de 90% liggen.
• Taalverschillen: Er is een consistente prestatiekloof tussen Engels en Chinees; modellen presteren over het algemeen beter op Engelse problemen. Dit wordt statistisch significant geacht en suggereert dat Engels nog steeds domineert in pre-training datasets.
• Inconsistentie: Modellen kunnen vaak het juiste antwoord vinden bij veelvuldige pogingen (Pass@64), maar missen consistentie (Cons@64). Bijvoorbeeld, op de HARD-set steeg de prestatie van een 7B-model van 11,1% (Pass@1) naar 74,0% (Pass@64), maar de consensus was slechts 22,0%.
• Heuristische Gokken: Case studies tonen aan dat modellen soms aannames doen (bijv. symmetrie) zonder deze te bewijzen. In OlymMATH-LEAN falen deze "gokken" omdat ze niet compileren in Lean, wat aantoont dat formele verificatie essentieel is om echte redeneercapaciteit te meten.
• Vergelijking: OlymMATH-HARD onderscheidt zich beter tussen de beste modellen dan AIME of OlympiadBench, wat het een superieur instrument maakt voor het evalueren van de grenzen van AI.

5. Betekenis en Toekomstperspectief

OlymMATH markeert een verschuiving in de evaluatie van wiskundige redenering:

• Van Antwoord naar Proces: Het benadrukt dat het eindantwoord niet genoeg is; de rigoureusheid van het bewijsproces is cruciaal.
• Betrouwbaarheid: Door het gebruik van gedrukte bronnen en formele verificatie biedt het een betrouwbaarder maatstaf voor de werkelijke capaciteiten van LLM's dan web-gescraped datasets.
• Onderzoeksrichtingen: De dataset biedt een basis voor het ontwikkelen van proces-gerichte beloningmodellen (reward models) die heuristische shortcuts kunnen straffen tijdens reinforcement learning. Het stelt ook de gemeenschap in staat om meertalige redeneerpatronen en de impact van taal op wiskundige prestaties grondig te bestuderen.

Kortom, OlymMATH is een essentiële nieuwe standaard om de grenzen van redenering in grote taalmodellen te testen, met name voor complexe, Olympiade-niveau problemen waar huidige modellen nog tekortschieten.