Technische Samenvatting: IMProofBench

Probleemstelling

Huidige benchmarks voor het evalueren van Large Language Models (LLM's) op het gebied van wiskunde zijn ontoereikend voor het beoordelen van onderzoeksniveau-capaciteiten. Bestaande datasets richten zich voornamelijk op wiskundige problemen uit de middelbare school of de bacheloropleiding (bijv. AIME, MATH), die steeds vaker oplosbaar zijn door state-of-the-art modellen en er niet in slagen echte bewijsvoeringsvaardigheden te testen. Bovendien beperken benchmarks die zich richten op geavanceerde wiskunde, zoals FrontierMath en Humanity's Last Exam (HLE), de evaluatie vaak tot de correctheid van het eindantwoord. Deze beperking stelt modellen in staat om shortcuts te gebruiken of het juiste antwoord te raden zonder logisch sluitende argumenten te construeren, waardoor de cruciale vaardigheid van het genereren van rigoureuze wiskundige bewijzen over het hoofd wordt gezien. Er is een gebrek aan een gestandaardiseerde, private benchmark die LLM's evalueert op bewijsvoering op onderzoeksniveau binnen een realistische, door tools ondersteunde omgeving.

Methodologie

Benchmark Constructie (IMProofBench)

IMProofBench is een private benchmark bestaande uit 77 peer-reviewed problemen, ontwikkeld in samenwerking met meer dan 44 professionele wiskundigen. De procesgang voor probleemcreatie omvat:

• Auteurschap: Problemen worden geschreven door onderzoekers binnen hun specifieke expertisegebieden, variërend van mondelinge examenvragen op masterniveau tot open onderzoeksproblemen.
• Peer Review: Elke inzending ondergaat een strikt beoordelingsproces door een kernteamlid en een externe expert in het relevante vakgebied om de wiskundige correctheid, passende moeilijkheidsgraad en helderheid te waarborgen.
• Structuur: Elk probleem bestaat uit een hoofdbewerking voor bewijsvoering en vervolgvragen met unieke, automatisch te beoordelen antwoorden. Deze dubbele structuur ondersteunt zowel de menselijke expertbeoordeling van het bewijs als de geautomatiseerde kwantitatieve analyse van eindantwoorden.
• Dynamisch Karakter: De benchmark is ontworpen als een continu platform. Problemen worden op basis van voortgang toegevoegd, en auteurs worden aangemoedigd om problemen te laten uitfaseren als deze door nieuw onderzoek oplosbaar worden, zodat de benchmark niet verzadigd raakt.

Evaluatiekader

De evaluatie simuleert een realistische onderzoeksomgeving met behulp van een agentic framework gebouwd op het Inspect framework. Modellen opereren met toegang tot:

• Computationele Tools: Python (NumPy, SciPy, SymPy), Bash (Arch Linux), en gespecialiseerde wiskundige software waaronder SageMath, GAP, Maxima, PARI/GP en Singular.
• Literatuuronderzoek: Webzoekmogelijkheden om relevante stellingen, papers of data (bijv. OEIS) te lokaliseren.
• Interactie: Modellen nemen deel aan interacties met meerdere beurten, waarbij ze een submit-tool gebruiken om redeneringsstappen te onderscheiden van de definitieve outputs.

Beoordelingsproces

Evaluatie vindt plaats in twee stadia:

1. Geautomatiseerde Beoordeling: Vervolgvragen worden beoordeeld door de outputs van het model te vergelijken met de grondwaarheid (ground-truth) antwoorden.
2. Menselijke Expertbeoordeling: Het hoofd-bewijs wordt geëvalueerd door de auteur van het probleem aan de hand van een 0–3 schaal:
   • 0/3: Geen vooruitgang.
   • 1/3: Minimale vooruitgang (beperkte voortgang).
   • 2/3: Significante vooruitgang (substantiële arbeid voltooid).
   • 3/3: Volledige oplossing.
     Beoordelaars annoteren ook specifieke fouttypen (logische fouten, hallucinaties, rekenfouten, conceptuele misverstanden) en prestatie-indicatoren (begrip, correcte resultaten, inzichten, bruikbaarheid). Om bias te voorkomen, worden de identiteiten van de modellen verborgen tijdens de beoordeling.

Belangrijkste Bijdragen

1. IMProofBench: Een private, evoluerende benchmark die specifiek is ontworpen voor wiskundige bewijsvoering op onderzoeksniveau, ontwikkeld door directe samenwerking met de wiskundige gemeenschap.
2. Systematische Analyse: Een uitgebreide evaluatie van state-of-the-art LLM's op bewijsvoering, beoordeeld door menselijke experts, wat verder gaat dan eenvoudige nauwkeurigheid van het eindantwoord.
3. Kwalitatieve Inzichten: Een gedetailleerde analyse van de sterktes en faalmodi van modellen, waarbij het gat tussen de nauwkeurigheid van het eindantwoord en de werkelijke bewijsvoeringscapaciteit, evenals de interactie van modellen met research tools, wordt belicht.

Experimentele Resultaten

Prestatieoverzicht

De auteurs evalueerden 10 LLM's op het bewijsgerichte deel van de benchmark:

• Top Performers: GPT-5.4 behaalde de hoogste prestaties en produceerde volledige oplossingen (3/3) voor 49% van de taken. GEMINI-3.1-PRO volgde op korte afstand met 46%.
• Lagere Performers: CLAUDE-OPUS-4.6 leverde slechts volledige oplossingen voor 32% van de taken.
• Open Problemen: Onder de 23 open onderzoeksvragen in de benchmark loste GPT-5 er één op in december 2025.

Eindantwoord vs. Bewijsvoering

Op de subset van 45 vragen met vervolgvragen scoorde GPT-5.4 75% op nauwkeurigheid van het eindantwoord. De correlatie tussen de scores van de vervolgvragen en de door mensen beoordeelde voortgang van het bewijs was 0.51, wat suggereert dat hoewel de nauwkeurigheid van het eindantwoord een nuttige benadering is, het niet de nuance bezit die nodig is om de kwaliteit van het redeneerproces te evalueren.

Fout- en Toolanalyse

• Fouttypen: Logische fouten waren de meest voorkomende faalmodus (bijv. ongegronde aannames), met name bij CLAUDE-OPUS-4.6 (40% van de reacties). Hallucinaties van niet-bestaande stellingen werden eveneens waargenomen.
• Toolgebruik: Modellen varieerden aanzienlijk in toolgebruik. GEMINI-3.1-PRO deed bijna vier keer zoveel tool-aanroepen als andere modellen, maar gebruikte de minste output-tokens.
• Ablatie-studie: Een ablatie op de agentic setup toonde aan dat toegang tot tools de prestaties over het algemeen verbeterde (bijv. +14.4% voor GROK-4), hoewel sommige modellen (bijv. GEMINI-2.5-PRO) een lichte afname vertoonden, waarschijnlijk door suboptimale toolselectie (bijv. het overmatig gebruiken van code-interpreters voor wiskundige redenering).

Kwalitatieve Observaties

• Literatuurkennis: Toonaangevende modellen toonden een sterke bekendheid met gespecialiseerde wiskundige literatuur, maar hadden moeite met obscure bronnen zoals privé collegesnotities.
• Hallucinatie en Zelfvertrouwen: Modellen hallucineerden regelmatig resultaten om een antwoord te forceren en onthielden zich zelden van het geven van een oplossing, zelfs wanneer ze vastliepen. Ze presenteerden vaak gebrekkige argumenten met een hoog zelfvertrouwen.
• Inzicht: Ondanks fouten boden modellen frequent inzichten en gedeeltelijke voortgang die nuttig kunnen zijn voor menselijke onderzoekers, waarbij GPT-5.4 in ongeveer 60% van de pogingen betekenisvolle bijdragen leverde.

Betekenis en Claims

Het artikel stelt dat IMProofBench een kritiek gat in de AI-evaluatie dicht door de focus te verschuiven van competitie-stijl problemen naar bewijsvoering op onderzoeksniveau. De auteurs stellen dat:

1. Huidige Capaciteiten: State-of-the-art LLM's kunnen al een betekenisvol deel van de onderzoeksgerelateerde problemen oplossen, wat hun potentieel als wiskundige collaborateurs aangeeft.
2. Beperkingen: Huidige modellen blijven imperfect, gevoelig voor logische fouten en hallucinaties, en missen vaak het vermogen om onderscheid te maken tussen een correct eindantwoord en een geldig bewijs.
3. Noodzaak van Evaluatie: De benchmark toont aan dat metrieken gebaseerd op het eindantwoord onvoldoende zijn om wiskundige capaciteit te meten; menselijke expertbeoordeling van het redeneerproces is essentieel.
4. Toekomstige Richting: Dit werk vestigt een kader voor de continue, dynamische evaluatie van LLM's in realistische onderzoeksomgevingen, wat de studie naar hoe AI effectief kan worden geïntegreerd in wiskundige workflows faciliteert.

De auteurs hanteren een bescheiden standpunt door te merken dat de benchmark momenteel nog in actieve ontwikkeling is met een beperkt aantal problemen (77), maar beargumenteren dat zelfs deze schaal waardevolle inzichten biedt in de trajectorie van AI in wiskundig onderzoek.