Technische Samenvatting: Diversiteit op het Moment van Inference bij RL-getrainde Lean Theorema-proevers

Probleemstelling

Recente neurale theorema-proevers, met name die getraind met Reinforcement Learning (RL) en verifieerbare beloningen (RLVR), hebben sterke prestaties behaald op formele bewijsbenchmarks zoals miniF2F. De heersende aanname is dat voldoende RL-training en meer rekenkracht op het moment van inference (via i.i.d. sampling) modellen in staat stellen om de structurele prioren die nodig zijn voor formele bewijzen te internaliseren.

Dit artikel daagt die aanname uit en diagnosticeert een fenomeen van mode collapse op het moment van inference bij RL-getrainde Lean-proevers. Specifiek observeren de auteurs dat het verhogen van het sampling-budget ($k$) veel eerder dan verwacht afnemende meeropbrengsten oplevert. Op de miniF2F-test-benchmark met DeepSeek-Prover-V1.5-RL levert het verdubbelen van het sampling-budget van $k=32$ naar $k=64$ geen enkele extra opgeloste stelling op (stuck at 42/244). Het model convergeert naar een smal scala aan bewijsstrategieën en faalt in het verkennen van alternatieven, zelfs wanneer extra stochastische samples worden aangeboden.

Methodologie

De studie hanteert een gecontroleerd diagnostisch raamwerk met DeepSeek-Prover-V1.5-RL en zijn niet-RL basisvariant, naast cross-model vergelijkingen met DeepSeek-Prover-V2-7B (RL) en Goedel-Prover (alleen SFT).

1. De Interventie van het Skelet-schema

Om te testen of het plateau te wijten is aan een gebrek aan structurele diversiteit in plaats van een gebrek aan rekenkracht, introduceren de auteurs een vast, deterministisch schema van 15 tactic-skeletten.

• Structuur: Een $15 \times 8 = 120$ rooster dat 15 handgeselecteerde Lean tactic-skeletten (bijv. simp, intro, constructor, aesop) combineert met 8 goal-hint-commentaren (natuurtaalsuggesties).
• Uitvoering: Voor een budget $k$ probeert het model de eerste $k$ invoeren van dit rooster. Dit dwingt het model om bewijzen te starten met specifieke strategische openingen in plaats van te vertrouwen op willekeurige sampling.
• Ablaties: Om de bron van verbetering te isoleren, vergelijken de auteurs:
  • B-RL (Skelet): Het gestructureerde schema van 15 skeletten.
  • C1 (Parafraase): 16 semantisch equivalente instructieparafraases (geen tactic-structuur).
  • C2 (Irrelevante Commentaren): 16 inhoudsloze Lean-commentaren.
  • C3 (Alleen NL): Een specifieke conditie die uitsluitend natuurtaalhints gebruikt zonder tactic-voorvoegsels.

2. Stratificatie van Moeilijkheid

De auteurs definiëren een empirische formalisatie-moeilijkheidsscore ($\sigma$) met behulp van een leave-one-out constructie. Voor een doelstelling telt $\sigma$ hoeveel andere basismodellen (Goedel-Prover, V2-7B) deze oplossen zonder interventie. Dit stratificeert stellingen in buckets: Frontier (onopgelost door anderen), Hard, Medium, Easy en Trivial.

3. Directe Distributie-meting

Om voorbij gedragsplateaus te gaan, analyseren de auteurs de diversiteit van de eerste tactic-head over 13.159 stochastische samples. Ze tellen het aantal verschillende leidende tactic-identificatoren (bijv. have, rw, norm_num) die per stelling worden gegenereerd.

Belangrijkste Resultaten

1. Het Plateau Doorbreken via Structurele Gidsing

• Basis-Collapse: DeepSeek-Prover-V1.5-RL met i.i.d. sampling lost 38 stellingen op bij $k=16$, 42 bij $k=32$, en blijft steken op 42 bij $k=64$.
• Effectiviteit van Skeletten: Het vaste skelet-schema doorbreekt dit plateau en lost 55 stellingen op bij $k=16$ (+45% relatieve verbetering) en blijft nieuwe bewijzen vinden tot $k=64$ (60 in totaal).
• Ablatiebevindingen:
  • Structuur vs. Diversiteit: Instructieparafraases (C1) leveren dezelfde pass@16 op als de basis (38/244), terwijl irrelevante commentaren (C2) de prestaties degraderen tot 25/244. Dit bevestigt dat winst wordt gedreven door structurele gidsing, niet door lichte prompt-diversiteit.
  • NL vs. Tactics: De alleen-NL conditie (C3) lost 48/244 op, tussen de basis en de volledige skeletten in. Dit geeft aan dat natuurtaalhints ongeveer 58% van het gat dichten, terwijl letterlijke tactic-voorvoegsels het resterende deel bijdragen.

2. Lokalisatie van de Winst

De structurele winst is geconcentreerd in de Easy en Trivial buckets (stellingen die oplosbaar zijn door andere open-source provers maar gemist worden door de i.i.d. sampling van V1.5-RL).

• In de gecombineerde Easy+Trivial kolom levert de skelet-interventie een nettowinst op van +15, terwijl parafraases 0 opleveren en irrelevante commentaren -14.
• Geen enkele verstoring opent de "Frontier" bucket (stellingen die door geen enkel basismodel worden opgelost), wat suggereert dat de interventie onderverkenning van bekende oplosbare problemen verhelpt in plaats van de grens van capaciteit uitbreidt.

3. RL-specifiekheid van Mode Collapse

• Contrast met Basismodel: DeepSeek-Prover-V1.5-Base (niet-RL) lost geen enkele stelling op onder welke conditie dan ook (i.i.d. of skeletten). Dit stelt vast dat RL de locus is van zowel bewijscapaciteit als de daaropvolgende mode collapse. Het basismodel mist de capaciteit om geldige bewijzen te genereren; de RL-fase creëert die capaciteit maar collapseert deze naar een smal beleid.
• Cross-model Contrast:
  • V2-7B (RL): Toont een vlakke aggregatiewinst (+1) maar opent +3 frontier-stellingen die ontoegankelijk zijn voor elke i.i.d. basis.
  • Goedel-Prover (SFT): Toont een negatieve winst (-10,0 $\pm$ 4,4) met skeletten. SFT-getrainde modellen lijken al een breed scala aan tactic-stammen te verkennen, waardoor het vaste skelet-schema overbodig of beperkend is.

4. Direct Bewijs van Collapse

Distributie-analyse onthult dat de mediaan-stelling slechts 2 verschillende eerste tactic-heads ontvangt over 64 samples, met 49% van de benchmark die een deterministische enkele strategische opening ontvangt. De waargenomen Shannon-entropie is $\le 8\%$ van de theoretische capaciteit, wat ernstige mode collapse bevestigt.

Betekenis en Claims

Het artikel herformuleert het verhaal van "tactic-skeletten verbeteren prestaties" naar "RL-getrainde provers de tactic-ruimte op het moment van inference ernstig onderverkennen."

• RL als Dubbel Agent: De auteurs claimen dat RL een dubbele rol speelt: het is de fase die bewijscapaciteit creëert (aangezien het basismodel er geen heeft) en tegelijkertijd de fase die die capaciteit collapseert naar een smal beleid.
• Scaling op het Moment van Inference: De resultaten suggereren dat het simpelweg schalen van inference-rekenkracht via i.i.d. sampling veel eerder afnemende meeropbrengsten heeft dan aangenomen. Structurele diversiteit (variatie in bewijsstrategieën via prompts) is een efficiëntere as voor scaling.
• Herstelbaarheid: De mode collapse is specifiek voor RL-getrainde modellen. SFT-getrainde modellen vertonen niet hetzelfde herstelbare collapse via structurele hints; in feite lijden ze hieronder. Dit impliceert dat toekomstige interventies (entropy-regulatie tijdens training of skelet-retrieval tijdens inference) de afweging moeten navigeren tussen het creëren van capaciteit en het behouden van diversiteit.

De studie concludeert dat "mode collapse" een reëel, pipeline-afhankelijk fenomeen is dat inherent is aan het RL-finetuningproces in domeinen van formele verificatie, en dat vaste structurele interventies het verloren onderzoek effectief kunnen herstellen zonder aanvullende training.