Sintesi Tecnica: Miglioramento dell'Autoformalizzazione in Lean4 tramite Fine-tuning con Consistenza Ciclica

1. Il Problema

L'autoformalizzazione è il processo di traduzione automatica di testi matematici in linguaggio naturale (NL) in linguaggi di prova formale, come Lean4. Sebbene i grandi modelli linguistici (LLM) abbiano fatto progressi significativi nel ragionamento matematico, l'autoformalizzazione rimane una sfida critica: i modelli tendono a produrre codice Lean4 che è sintatticamente valido (compila correttamente) ma semanticamente errato, fallendo nel catturare il significato matematico inteso.

L'obiettivo di questo progetto è migliorare la fedeltà semantica della traduzione NL $\to$ Lean4, superando la semplice correttezza sintattica.

2. Metodologia

Il progetto propone un approccio sequenziale che combina Supervised Fine-Tuning (SFT) e Reinforcement Learning (RL), utilizzando un modello di base leggero e una metrica di valutazione innovativa.

Architettura del Modello

• Modello Base: Viene utilizzato Qwen3.5-2B (2 miliardi di parametri).
• Adattamento Efficiente: Si applica LoRA (Low-Rank Adaptation) limitando gli aggiornamenti ai sottolivelli Feed-Forward (FFN) del transformer, con un rank $r=16$ e $\alpha=32$. Questo porta a circa 9,4 milioni di parametri addestrabili su un totale di 2B, rendendo il training fattibile su una singola GPU.
• Pipeline a Due Fasi:
  1. Fase SFT: Addestramento iniziale su FineLeanCorpus (509k coppie NL/Lean4).
  2. Fase RL: Affinamento tramite GRPO (Group Relative Policy Optimization).

La Metrica di Consistenza Ciclica

Il cuore dell'innovazione risiede nella definizione di una funzione di ricompensa basata sulla consistenza ciclica:

1. Si addestra un modello $f_\theta$ per tradurre da NL a Lean4.
2. Si addestra un modello "back-translator" $g_\phi$ (fissato dopo la fase SFT) per tradurre da Lean4 a NL.
3. La ricompensa per una formalizzazione $\hat{l}$ di una frase $s$ è la similarità coseno tra l'embedding della frase originale $s$ e l'embedding della frase ricostruita $g_\phi(\hat{l})$:
   $$C_\theta(s) = \cos(e(s), e(g_\phi(f_\theta(s))))$$
   Dove $e(\cdot)$ è l'embedding prodotto dal modello all-MiniLM-L6-v2.
4. Questa metrica serve sia come segnale di ricompensa per il RL (GRPO) che come metrica di valutazione principale.

Strategie di Addestramento Confrontate

Il lavoro confronta tre regimi di addestramento:

1. SFT con Curriculum: Addestramento sequenziale ordinato per difficoltà (da 1 a 10).
2. SFT senza Curriculum: Addestramento sullo stesso dataset ma con ordine casuale (shuffled).
3. RL con GRPO: Fine-tuning del modello SFT (inizializzato dal curriculum) utilizzando la ricompensa di consistenza ciclica.

Dati e Decontaminazione

• Dataset di Training: FineLeanCorpus (FLC), filtrato per rimuovere duplicati, errori di compilazione e casi con alta similarità TF-IDF rispetto a PutnamBench (per evitare data leakage).
• Benchmark di Valutazione:
  • Un sottoinsieme tenuto da parte di FLC (700 problemi).
  • PutnamBench: 660 problemi di livello competizione (difficili, fuori distribuzione rispetto alla media di FLC).

3. Contributi Chiave

1. Pipeline di Fine-tuning: Implementazione end-to-end per l'autoformalizzazione Lean4 su Qwen3.5-2B con LoRA, includendo una rigorosa decontaminazione dei dati.
2. Studio Ablativo sul Curriculum: Dimostrazione che, a questa scala di modello (2B) e dimensione del dataset, l'ordinamento per difficoltà (curriculum learning) non offre benefici misurabili rispetto all'addestramento casuale.
3. RL con Ricompensa Semantica: Sviluppo di un metodo GRPO che utilizza la consistenza ciclica come segnale di ricompensa "soft". Questo approccio migliora significativamente la fedeltà semantica senza richiedere un compilatore Lean4 in tempo reale per ogni passo (che sarebbe troppo lento), evitando costi computazionali elevati.

4. Risultati Sperimentali

Performance Quantitativa

I risultati mostrano un miglioramento sostanziale del modello RL rispetto alle varianti SFT:

Modello	Mean Cycle Consistency (FLC)	Mean Cycle Consistency (PutnamBench)	Cross-Entropy Loss
Base 2B (Few-shot)	0.093	0.034	-
SFT No-Curriculum 2B	0.519	0.432	0.640
SFT Curriculum 2B	0.513	0.422	0.680
RL (GRPO) 2B	0.669	0.561	0.691
SFT Curriculum 9B	0.585	0.548	-

• Miglioramento RL: Il modello RL supera il SFT di circa 0.156 punti su FLC e 0.139 su PutnamBench.
• Impatto sulla Perplexity: L'aumento della Cross-Entropy loss è minimo (+0.011 nats), indicando che la capacità di modellazione linguistica di base non viene compromessa.
• Curriculum vs. Shuffled: Non vi è differenza statisticamente significativa tra SFT con e senza curriculum (p-value > 0.3), suggerendo che l'ordinamento della difficoltà non è cruciale per modelli di questa scala.
• Scala vs. RL: Un modello 9B addestrato solo con SFT (curriculum) performa meglio del 2B SFT, ma il 2B RL supera il 9B SFT su FLC, dimostrando che il segnale di ricompansa semantica è più efficace dell'aumento di scala in questo contesto specifico.

Analisi Qualitativa e Limiti

• Dominio Matematico: Il RL migliora costantemente su tutti i domini, ma il guadagno è maggiore per l'algebra e la teoria dei numeri rispetto all'analisi e al calcolo, dove la complessità strutturale del Lean4 rende la back-translation più rumorosa.
• Reward Hacking: È stato osservato che in alcuni casi (specialmente su FLC), il back-translator può "eco" letteralmente la frase originale se il codice Lean4 generato è molto simile al testo naturale, inflazionando artificialmente la ricompensa. Questo suggerisce che i risultati su PutnamBench (più diversificati) sono una stima più conservativa e affidabile.
• Fallimento del 9B: Il modello 9B, pur avendo più capacità, ha fallito nel seguire le istruzioni di output (generando ragionamento in NL invece di codice Lean4), evidenziando problemi di allineamento o di "modalità di pensiero" attiva non controllata.

5. Significato e Conclusioni

Questo lavoro dimostra che l'uso di Reinforcement Learning guidato da consistenza ciclica è una strategia superiore per l'autoformalizzazione rispetto al semplice SFT, anche su modelli di dimensioni ridotte (2B).

• Efficienza: Permette di ottenere prestazioni superiori a modelli più grandi (9B) senza il costo computazionale di training su scala massiccia.
• Robustezza Semantica: La metrica di consistenza ciclica agisce come un proxy efficace per la correttezza semantica, superando i limiti della sola validazione sintattica.
• Futuro: Il lavoro suggerisce che per migliorare ulteriormente l'autoformalizzazione, è necessario combinare segnali "soft" (come la consistenza ciclica) con feedback "hard" del compilatore Lean4 e sviluppare back-translator più robusti per evitare il reward hacking.

In sintesi, il progetto valida l'ipotesi che ottimizzare per la "fedeltà del viaggio di ritorno" (NL $\to$ Lean $\to$ NL) sia una via efficace per insegnare agli LLM a formalizzare la matematica in modo semanticamente corretto.