Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning

Titel: Verbetering van Lean4 Autoformalisatie via Cycle Consistency Fine-tuning

Auteur: Arsen Shebzukhov (Stanford University, CS224N Project)
Doel: Het automatiseren van de vertaling van natuurlijke wiskundige taal (NL) naar formele bewijs-taal (Lean4) met behulp van Large Language Models (LLM's).

---

1. Probleemstelling

Autoformalisatie is het proces waarbij natuurlijke wiskundige teksten automatisch worden vertaald naar formele code (zoals Lean4) die door een bewijsassistent kan worden geverifieerd. Hoewel LLM's grote vooruitgang hebben geboekt in redeneren, blijft autoformalisatie moeilijk. Modellen genereren vaak code die syntactisch correct is (compilatie lukt), maar semantisch onjuist is (het vat de bedoelde wiskundige betekenis niet correct).

De uitdaging is om modellen te trainen die niet alleen correcte syntaxis produceren, maar ook de semantische betekenis van de oorspronkelijke stelling behouden.

2. Methodologie

De auteur gebruikt een Qwen3.5-2B model en past LoRA (Low-Rank Adaptation) toe om de training efficiënt te houden (slechts ~9,4M trainbare parameters). De aanpak bestaat uit drie fasen:

A. Data en Voorbewerking

• Dataset: Gebruik van FineLeanCorpus (509k NL/Lean4-paren) met moeilijkheidsgraden (1-10).
• Decontaminatie: Strikte filtering om te voorkomen dat het model PutnamBench (660 competitieproblemen) tijdens het trainen heeft gezien.
• Splitsing: De data wordt gesplitst in training (SFT), validatie, en een vastgehouden evaluatieset.

B. Training Regimes

Het paper vergelijkt drie trainingstrategieën:

1. Supervised Fine-Tuning (SFT) met Curriculum Learning: Training verloopt sequentieel van makkelijk (niveau 1) naar moeilijk (niveau 10).
2. SFT zonder Curriculum: Training op dezelfde data, maar volledig gemengd (shuffled).
3. Reinforcement Learning (RL) met GRPO:
   • Algoritme: Group Relative Policy Optimization (GRPO), dat geen apart critic-model vereist door beloningen binnen een groep van samples te normaliseren.
   • Reward Mechanisme (Cycle Consistency): Dit is de kerninnovatie.
     • Een model $f$ vertaalt Natural Language (NL) $\to$ Lean4.
     • Een vast (frozen) back-translator model $g$ vertaalt Lean4 $\to$ NL'.
     • De beloning is de cosine similarity tussen de originele zin $s$ en de terugvertaalde zin $NL'$ (gebruikmakend van all-MiniLM-L6-v2 embeddings).
     • Formule: $r = \cos(e(s), e(g(f(s))))$.
   • Het idee is dat een goede formalisatie de betekenis moet behouden in een "NL $\to$ Lean4 $\to$ NL" lus.

C. Evaluatie

• Hoofdmeter: Gemiddelde Cycle Consistency Score ($\bar{C}$).
• Secundaire meter: Cross-entropy verlies (om te controleren of de taalvaardigheid niet verslechtert).
• Datasets: Een vastgehouden subset van FineLeanCorpus en PutnamBench.

---

3. Belangrijkste Bijdragen

1. Pipeline voor Autoformalisatie: Een volledig geïmplementeerde fine-tuning pipeline voor Qwen3.5-2B met LoRA, inclusief data-decontaminatie voor PutnamBench.
2. Ablatiestudie Curriculum Learning: Het paper toont aan dat voor dit modelformaat (2B parameters) en datasetgrootte, het sequentieel trainen op moeilijkheidsgraden (curriculum) geen meetbaar voordeel biedt ten opzichte van willekeurige training.
3. RL met Cycle Consistency: De introductie van GRPO met een cycle-consistency reward. Dit resulteert in een aanzienlijke verbetering in semantische nauwkeurigheid zonder de basis-taalvaardigheid (cross-entropy) significant te schaden.

---

4. Resultaten

De resultaten tonen aan dat RL de SFT-baselines aanzienlijk overtreft:

Model	FLC (Held-out) $\bar{C}$	PutnamBench $\bar{C}$	Cross-Entropy Loss
Base 2B (Few-shot)	0.093	0.034	-
SFT (Geen Curriculum)	0.519	0.432	0.640
SFT (Curriculum)	0.513	0.422	0.680
RL (GRPO)	0.669	0.561	0.691

• Verbetering: RL verbetert de cycle consistency met 0.156 op FLC en 0.139 op PutnamBench ten opzichte van de SFT-curriculum baseline.
• Statistiek: De verbetering is statistisch significant ($p < 10^{-56}$).
• Curriculum vs. Shuffled: Er is geen significant verschil tussen SFT met en zonder curriculum (p-waarden > 0.3), wat suggereert dat curriculum learning bij dit modelformaat geen meerwaarde heeft.
• Schaling: Een groter model (9B) presteert beter dan het kleine model (2B) met SFT, maar het kleine model (2B) met RL presteert zelfs beter dan het grote model (9B) met alleen SFT op de in-distribution data (FLC).

Analyse per Domein:

• Discrete wiskunde (getaltheorie, algebra) profiteert het meest van RL.
• Continue wiskunde (calculus, analyse) scoort lager, waarschijnlijk omdat de terugvertaling (back-translation) van complexe $\epsilon-\delta$ definities en limieten "ruis" introduceert, wat de reward-signalen minder informatief maakt.

---

5. Betekenis en Conclusie

• Semantische Fidelity: De studie bewijst dat cycle consistency een effectieve, zij het imperfecte, proxy is voor het trainen van modellen om de betekenis van wiskundige stellingen te behouden, niet alleen de syntaxis.
• Efficiëntie: Het is mogelijk om met een relatief klein model (2B parameters) en LoRA, via RL, prestaties te bereiken die dicht in de buurt komen van of zelfs grotere modellen (9B) met alleen SFT overtreffen.
• Beperkingen:
  • De cycle consistency-maatstaf kan "reward hacking" toelaten (bijvoorbeeld als het back-translator-model de originele zin letterlijk teruggeeft zonder de Lean4-code echt te begrijpen).
  • Het gebruik van sorry in de gegenereerde theorema's betekent dat syntactische correctheid niet gelijkstaat aan wiskundige waarheid.
• Toekomst: De volgende stap is het combineren van deze "soft" cycle-consistency reward met "harde" feedback van de Lean4 compiler om zowel semantische als syntactische correctheid te garanderen.

Kortom, dit paper demonstreert dat Reinforcement Learning met een cycle-consistency doelwit een krachtige methode is om de kwaliteit van autoformalisatie te verhogen, zelfs zonder enorme rekenkracht of enorme modelgroottes.