Proof-RM: A Scalable and Generalizable Reward Model for Math Proof

1. Het Probleem: De Asymmetrie van Verificatie in Wiskunde

Hoewel Large Language Models (LLMs) sterke redeneervermogens hebben ontwikkeld voor wiskundige problemen via Reinforcement Learning with Verifiable Rewards (RLVR), stuiten ze op een fundamentele beperking bij bewijsvoering.

• Asymmetrie van verificatie: Bij veel wiskundige taken (zoals meerkeuzevragen of numerieke antwoorden) is het controleren van het eindantwoord eenvoudig en objectief (bijv. string matching). Echter, bij volledige wiskundige bewijzen is het vaststellen van de juistheid complex. Een bewijs vereist een stap-voor-stap controle van logica, de toepassing van theorema's, en het voldoen aan voorwaarden.
• Beperkingen van bestaande methoden: Bestaande RLVR-methoden vertrouwen vaak op het eindantwoord. Dit leidt tot "shortcut learning", waarbij modellen een correct eindantwoord kunnen genereren met een onjuist of incompleet bewijs (bijv. door niet-bestaande theorema's te gebruiken of logische gaten te negeren).
• Kosten van menselijke annotatie: Het nauwkeurig evalueren van complexe bewijzen vereist experts (zoals IMO-deelnemers), wat extreem duur en niet schaalbaar is voor het trainen van reward modellen (RM).

2. Methodologie: Proof-RM Pipeline

De auteurs introduceren een schaalbaar framework om een Reward Model te trainen dat volledige bewijsprocessen kan evalueren. De aanpak bestaat uit drie hoofdstappen:

A. Schaalbare Data-Constructie (QPC Triplets)

Om een generaliseerbaar model te trainen, is een divers dataset nodig van Question-Proof-Check (QPC) triplets.

• Diversiteit: De pipeline combineert bewijzen uit diverse bronnen (Olympiades, Putnam, USAMO, studentenwerk) met verschillende generatiemethoden (herformulering, maskeren van stappen, augmentatie) en verschillende LLMs (DeepSeek-R1, GPT-5-mini, Gemini, etc.).
• Generatie van fouten: LLMs worden geprompt om niet alleen correcte bewijzen te genereren, maar ook foutieve bewijzen met specifieke foutpatronen (logische gaten, hallucinaties, onvolledige redenering).
• Labeling met menselijke validatie: Omdat menselijke annotatie duur is, gebruiken de auteurs een hybride aanpak:
  1. Drie verschillende LLMs beoordelen elk bewijs vijf keer.
  2. Alleen bewijzen waarbij alle LLMs overeenkomen (unanimiteit) worden behouden.
  3. Combinatie-niveau menselijke check: Data wordt opgesplitst in combinaties (bron + methode + model). Voor elke combinatie wordt een steekproef (5%) door mensen gecontroleerd. Als de menselijke consistentie met de LLM-labels hoog genoeg is (>75-90%), wordt die hele dataset-combinatie als "silver-standard" geaccepteerd. Dit bespaart >90% van de menselijke tijd ten opzichte van handmatige controle van elk item.
  • Resultaat: Een dataset van ~21.000 QPC-triplets.

B. Stabiele RLVR Training

Het trainen van een RM met binair T/F (True/False) supervisie op lange redeneerprocessen leidt vaak tot instabiliteit en "model collapse" (herhaling van tokens, syntactische incoherentie). De auteurs introduceren twee innovaties om dit op te lossen:

1. LLM-as-a-RM-for-RM: Een apart LLM (DeepSeek-V3.1) controleert de output van het Reward Model op oppervlakkige fluïditeit en gedragsconsistentie (bijv. herhaling van tokens, zinloze zinnen, overhaaste conclusies). Als het RM een foutieve outputstructuur genereert, krijgt het een negatieve beloning, zelfs als het eindantwoord (T/F) correct is. Dit voorkomt dat het model "geluk" leert.
2. Balanced Token Weighting: Bestaande token-weighting strategieën (zoals GRPO of DAPO) leiden tot ongewenste variaties in de outputlengte (te kort of te lang). De auteurs gebruiken een gewogen gemiddelde van token-weights om de lengte van de redenering stabiel te houden tijdens het trainen.

C. Architectuur

Het model is gebaseerd op DeepSeek-R1-0528-distill-Qwen3 (8B, 14B, 32B). Er wordt geen aparte SFT-fase (Supervised Fine-Tuning) gebruikt; het model start direct met RLVR omdat de basismodellen al sterke redeneerfähigheden hebben.

3. Belangrijkste Bijdragen

1. Analyse van verificatie-asymmetrie: Het paper benadrukt dat de huidige successen in wiskundig RL grotendeels gebaseerd zijn op datasets met sterke verificatie-asymmetrie (eenvoudig eindantwoord) en pleit voor modellen die het proces van bewijsvoering controleren.
2. Schaalbare Data-pipeline: Een methode om grote hoeveelheden hoogwaardige, diverse QPC-data te genereren met minimale menselijke inspanning via "composition-level human check".
3. Stabiele RL-training voor Proof-RM: Een praktische trainingsspecificatie (LLM-as-a-RM-for-RM + balanced token weighting) die modelcollapse voorkomt en stabiele prestaties garandeert over lange trainingstrajecten (>300 stappen).

4. Resultaten

De experimenten tonen aan dat Proof-RM superieur is aan bestaande baselines en frontier LLMs:

• Nauwkeurigheid: ProofRM-32B bereikt 82,4% nauwkeurigheid op de testset, wat een aanzienlijke verbetering is ten opzichte van de basismodellen (bijv. +9,9% t.o.v. Distill-Qwen3-32B) en ook beter presteert dan gesloten modellen zoals GPT-5-mini en Gemini-2.5-Flash.
• Generalisatie: Het model generaliseert uitstekend naar onbekende datasets (zoals de OPC-dataset van Dekoninck et al.), waar het de prestaties van DeepSeek-R1 overtreft en dicht bij Gemini-2.5-Flash komt.
• Test-time Scaling (Best-of-k): ProofRM kan effectief worden gebruikt om de beste bewijzen te selecteren uit een set gegenereerde kandidaten. De "Best-of-k" curves tonen aan dat ProofRM een betere discriminatievermogen heeft dan baselines, wat essentieel is voor agents die tijdens het testen meerdere opties genereren.
• Foutdetectie: Het model is beter in het identificeren van complexe logische fouten (zoals onvolledige logische flows en misbruik van aannames) dan ongetrainde baselines, die vaak "geloofwaardige" maar foutieve bewijzen accepteren.

5. Betekenis en Impact

• Oplossing voor complexe wiskunde: Proof-RM biedt een haalbare route om RL toe te passen op bewijsgebaseerde wiskundige problemen, een domein dat tot nu toe te duur en complex was voor geautomatiseerde evaluatie.
• Vertrouwen in AI: Door het vermogen om de logica van een bewijs te verifiëren en niet alleen het eindantwoord, verhoogt dit model de betrouwbaarheid van AI-systemen in wetenschappelijke en educatieve contexten.
• Schaalbaarheid: De gepresenteerde pipeline toont aan dat het mogelijk is om grote, diverse datasets voor bewijsverificatie te creëren zonder de onhaalbare kosten van volledige menselijke annotatie, wat een katalysator is voor toekomstige doorbraken in AI-wiskunde.

Kortom, Proof-RM is een doorbraak in het overbruggen van de kloof tussen het genereren van complexe wiskundige bewijzen en het betrouwbaar verifiëren daarvan, waardoor het mogelijk wordt om LLMs te trainen op het niveau van topwiskundigen.