Technische Samenvatting: Niet alle bewijzen zijn gelijk: Het evalueren van de kwaliteit van LLM-bewijzen voorbij correctheid

Probleemstelling

Hoewel Large Language Models (LLM's) een aanzienlijk vermogen hebben getoond in het genereren van correcte wiskundige bewijzen, richten huidige evaluatiebenchmarks zich bijna uitsluitend op correctheid. Deze eenzijdige focus negeert cruciale dimensies van bewijskwaliteit die essentieel zijn voor wiskundig nut, zoals helderheid, beknoptheid, inzicht en overdraagbaarheid. Een bewijs kan formeel correct zijn, maar kan ook overdreven verbaal zijn, leunen op tedieuze brute-force berekeningen, obscure technieken gebruiken die ontoegankelijk zijn voor de beoogde doelgroep, of er niet in slagen zich aan te passen aan specifieke methodologische beperkingen. Bov�ловать, bestaande benchmarks behandelen alle correcte bewijzen vaak als even waardevol, waardoor ze de substantiële stilistische en structurele variaties tussen hen niet kunnen vatten. De uitdaging ligt in het definiëren en meten van deze subjectieve kwaliteiten op een schaalbare, geautomatiseerde manier zonder te vertrouwen op dure of inconsistente menselijke evaluatie.

Methodologie: PROOFRANK

Om deze tekortkomingen aan te pakken, introduceren de auteurs PROOFRANK, de eerste benchmark die specifiek is ontworpen om schaalbare proxies van bewijskwaliteit in door LLM gegenereerde wiskunde te evalueren. De benchmark bestaat uit 382 uitdagende, competitie-problemen met een eindantwoord die de gebieden algebra, meetkunde, combinatoriek, calculus en getaltheorie beslaan. Het gebruik van problemen met een eindantwoord maakt schaalbare correctheidsverificatie mogelijk, terwijl nog steeds rigoureuze schriftelijke bewijzen vereist zijn.

Het evaluatiekader steunt op paarsgewijze vergelijkingen van correcte oplossingen om de moeilijkheid van het toekennen van absolute scores aan diverse problemen te vermijden. Correctheid wordt behandeld als een vereiste; modellen worden alleen vergeleken op problemen waar beide modellen geldige oplossingen produceren. PROOFRANK evalueert vijf complementaire metrieken, onderverdeeld in twee typen:

1. Bewijs-niveau metrieken (Het vergelijken van individuele bewijzen)

• Beknoptheid: Gemeten via compressibiliteit. Een sterk redeneermodel probeert een bewijs in te korten terwijl de logische equivalentie behouden blijft. De metriek is de ratio van de oorspronkelijke tekstlengte tot de verkorte lengte. Lagere ratio's duiden op hogere beknoptheid (meer redundante tekst verwijderd).
• Computationele Gemak: Beoordeelt in welke mate een bewijs leunt op tedieuze algebra, enumeratie of gevalcontrole (case-checking). Een LLM-rechter vergelijkt paren bewijzen om te bepalen welk bewijs minder "tijd om te volgen" vereist vanwege notatiedichtheid en expliciete berekening.
• Cognitieve Eenvoud: Meet de toegankelijkheid van de gebruikte bewijstechnieken. Het evalueert de complexiteit van de kernideeën, de verfijning van de instrumenten (bijv. niche-stellingen versus standaardmethoden) en de moeilijkheid van het integreren van meerdere concepten.

2. Probleem-niveau metrieken (Het vergelijken van modelgedrag over meerdere pogingen)

• Diversiteit: Kwantificeert het vermogen van een model om verschillende geldige benaderingen van hetzelfde probleem te produceren. Oplossingen worden gegroepeerd op techniek (met behulp van door LLM gegenereerde samenvattingen), en diversiteit wordt gemeten door de entropie van de distributie van het model over deze clusters.
• Adaptiviteit: Evalueert of een model een correct bewijs kan produceren terwijl het zich houdt aan een gespecificeerde techniek die in de prompt is gevraagd. Dit test het vermogen van het model om aan beperkingen te voldoen en specifieke wiskundige paden te verkennen.

Rangschikkingssysteem: Paarsgewijze uitkomsten worden geaggregeerd naar model-niveau ratings met behulp van een Bradley-Terry model, wat Elo-achtige scores oplevert. Deze aanpak verzacht de biases die inherent zijn aan absolute scoring en gaat om met incomplete vergelijkingsgrafieken waarbij modellen niet elk probleem oplossen.

Belangrijkste Bijdragen

1. Schaalbare Bewijs-stijl Metrieken: De auteurs definiëren en implementeren een suite van vijf metrieken (beknoptheid, computationeel gemak, cognitieve eenvoud, diversiteit, adaptiviteit) die dienen als concrete, meetbare proxies voor subjectieve bewijskwaliteit.
2. PROOFRANK Benchmark: De introductie van een uitgebreide benchmark bestaande uit 382 competitie-niveau problemen, samengesteld om LLM's te evalueren voorbij loutere correctheid.
3. Empirische Evaluatie van Frontier Modellen: Een systematische evaluatie van 10 state-of-the-art modellen (waaronder GPT-5.4, Gemini-3.1-Pro, Kimi-K2.5, etc.), die duidelijke sterktes en zwaktes onthult die onzichtbaar zijn voor correctheid-alleen benchmarks.

Experimentele Resultaten

De evaluatie onthult substantiële verschillen in bewijskwaliteit tussen modellen die niet door nauwkeurigheid alleen worden gevangen:

• Dominantie van GPT-5.4: GPT-5.4 voert de ranglijst aan, met de hoogste nauwkeurigheid (86,4%) en top performance op drie van de vijf kwaliteitmetrieken (Computationeel Gemak, Cognitieve Eenvoud en Adaptiviteit).
• Trade-offs en Divergentie: Er is een lage correlatie tussen nauwkeurigheid en kwaliteitmetrieken. Bijvoorbeeld, GLM-5 bereikt een redelijke nauwkeurigheid (49,1%), maar presteert onder het gemiddelde op alle kwaliteitmetrieken. Daarentegen scoort QWEN3.5-397B hoog op Computationeel Gemak (het vermijden van brute-force methoden), maar heeft de laagste nauwkeurigheid onder de geëvalueerde modellen, wat wijst op een trade-off tussen elegantie en correctheid.
• Modelspecifieke Zwaktes: GEMINI-3.1-PRO presteert bijzonder slecht op beknoptheid, waarbij oplossingen gemiddeld 3,5 keer verbaaler zijn dan nodig. KIMI-K2.5-THINK is het meest beknopte model, maar staat het laagst in Cognitieve Eenvoud.
• Effecten van Prompting: Experimenten tonen aan dat beknoptheid gedeeltelijk controleerbaar is via prompting. Het afdwingen van beknoptheid leidt echter vaak tot significante dalingen in nauwkeurigheid (bijv. een daling van ~15% voor Kimi en DeepSeek), wat suggereert dat stijloptimalisatie geen "gratis" verbetering is en een zorgvuldige balans vereist.
• Noodzaak van Correctheidfiltering: Wanneer de correctheidsfiltering wordt verwijderd, verschuiven de rangschikkingen drastisch. Modellen die eenvoudige maar incorrecte argumenten produceren (bijv. STEP-3.5-FLASH) blazen hun kwaliteitsscores kunstmatig op, wat onderstreept dat evaluatie van kwaliteit gebaseerd moet zijn op correctheid.

Betekenis en Claims

Het artikel claimt dat PROOFRANK een noodzakelijke uitbreiding biedt van het evaluatielandschap voor wiskundig redeneren in LLM's. Door verder te gaan dan binaire correctheid, onthult de benchmark dat modellen over verschillende "bewijs-persoonlijkheden" beschikken — sommige zijn rigoureus maar verbaal, andere zijn elegant maar foutgevoelig, en sommige zijn adaptief terwijl anderen rigide zijn.

De auteurs stellen dat deze bevindingen cruciaal zijn voor praktische toepassingen:

• Educatieve en Onderzoek Nut: In educatieve omgevingen zijn de helderheid en het inzicht van een bewijs even belangrijk als de correctheid ervan. In onderzoek kan het vermogen om diverse of aanpasbare bewijzen te genereren helpen bij het verkennen van nieuwe wiskundige wegen.
• Modelselectie: De niet-triviale trade-offs tussen nauwkeurigheid en kwaliteitmetrieken suggereren dat gebruikers modellen moeten selecteren op basis van specifieke behoeften (bijv. prioriteit geven aan computationeel gemak voor verificatie of diversiteit voor brainstormen) in plaats van enkel te vertrouwen op nauwkeurigheidsscores.
• Toekomstige Richtingen: Het werk suggereert dat toekomstige evaluaties van wiskundig redeneren de bruikbaarheid van gegenereerde bewijzen moeten meten, waarbij wordt erkend dat een correct bewijs niet inherent een goed bewijs is als het er niet in slaagt inzicht te communiceren of over te dragen naar andere contexten.

Het artikel blijft bescheiden over de beperkingen en erkent dat bewijskwaliteit inherent subjectief is en dat hun metrieken proxies zijn in plaats van absolute maten. Het vertrouwt op LLM-judges, wat potentiële biases introduceert, hoewel uitgebreide validatie-experimenten suggereren dat deze proxies robuust zijn en redelijk goed aansluiten bij menselijke oordelen op specifieke dimensies zoals computationeel gemak en cognitieve eenvoud.