Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning

In de wereld van de wiskunde bestaat er een hardnekkige kloof tussen de taal die mensen gebruiken om ideeën te beschrijven en de rigide, precieze taal die computers nodig hebben om ze te verifiëren. Wiskundigen schrijven bewijzen in natuurlijke taal, vol nuance en context, terwijl computers formele verklaringen vereisen die geen ruimte laten voor ambiguïteit. Het overbruggen van deze kloof is een taak genaamd autoformalisatie, waarbij kunstmatige intelligentie probeert een menselijke wiskundige gedachte te vertalen naar een code-achtig formaat dat een computer kan controleren. Jarenlang was de hoop dat machines niet alleen deze vertalingen konden uitvoeren, maar ook hun eigen werk konden beoordelen, optredend als een geautomatiseerde scheidsrechter om te waarborgen dat de wiskunde correct is. Het controleren van dit werk is echter een hardnekkige flessenhals gebleven. Hoewel computers gemakkelijk kunnen zien of een regel code syntactisch gebroken is, hebben ze moeite om te begrijpen of het vertaalde idee daadwerkelijk hetzelfde betekent als de oorspronkelijke menselijke gedachte. Menselijke experts kunnen dit wel, maar het proces is traag, duur en moeilijk op te schalen naarmate wiskundige problemen complexer worden.

Een nieuwe studie pakt deze uitdaging aan door een slimmere manier voor kunstmatige intelligentie voor te stellen om als rechter op te treden. In plaats van één groot taalmodel te vragen om een snelle, algemene beoordeling te geven op een vertaalde wiskundige opgave, hebben de onderzoekers een systeem ontwikkeld dat de evaluatie onderverdeelt in specifieke, beheersbare onderdelen. Ze ontdekten dat wanneer een AI wordt begeleid om naar afzonderlijke kwaliteiten te kijken—zoals of de logische structuur behouden is gebleven, of de wmathematische objecten consistent zijn, en of de uiteindelijke code beknopt is—het een veel betrouwbaardere en nauwkeurigere beoordeling produceert dan wanneer het wordt gevraagd om een enkel, breed oordeel. De studie demonstreert dat deze gedetailleerde, meerstapsbenadering zelfs kleinere, minder krachtige AI-modellen laat presteren beter dan grotere, complexere modellen die vertrouwen op grove, algemene oordelen. Door de evaluatie te organiseren in een duidelijke set criteria, hebben de onderzoekers een schaalbare methode gecreëerd die ons dichter bij een toekomst brengt waarin machines hun eigen wiskundige redenering betrouwbaar kunnen verifiëren, waardoor de noodzaak voor constante menselijke supervisie wordt verminderd.

De kern van het probleem ligt in hoe we deze vertalingen momenteel evalueren. Traditioneel, als een computer niet kan bewijzen dat een stelling waar is met behulp van een stellingbewijzer (theorem prover), wordt de vertaling als mislukt gemarkeerd. Dit binaire pass-of-fail-systeem behandelt alle fouten als gelijk, of het nu gaat om een kleine typefout of een fundamenteel misverstand van de wiskunde. Het biedt geen inzicht in wat er misging of hoe dicht de vertaling bij de correctheid was. Om dit op te lossen, introduceerden de onderzoekers een raamwerk dat evaluatie behandelt als een checklist van specifieke attributen in plaats van een enkele score. Ze definieerden vier hoofdpijlers voor het beoordelen van een vertaling: logische preservatie, wat controleert of de oorspronkelijke redeneerstappen intact zijn gebleven; wiskundige consistentie, wat ervoor zorgt dat de getallen en operaties zinvol zijn; formele kwaliteit, die kijkt naar hoe schoon en leesbaar de code is; en formele validiteit, die bevestigt dat de code de strikte grammaticale regels van de computertaal volgt.

Om dit idee te testen, stelde het team een experiment op waarbij ze verschillende modellen van kunstmatige intelligentie vroegen om als rechter op te treden. Ze vergeleken twee verschillende benaderingen. In de eerste werd een model gevraagd om naar een vertaling te kijken en er een enkele algemene score aan te geven, vergelijkbaar met een docent die een essay beoordeelt met één lettercijfer. In de tweede benadering werd hetzelfde model gevraagd de vertaling te evalueren tegen de specifieke pijlers die hierboven werden genoemd, waarbij een aparte score werd gegeven voor logica, consistentie, kwaliteit en validiteit. Deze individuele scores werden vervolgens gecombineerd om tot een definitieve beoordeling te komen. De onderzoekers gebruikten een dataset van wiskundige problemen uit twee bekende bronnen, die zowel door mensen geschreven vertalingen als vertalingen gegenereerd door verschillende AI-modellen bevatten. Ze vergeleken vervolgens de rangschikkingen geproduceerd door deze AI-rechters met de rangschikkingen gegeven door menselijke experts.

De resultaten waren opmerkelijk. De benadering die gebruik maakte van de gedetailleerde, meerdelige evaluatie presteerde consequent beter dan de methode met de enkele score. Wanneer de AI-rechters werden begeleid om naar de specifieke atomaire eigenschappen van de vertaling te kijken, kwamen hun rangschikkingen van de vertalingen veel nauwer overeen met de rangschikkingen van de menselijke experts. In veel gevallen stelde de fijnmazige benadering zelfs kleinere, minder rekenintensieve AI-modellen in staat om beter te presteren dan grotere, krachtigere modellen die de grove, enkelvoudige score-methode gebruikten. Dit suggereert dat de structuur van het evaluatieproces belangrijker is dan enkel de omvang van de 'hersenen' die de beoordeling uitvoeren. Door de taak onder te verdelen, konden de modellen zich concentreren op specifieke signalen van correctheid die ze in een brede, algemene beoordeling wellicht zouden missen.

De studie onderzocht ook hoe deze AI-rechters en menselijke experts in hun denken verschilden. Bij het evalueren van gebrekkige vertalingen hadden menselijke experts de neiging om de verschillende aspecten van de vertaling als aparte kwesties te behandelen; een probleem met de logica betekende niet noodzakelijkerwijs dat de code slecht geschreven was. De AI-modellen vertoonden echter vaak de neiging om deze aspecten aan elkaar te koppelen, waarbij een fout in één gebied de beoordeling van een ander gebied leek te beïnvloeden. Ondanks dit verschil in hoe zij de informatie verwerkten, hielp de gedetailleerde evaluatiemethode de AI-modellen om hun uiteindelijke conclusies af te stemmen op het menselijke oordeel. De onderzoekers vonden dat de AI-rechters bijzonder goed waren in het identificeren wanneer een vertaling syntactisch geldig maar semantisch onjuist was, een onderscheid dat cruciaal is voor wiskundige redenering.

Een van de meest praktische bevindingen was dat deze gedetailleerde methode efficiënt is. Omdat de evaluatie is onderverdeeld in kleinere taken, is het niet nodig om de meest massieve en dure AI-modellen te gebruiken om goede resultaten te behalen. De onderzoekers toonden aan dat een kleiner model, wanneer geleid door deze specifieke set criteria, resultaten kon behalen die vergelijkbaar zijn met die van veel grotere modellen. Dit is significant omdat het betekent dat hoogwaardige evaluatie van wiskundige redenering toegankelijk en betaalbaar kan worden, in plaats van beperkt te zijn tot degenen met toegang tot de krachtigste computerbronnen. Het systeem bleek ook stabiel te zijn; zelfs wanneer de AI-modellen meerdere keren werden uitgevoerd met lichte variaties in hun interne willekeur, bleven de uiteindelijke scores consistent, wat suggereert dat de methode robuust is.

Uiteindelijk biedt dit werk een nieuw pad voorwaarts voor het veld van automatische wiskundige redenering. Het beweegt weg van het idee dat een enkele, monolithische AI-rechter de beste oplossing is en omarmt in plaats daarvan een meer gestructureerde, ensemble-benadering. Door duidelijke, interpreteerbare criteria te definiëren voor wat een goede vertaling maakt, hebben de onderzoekers een systeem gecreëerd dat niet alleen nauwkeuriger maar ook transparanter is. We kunnen precies zien waarom een vertaling hoog of laag is beoordeeld, in plaats van alleen een 'black-box' score te ontvangen. Deze helderheid is essentieel voor het opbouwen van vertrouwen in geautomatiseerde systemen en voor het gebruik ervan om wiskundigen en computerwetenschappers te helpen bij het aanpakken van steeds complexere problemen. De studie suggereert dat de toekomst van het evalueren van machinale redenering niet ligt in het groter maken van de rechters, maar in het preciezer maken van de vragen die zij stellen.