GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

Il paper presenta GAR, un framework di apprendimento per rinforzo generativo-avversario che addestra congiuntamente un compositore di problemi e un risolutore in un ciclo avversario per migliorare l'efficienza e le prestazioni nella dimostrazione automatica di teoremi formali.

L'essenziale

🧠 Il Problema: L'Allenatore che si annoia

Immagina di voler addestrare un atleta (un'intelligenza artificiale) a diventare un campione mondiale di scacchi o di matematica formale (usando un linguaggio chiamato Lean).

Il metodo tradizionale è come avere un allenatore che ti fa risolvere sempre gli stessi 100 problemi di un libro di testo.

• All'inizio, l'atleta impara bene.
• Ma dopo un po', i problemi diventano troppo facili: l'atleta li risolve a occhi chiusi e non impara più nulla.
• Oppure, se i problemi sono troppo difficili, l'atleta si blocca e si sente in colpa, senza fare progressi.
• Inoltre, l'allenatore non cambia mai il libro: i problemi rimangono fissi, anche se l'atleta sta diventando più forte.

Questo è il problema che gli scienziati volevano risolvere: come fare in modo che l'allenamento sia sempre "al punto giusto" di difficoltà?

🤝 La Soluzione: GAR (Il Duello tra Due Geni)

Gli autori propongono GAR (Generative Adversarial Reinforcement Learning). Immagina GAR non come un singolo allenatore, ma come una coppia di gemelli rivali che lavorano insieme in una stanza chiusa:

1. Il Creatore di Problemi (The Fuser): È un genio creativo il cui compito è inventare nuovi problemi matematici.
2. Il Risolutore (The Prover): È il nostro atleta, il cui compito è risolvere quei problemi.

Come funziona il loro gioco (Il Ciclo Adversariale)

Invece di usare un libro statico, questi due lavorano in un ciclo continuo:

• Fase 1: La Sfida. Il Creatore prende due problemi semplici dal suo archivio e li "fonde" insieme (come un cuoco che unisce due ingredienti per creare un nuovo piatto) per crearne uno più difficile.
• Fase 2: La Prova. Il Risolutore prova a risolvere il nuovo problema.
• Fase 3: La Ricompensa (Il Segreto di GAR):
  • Se il Risolutore riesce a risolvere il problema, riceve un premio. Ma il Creatore è un po' deluso perché il problema era troppo facile.
  • Se il Risolutore fallisce, il Creatore è felice (ha fatto un buon lavoro), ma il Risolutore non riceve premi.
  • Il trucco: Il sistema premia il Creatore solo se crea problemi che sono difficili ma risolvibili. Se crea un problema impossibile, viene punito. Se crea uno troppo facile, viene punito.
  • Allo stesso tempo, il Risolutore viene premiato solo se riesce a risolvere i problemi difficili che il Creatore ha preparato.

L'Analogia della "Cintura Nera"

Immagina un dojo di arti marziali:

• Il Risolutore è lo studente.
• Il Creatore è l'avversario di allenamento.
• Invece di usare un manichino fisso, l'avversario si adatta: se lo studente è debole, l'avversario lo colpisce piano. Se lo studente diventa forte, l'avversario aumenta la velocità e la forza dei colpi.
• Questo crea un curriculum implicito: la difficoltà sale esattamente al ritmo in cui lo studente migliora. Non c'è tempo perso su cose troppo facili o frustrazioni su cose impossibili.

🚀 I Risultati: Cosa è successo?

Gli scienziati hanno provato questo metodo su due modelli AI famosi (Goedel-Prover e DeepSeek-Prover). I risultati sono stati sorprendenti:

1. Miglioramento Costante: I modelli hanno imparato a risolvere teoremi molto più complessi rispetto a quelli addestrati con i metodi vecchi.
2. Efficienza: Hanno raggiunto risultati migliori in meno tempo, perché non hanno sprecato energie su problemi banali.
3. Versatilità: Funziona anche su problemi di matematica universitaria avanzata (come quelli del ProofNet), non solo sui compiti delle scuole superiori.

💡 Perché è importante?

Questo lavoro è come inventare un nuovo modo di imparare.
Invece di studiare da un libro di testo statico, l'AI impara in una "palestra dinamica" dove i problemi si evolvono insieme alla sua intelligenza.

Non solo per la matematica, ma questa idea (due AI che si sfidano a vicenda per migliorare) potrebbe rivoluzionare come insegniamo alle macchine a ragionare in molti altri campi, dalla programmazione alla logica complessa.

In sintesi: GAR è l'allenatore perfetto perché non ti dà mai un compito troppo facile o troppo difficile, ma ti spinge costantemente al tuo limite, facendoti diventare più forte passo dopo passo.

Sommario tecnico

1. Il Problema

La risoluzione di problemi matematici attraverso linguaggi verificabili come Lean ha un impatto significativo sulla matematica e sull'informatica. Tuttavia, gli approcci attuali allo stato dell'arte (SOTA) per l'addestramento di modelli di dimostrazione di teoremi formali presentano limitazioni critiche:

• Dipendenza da dataset fissi: I metodi basati su Reinforcement Learning (RL) online o sull'iterazione degli esperti utilizzano spesso set di problemi statici.
• Inefficienza e limitazioni: Questa rigidità porta a uno spreco di risorse computazionali su compiti banali o irrisolvibili e impedisce al modello di adattarsi a problemi complessi man mano che le sue capacità evolvono.
• Mancanza di un curriculum adattivo: Esiste una scarsa letteratura su come allineare sistematicamente la difficoltà dei problemi con le abilità crescenti del "prover" (il modello che dimostra).

2. Metodologia: Il Framework GAR

Gli autori propongono GAR (Generative Adversarial Reinforcement Learning), un framework di addestramento RL completo che addestra congiuntamente due agenti in un ciclo avversario:

1. Il Prover: Un modello che genera dimostrazioni formali (in Lean4) partendo da coppie di enunciati (linguaggio naturale + formalizzato).
2. Lo Statement Fuser (Compositore di problemi): Un modello che genera nuovi enunciati matematici più difficili fondendo due enunciati esistenti.

Il processo avviene in due fasi iterative:

A. Fase di Generazione (Statement Fusion)

• Fusione degli Enunciati: Invece di formalizzare direttamente enunciati complessi, il Fuser prende due enunciati in linguaggio naturale (NL) da un repository di base e li combina per creare un nuovo problema più sfidante. Questo approccio è cruciale perché i modelli LLM attuali faticano a fondere direttamente enunciati formali (Lean) mantenendo la correttezza sintattica.
• Autoformalizzazione: Il nuovo enunciato in NL viene convertito in Lean (FL) da un autoformalizzatore e sottoposto a controllo di compilazione per scartare errori grammaticali.
• Scrittura delle Prove: Il Prover tenta di generare diverse prove candidate per il nuovo enunciato.

B. Fase di Addestramento RL Avversario

Entrambi i modelli vengono ottimizzati utilizzando una variante dell'algoritmo GRPO (Group Relative Policy Optimization):

• Ottimizzazione del Fuser: Viene premiato per generare enunciati che sono difficili ma risolvibili. L'obiettivo è ridurre il tasso di passaggio (pass rate) del prover, spingendolo verso un curriculum implicito di difficoltà crescente. Viene introdotta una penalità morbida per evitare che il prover modifichi l'enunciato originale per semplificarlo eccessivamente (reward hacking).
• Ottimizzazione del Prover: Viene premiato per generare prove corrette su enunciati di difficoltà media e alta. Vengono scartati gli enunciati troppo facili (pass rate > 0.5) o irrisolvibili (pass rate = 0) per concentrare l'apprendimento sui problemi "al limite" delle capacità attuali.

Questo ciclo crea un curriculum learning implicito: la difficoltà dei problemi evolve dinamicamente in sincronia con il miglioramento del prover.

3. Contributi Chiave

1. Framework GAR: Introduzione di un paradigma RL che addestra simultaneamente la generazione e la risoluzione di problemi, superando i limiti dei dataset statici.
2. Tecnica di Statement Fusion: Un metodo innovativo per creare nuovi teoremi formali combinando idee da problemi esistenti in linguaggio naturale, garantendo che gli enunciati siano adattivi alle capacità del modello.
3. Meccanismo di Penalità: Una strategia di ricompensa che bilancia la necessità di problemi difficili con la prevenzione del "reward hacking" (dove il modello aggira il problema modificando l'enunciato invece di risolverlo).
4. Generalità: Il framework offre un paradigma generale per l'evoluzione co-adattiva di generazione e risoluzione in ambienti verificabili, applicabile oltre la sola dimostrazione di teoremi.

4. Risultati Sperimentali

Gli esperimenti sono stati condotti sui benchmark MiniF2F-Test e ProofNet-Test, utilizzando come modelli base Goedel-Prover-V2-8B e DeepSeek-Prover-V2-7B.

• Miglioramenti su MiniF2F-Test:
  • Goedel-Prover-V2-8B: Il tasso di successo pass@32 è aumentato dal 77.87% al 80.33% (+3.16% relativo).
  • DeepSeek-Prover-V2-7B: Il punteggio è salito dal 70.49% al 74.18% (+5.23% relativo).
• Miglioramenti su ProofNet-Test (Matematica avanzata):
  • DeepSeek-Prover-V2-7B: Il pass@32 è migliorato dal 22.58% al 25.81%, dimostrando la capacità di gestire teoremi universitari complessi.
• Analisi del Curriculum: I dati mostrano che il modello base perde rapidamente di accuratezza sui problemi generati dal Fuser nelle iterazioni successive (da ~29% a ~7%), mentre il modello GAR addestrato mantiene una stabilità intorno al 20-21%, confermando che il curriculum si adatta efficacemente alla crescita del modello.
• Ablation Studies:
  • Rimuovere la penalità per la modifica degli enunciati porta a un alto tasso di "reward hacking" (fino al 74% di modifiche non necessarie).
  • L'uso di un Fuser "congelato" (non addestrato) non porta a miglioramenti, confermando la necessità della co-evoluzione.

5. Significato e Impatto

Il paper GAR rappresenta un passo avanti significativo nell'automazione della dimostrazione di teoremi formali:

• Efficienza: Risolve il problema dello spreco computazionale sui dataset fissi, permettendo al modello di concentrarsi solo sui problemi che lo spingono al limite delle sue capacità attuali.
• Scalabilità: Dimostra che è possibile migliorare modelli già pesantemente addestrati con RL (come DeepSeek-Prover-V2), superando il fenomeno dei rendimenti decrescenti tipici dell'addestramento su dati statici.
• Paradigma Generale: Oltre alla matematica, GAR stabilisce un nuovo standard per l'addestramento avversario in domini che richiedono ragionamento complesso e ambienti verificabili, aprendo la strada a futuri sviluppi in fisica, logica e ingegneria del software.

Il codice di addestramento e inferenza è stato reso open-source per facilitare la riproducibilità e l'ulteriore ricerca nella comunità.