VERIFY-RL: Verifiable Recursive Decomposition for Reinforcement Learning in Mathematical Reasoning

Technische Samenvatting: VERIFY-RL

1. Het Probleem: De tekortkomingen van heuristische decompositie

Bij het trainen van Large Language Models (LLM's) voor wiskundig redeneren is curriculum learning (het stapsgewijs trainen van eenvoudige naar complexe problemen) zeer effectief. De huidige methoden voor het opdelen van complexe problemen in subproblemen (decompositie) zijn echter vaak heuristisch. Dit betekent dat modellen zelf proberen "makkelijkere" varianten te genereren.

Het onderzoek identificeert drie fundamentele problemen met deze aanpak:

1. Gebrek aan garanties: Er is geen bewijs dat een gegenereerd subprobleem daadwerkelijk eenvoudiger is.
2. Gebrek aan relevantie: Er is geen garantie dat het oplossen van een subprobleem daadwerkelijk helpt bij het oplossen van het hoofdtraject (gebrek aan kennisoverdracht).
3. Ruis in training: Een aanzienlijk deel van de heuristisch gegenereerde decomposities (ongeveer 21,6%) is wiskundig ongeldig, wat leidt tot foutieve patronen en instabiliteit tijdens de Reinforcement Learning (RL) fase.

2. Methodologie: Verifieerbare Recursieve Decompositie

De auteurs introduceren VERIFY-RL, een raamwerk dat decompositie niet laat genereren door een model, maar afleidt uit formele wiskundige regels (in dit geval symbolische differentiatie). Het raamwerk rust op drie strikte, verifieerbare eigenschappen (V1–V3):

• V1: Structural Simplicity (Eenvoud): Het subprobleem moet een lagere structurele complexiteit (nesting depth $\delta$) hebben dan het hoofdtraject.
• V2: Solution Containment (Hulpvaardigheid): De oplossing van het subprobleem moet een onderdeel (factor of term) zijn van de oplossing van het hoofdtraject. Dit garandeert dat het leren van de subtaak direct bijdraagt aan de hoofdtas.
• V3: Rule Derivation (Relatie): De decompositie moet direct voortvloeien uit een formele calculusregel (zoals de kettingregel, productregel of somregel).

Het proces:

1. Decompositie: Problemen worden recursief afgebroken tot basisgevallen ($D_1$) met behulp van symbolische regels.
2. Verificatie: Elke stap wordt automatisch gecontroleerd via symbolische computatie (SymPy) om te voldoen aan V1, V2 en V3. Dit resulteert in "verificatie door constructie" (100% succesrate).
3. Curriculum Constructie: De problemen worden via een topological sort gerangschikt van laag naar hoog niveau van complexiteit.
4. RL Training: Modellen (0.6B tot 3B parameters) worden getraind met algoritmen zoals GRPO (Group Relative Policy Optimization), PPO of DPO, waarbij de beloning gebaseerd is op de correctheid van de symbolische uitkomst.

3. Belangrijkste Bijdragen

• Formeel Raamwerk: De introductie van een wiskundig onderbouwd raamwerk voor decompositie dat garanties biedt die heuristische methoden missen.
• Verifieerbare Operators: Het definiëren van decompositie-operatoren voor de ketting-, product- en somregel die bewezen de V1–V3 eigenschappen behouden.
• Algoritme voor Curriculum: Een methode om een foutloos leerpad te bouwen door recursieve decompositie-bomen te gebruiken.
• Empirische Validatie: Het aantonen dat het elimineren van ongeldige decomposities de nauwkeurigheid op de moeilijkste taken drastisch verhoogt.

4. Resultaten

De experimenten met Qwen3-modellen en DeepSeek-R1-distillaten laten indrukwekkende verbeteringen zien:

• Nauwkeurigheid: Op de moeilijkste problemen ($D_5$) verdubbelde de nauwkeurigheid van de baseline van 32% naar 68% (een relatieve verbetering van 112% voor het 1.5B model).
• Algoritme-prestaties: GRPO bleek superieur aan PPO en DPO voor deze specifieke taak, wat wijst op een stabielere optimalisatie bij groep-relatieve normalisatie.
• Ablatie-studies:
  • De volgorde van het curriculum (eenvoud $\to$ complexiteit) was de belangrijkste factor voor succes.
  • De verificatie-eigenschappen zijn cruciaal: het weglaten van V1 (eenvoud) zorgde voor de grootste daling in prestaties (-17.2 punten).
  • Complexe beloningsfuncties (zoals het belonen van de juiste regelidentificatie) boden slechts marginale winst vergeleken met de basisbeloning (correctheid + formaat).

5. Betekenis en Conclusie

De significantie van dit werk ligt in het verschuiven van "probabilistische" decompositie (gebaseerd op de gok van een LLM) naar "deterministische" decompositie (gebaseerd op formele logica).

VERIFY-RL bewijst dat:

1. Wiskundige precisie in de trainingsstructuur essentieel is om de ruis die inherent is aan LLM-generaties te elimineren.
2. Een strikt gecontroleerd curriculum de efficiëntie en de uiteindelijke redeneercapaciteit van kleine modellen (onder 3B parameters) enorm kan vergroten.
3. Dit principe van "verifieerbare decompositie" potentieel kan worden uitgebreid naar andere domeinen met formele regels, zoals algebra of logische bewijsvoering.