Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification

Hieronder volgt een gedetailleerde technische samenvatting van het paper "Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification", vertaald en samengevat in het Nederlands.

Titel: Goedel-Code-Prover: Hiërarchisch Bewijszoek voor Open State-of-the-Art Code Verificatie

1. Het Probleem

Grote Taalmodellen (LLMs) zijn uitstekend in het genereren van code die er plausibel uitziet, maar bieden beperkte garanties op correctheid. Formele verificatie, waarbij machine-controleerbare bewijzen worden geconstrueerd om te garanderen dat implementaties voldoen aan specificaties, is de oplossing. Echter, het automatiseren hiervan blijft een uitdaging, vooral in Lean 4.

De paper identificeert drie fundamentele problemen die bestaande methoden (die succesvol zijn in wiskundig bewijs) falen bij code-verificatie:

1. Ongegronde decompositie: In wiskunde kunnen LLMs gebaseerd op een rijke corpus van handgeschreven bewijzen zinnige subdoelen voorstellen. Voor code-verificatie bestaat dergelijk corpus niet; ontwikkelaars vertrouwen op testen in plaats van formele redenering. LLMs genereren daarom vaak subdoelen die semantisch ongeldig zijn of niet eenvoudiger dan het oorspronkelijke doel.
2. Concept-proliferatie: Elke nieuwe functie in een programma introduceert een unieke "conceptuele wereld" met nieuwe datatypen en invarianten. In tegenstelling tot wiskunde, waar bibliotheken zoals Mathlib herbruikbare lemmata bieden, moeten bij code-verificatie eigenschappen vaak van nul worden bewezen zonder bestaande ondersteuning.
3. Verschil in tactieken (Tactic distribution shift): Bewijzen voor code vereisen specifieke automatisering (zoals grind, SMT-ondersteunde lemma's en computationele reflectie native_decide) die sterk afwijken van de algebraïsche tactieken die in wiskundige bewijzen dominant zijn.

2. Methodologie

De auteurs stellen een hiërarchisch bewijszoekraamwerk voor dat de verificatie taak decomposeert in twee fasen, aangedreven door een uniek beleid (policy) genaamd Goedel-Code-Prover-8B.

A. Hiërarchische Architectuur
Het proces verloopt in twee fasen:

1. Fase 1: Recursieve Lemma-decompositie (Planning): Het verificatiedoel wordt recursief opgesplitst in structureel eenvoudigere sub-lemmata.
2. Fase 2: Lemma-voltooiing (Proving): De "blad-lemmata" (leaf lemmas) worden individueel bewezen door iteratief tactieken te genereren en te verfijnen op basis van feedback van de Lean 4-compiler.

B. De Decompositie Score (Kerninnovatie)
Om de kwaliteit van een decompositie te meten en te sturen, introduceren de auteurs een principiële decompositie score ($S$). Deze score fungeert zowel als beloning tijdens het trainen als als rangschikkingscriterium tijdens de inferentie. De score combineert twee dimensies:

• Constructieve rechtvaardiging (Constructive Justification): De voorgestelde lemmata moeten logisch het bovenliggende theorema impliceren. Dit wordt verifieerd via:
  • Proof reconstruction: Een bewijs dat de implicatie $(L_1 \land \dots \land L_k) \Rightarrow G$ toont.
  • Quickcheck: Automatische zoektocht naar contra-voorbeelden. Als een lemma een contra-voorbeeld heeft, wordt de hele decompositie verworpen.
• Structuur-effectiviteit (Structural Effectiveness): De decompositie moet de moeilijkheidsgraad verlagen. Dit wordt gemeten via de operator footprint ($d(\cdot)$), het aantal logische en domeinspecifieke operatoren in de Abstract Syntax Tree (AST). De score berekent de reductie in complexiteit tussen het oorspronkelijke doel en de zwaarste subdoel (gemeten via LogSumExp).

De formule is: $S = r \cdot v$, waarbij $v$ de validiteit is (binair) en $r$ de reductie in structuurcomplexiteit is.

C. Trainingspipeline: Hybrid Reinforcement Learning
Om een enkel model te trainen dat zowel decomposeert als bewijst, gebruiken ze een hybride aanpak om het probleem van "reward mismatch" op te lossen (decompositie heeft een continue score, bewijzen heeft een binair succes/falen signaal):

1. Supervised Fine-Tuning (SFT): Initiatie met gescaffoldeerde data van state-of-the-art modellen (GPT-5.2, Gemini-3-Flash) voor zowel decompositie als voltooiing.
2. Hybride Reinforcement Learning (RL):
   • Decompositie: Geoptimaliseerd via Group Relative Policy Optimization (GRPO) met de continue decompositie-score als beloning. Dit drijft de exploratie van betere decomposities.
   • Voltooiing: Gestabiliseerd via supervised replay van hoogwaardige bewijstrajecten, zodat het model niet afhankelijk wordt van het schaarse binair signaal van succes/falen.

3. Belangrijkste Resultaten

Het model werd geëvalueerd op drie Lean 4 benchmarks (Verina, Clever, AlgoVeri), totaal 427 taken.

• Prestatie: Goedel-Code-Prover-8B bereikte een 62,0% succesrate in het leveren van volledige, geverifieerde bewijzen.
• Vergelijking: Dit is een 2,6x verbetering ten opzichte van de sterkste bestaande baseline.
• Efficiëntie: Het 8B-parameter model overtreft neurale bewijzers die tot 84x groter zijn (zoals DeepSeek-Prover-V2-671B).
• Inferentie-schaalbaarheid: De succesrate neemt monotoon toe met meer zoekiteraties en een grotere steekproefbudget (pass@k), wat aangeeft dat het model nog niet verzadigd is.
• Kwaliteit van bewijzen: De gegenereerde bewijzen zijn complex, met gemiddeld 8-17 gedefragmenteerde lemmata en meer dan 130 regels bewijscode per taak.

4. Bijdragen

1. Hiërarchisch raamwerk: Een nieuw systeem voor Lean 4 dat complexe verificatiedoelen eerst structureel decomposeert voordat tactieken worden toegepast.
2. Principiële score: Een nieuwe metriek die constructieve geldigheid en structurele eenvoud combineert, gebruikt als zowel trainingsbeloning als inferentie-rangschikking.
3. Hybride RL-pijplijn: Een trainingsstrategie die de spanning tussen continue decompositie-beloningen en binair bewijs-falen oplost door GRPO en supervised replay te combineren.
4. Empirisch bewijs: Uitgebreide evaluatie die aantoont dat een doelgericht getraind klein model (8B) superieur is aan veel grotere, generieke modellen voor code-verificatie.

5. Betekenis en Impact

Dit werk is significant omdat het de kloof overbrugt tussen "code die er goed uitziet" en "code die formeel bewezen correct is". Het toont aan dat:

• De succesvolle methoden uit wiskundig bewijs niet direct toepasbaar zijn op code zonder aanpassing voor de unieke aard van software (concept-proliferatie en gebrek aan lemma-bibliotheken).
• Een planning-laag (decompositie) essentieel is voor complexe verificatietaken.
• Een klein, gespecialiseerd model (8B parameters) effectiever kan zijn dan enorme modellen als het correct is getraind op de specifieke structuur van het probleem (decompositie + voltooiing).

De paper legt de basis voor toekomstige systemen die veiligheidskritieke software kunnen verifiëren door LLMs te gebruiken om niet alleen code te schrijven, maar ook de complexe logische bewijzen te construeren die nodig zijn om die code te garanderen.