Technische Samenvatting: FormalRewardBench

Probleemstelling

Recente vooruitgang in neurale theoremaprovers is sterk afhankelijk van Versterkend Leren met Verifieerbare Beloningen (RLVR). In dit paradigma leveren bewijsassistenten (zoals Lean 4) binaire correctheidssignalen (slagen/mislukken) op basis van typecontrole. Hoewel deze signalen schaalbaar zijn en immuun voor beloningshacking, lijden ze aan spare credit toewijzing: modellen ontvangen geen leersignaal voor gedeeltelijke vooruitgang bij moeilijke problemen, aangezien een bewijs dat faalt in de laatste stap dezelfde nul-beloning ontvangt als een volledig onjuiste aanpak.

Om dit te mitigeren, hebben onderzoekers geleerde beloningsmodellen voorgesteld die in staat zijn bewijskwaliteit te evalueren voorbij binaire verificatie. Het vergelijken van deze beloningsmodellen is echter momenteel uitdagend, omdat dit doorgaans dure versterkende leertraining (RL) met ablatiestudies vereist. Bovendien richten bestaande benchmarks voor beloningsmodellen (zoals RewardBench en ProcessBench) zich op informele redenering in natuurlijke taal en adresseren ze niet de syntactische precisie, typecorrectheid en logische geldigheid die vereist zijn voor formeel theorema-bewijzen. Er is momenteel geen benchmark om beloningsmodellen direct te evalueren op formele bewijzen zonder trainingsruns.

Methodologie

De auteurs introduceren FormalRewardBench, de eerste benchmark die is ontworpen om beloningsmodellen te evalueren voor formeel theorema-bewijzen in Lean 4. De benchmark bestaat uit 250 voorkeursparen, waarbij elk paar een formeel geverifieerd correct bewijs en een onjuiste variant bevat.

Datasetconstructie

De dataset is afgeleid van MiniF2F, een collectie van 488 olympiade-niveau wiskundeproblemen die in Lean 4 zijn geformaliseerd. De auteurs maken gebruik van een gecontroleerde pipeline voor foutinjectie om onjuiste bewijzen te genereren die voldoen aan drie criteria:

1. Syntactische Validiteit: Het onjuiste bewijs moet parsen als geldige Lean-code.
2. Semantische Plausibiliteit: Fouten mogen niet triviaal zijn (bijvoorbeeld ongedefinieerde variabelen), maar moeten realistische faalmodi weerspiegelen.
3. Realistische Foutpatronen: Fouten moeten daadwerkelijke falen van Large Language Models (LLM's) nabootsen.

Foutinjectiestrategieën

Vijf door experts samengestelde strategieën worden gebruikt om onjuiste varianten te genereren, geïmplementeerd via prompts aan een frontier LLM (Claude Opus 4.5):

1. Minimale Enkele-Punt Variaties: Chirurgische modificaties aan correcte bewijzen (bijvoorbeeld het verwisselen van hypothesen, het wijzigen van een enkele variabele of lemmennaam) die semantisch falen veroorzaken terwijl de syntactische validiteit behouden blijft.
2. Motivering in Natuurlijke Taal: Het aanvullen van onjuiste bewijzen met misleidende commentaren in natuurlijke taal die het gebrekkige redeneren rechtvaardigen, om te testen op "verbositeit-bias".
3. Injectie van Python-code: Het vervangen van formele Lean-bewijsstappen door uitvoerbare Python-code die het probleem mogelijk computationeel oplost, maar faalt in de vereiste voor een formeel bewijs (het testen van taakvolging).
4. Geforceerde LLM-fouten: Het genereren van bewijzen met veelvoorkomende formele fouten die in eerdere modeloutput zijn geïdentificeerd, zoals onjuiste toepassing van tactieken, verkeerde selectie van hypothesen of onjuiste lemmainstantiatie.
5. Uitgebreide Onjuiste Bewijzen: Het genereren van onnodig lange bewijzen met verfijnde structuren en tussenliggende lemmata die fundamentele logische gebreken camoufleren.

Evaluatieprotocol

De benchmark evalueert modellen in twee settings:

• Puntsgewijs: Het model scoort elk bewijs onafhankelijk; nauwkeurigheid wordt gemeten als de score voor het correcte bewijs die van het onjuiste overtreft.
• Paarsgewijs: Het model vergelijkt twee bewijzen en geeft een voorkeur op. Om positiebias te mitigeren, wordt nauwkeurigheid alleen geteld als het model consistent het correcte bewijs identificeert in beide volgorde-indelingen (correct-eerst en correct-tweede).

Belangrijkste Resultaten

De auteurs evalueerden vier categorieën modellen: Frontier LLM's, Judge LLM's, General-Purpose LLM's en gespecialiseerde Theorema-bewijsmodellen.

1. Performantiehiërarchie: Frontier LLM's (bijvoorbeeld Claude Opus 4.5) behaalden de hoogste prestaties (59,8% paarsgewijze nauwkeurigheid). Judge LLM's (getraind op voorkeursdata) presteerden aanzienlijk beter dan gespecialiseerde theoremaprovers onder open-weight modellen (52,8% versus 12,8% voor sommige gespecialiseerde modellen).
2. De Generatie-Evaluatiekloof: Gespecialiseerde theorema-bewijsmodellen (bijvoorbeeld DeepSeek-Prover-V2-7B, Gödel-Prover-V2-8B) presteerden het slechtst (variërend van 0,0% tot 24,4%). Ondanks het behalen van state-of-the-art pass@k-metrics op MiniF2F worstelen deze modellen om bewijzen te evalueren. De auteurs schrijven dit toe aan een gebrek aan training in foutdetectie; deze modellen zijn geoptimaliseerd om correcte bewijzen te genereren via SFT en RLVR, maar hebben niet geleerd om fouten te identificeren of te bekritiseren.
3. Foutmoeilijkheidsgradiënt:
   • Makkelijkst: Injectie van Python-code (S3), waarbij detectie berust op taalidentificatie in plaats van bewijsbegrip.
   • Moeilijkst: Uitgebreide Onjuiste Bewijzen (S5) en Geforceerde Fouten (S4). Zelfs de beste modellen behaalden slechts ongeveer 60% op S5 en ongeveer 50% op S4.
   • Beperkingen van Judge-modellen: Judge-modellen vertoonden een bimodale patroon: bijna perfecte prestaties bij Python-injectie, maar instorten tot bijna nul bij uitgebreide bewijzen, wat suggereert dat hun voorkeurstraining oppervlakkige discriminatie ontwikkelt in plaats van diep formeel redeneren.
4. Positiebias: Er werd een significante positiebias waargenomen in alle categorieën, met name bij gespecialiseerde provers (bijvoorbeeld DeepSeek-Prover-V2-7B gaf 94,9% van de tijd de voorkeur aan het eerste bewijs, ongeacht de correctheid).

Betekenis en Claims

Het artikel claimt drie primaire bijdragen:

1. FormalRewardBench: Een nieuwe benchmark die directe vergelijking van beloningsmodellen voor formeel theorema-bewijzen mogelijk maakt zonder de noodzaak van dure RL-training met ablatiestudies.
2. Methodologie: Een herbruikbare set van vijf foutinjectiestrategieën voor het genereren van realistische onjuiste formele bewijzen, toepasbaar op andere bewijsassistenten, datavermeerdering of curriculumontwerp.
3. Empirisch Inzicht: De bevinding dat algemene beloningsmodelleringcapaciteiten (aangetroffen in frontier- en judge-modellen) effectiever overdragen naar bewijsevaluatie dan domeinspecifieke training in theorema-bewijzen.

De auteurs benadrukken dat hoewel het ontwikkelen van effectieve beloningsmodellen wiskundige ontdekking en verificatie kan versnellen, huidige modellen aanzienlijke beperkingen hebben. Zij wijzen erop dat formele verificatie de ultieme arbiter van correctheid blijft, aangezien imperfecte beloningsmodellen risico's van overmatige afhankelijkheid met zich meebrengen. De benchmark wordt publiek vrijgegeven om verder onderzoek naar beloningsmodellen voor formele wiskunde te stimuleren.

Het artikel concludeert met het benoemen van beperkingen, waaronder de afhankelijkheid van automatische verificatie voor de meeste voorbeelden, de focus uitsluitend op Lean 4, en de uitsluiting van procesniveau- of stap-voor-stap-evaluatie. Voor toekomstig werk wordt voorgesteld om zich te richten op hybride benaderingen die geleerde beloningsmodellen combineren met formele verificatie en de benchmark uit te breiden naar andere bewijsassistenten zoals Coq en Isabelle.