Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs

Titolo: Compile to Compress: Potenziamento dei Teoremi Formali tramite Output dei Compilatori

1. Il Problema

L'integrazione dei Large Language Models (LLM) nella dimostrazione automatica di teoremi (ATP) ha fatto passi da gigante, ma le prestazioni allo stato dell'arte richiedono spesso risorse computazionali proibitive durante la fase di test (test-time compute).

• Limitazioni attuali: I metodi esistenti si basano su estese esplorazioni (roll-out massicci) o finestre di contesto allungate per accumulare una storia di tentativi di prova.
• Il collo di bottiglia: I feedback dei compilatori (es. Lean 4) vengono spesso semplificati in indicatori binari (successo/fallimento) o messaggi di errore in testo semplice. Questo approccio ignora la ricca struttura informativa degli output dei compilatori, costringendo i modelli a dipendere da lunghe storie di interazione e limitando la profondità dell'esplorazione entro budget computazionali fissi.
• Obiettivo: Superare questo collo di bottiglia sfruttando la struttura intrinseca degli errori di compilazione per rendere l'esplorazione dello spazio delle prove più efficiente senza richiedere contesti storici infiniti.

2. Metodologia: "Compile to Compress"

Gli autori propongono un nuovo framework chiamato "Learning-to-Refine" (Imparare a Raffinare), basato sull'osservazione fondamentale che il compilatore agisce come un compressore di dimensioni.

• Il Compilatore come Compressore: Sebbene lo spazio dei programmi Lean sia combinatoriamente vasto, il compilatore mappa un'ampia varietà di tentativi di prova errati in un insieme compatto e strutturato di "modelli di fallimento" (failure modes). Molti programmi sintatticamente diversi generano lo stesso messaggio di errore, rivelando difetti semantici sottostanti comuni.
• Raffinamento Guidato dal Fallimento (Failure-Mode Driven Refinement): Invece di generare prove da zero, il modello impara a correggere localmente gli errori basandosi sul feedback esplicito del compilatore. Questo trasforma l'obiettivo di apprendimento da una generazione "alla cieca" a una correzione mirata.
• Catena di Distribuzioni (Chain of Distributions - CoD):
  • La generazione diretta campiona da una singola distribuzione fissa.
  • Il processo di raffinamento, invece, crea una catena di distribuzioni condizionate. Ogni passo di correzione dipende dallo stato corrente (prova fallita + messaggio di errore + problema), permettendo al modello di spostarsi dinamicamente verso regioni dello spazio delle prove che contengono soluzioni corrette, anche se inizialmente fuori distribuzione (OOD).
• Processo di Markov: Il framework tratta ogni passo di raffinamento come un processo decisionale di Markov, dipendente solo dallo stato attuale e non dall'intera storia passata. Questo riduce drasticamente la lunghezza del contesto necessaria.

3. Implementazione Tecnica

Il framework si articola in tre fasi principali:

1. Sintesi dei Dati "Cold-Start":

   • Viene creata una pipeline per generare dati di addestramento sintetici.
   • Si utilizzano modelli esterni (es. Claude-3.7-Sonnet) per analizzare gli errori di compilazione di soluzioni fallite e generare un "pensiero" (reasoning trace) che spiega come correggere l'errore, portando alla soluzione corretta.
   • I dati includono sia la generazione diretta che il raffinamento, bilanciati per l'addestramento.

2. Expert Iteration (Iterazione degli Esperti):

   • Una volta che il prover inizia a rifinire le prove, la distribuzione degli errori cambia.
   • Si esegue un'iterazione in cui il prover tenta di risolvere problemi, raffinando i propri fallimenti fino alla soluzione o all'esaurimento del budget.
   • Le traiettorie di successo vengono convertite in nuovi dati di supervisione per il raffinamento, permettendo al modello di adattarsi alle proprie distribuzioni di errore evolutive.

3. Strategia di Ricerca a Test-Time:

   • Il sistema modella l'auto-correzione come un problema di ricerca su un albero.
   • Ricerca Random: Bilancia casualmente tra nuove prove (BFS) e raffinamenti (DFS).
   • Ricerca Guidata dal Valore (Value-Guided Search): Viene addestrata una funzione di valore neurale per stimare il potenziale di successo di ogni nodo nell'albero di ricerca. Questa funzione guida l'esplorazione verso i rami più promettenti, ottimizzando l'allocazione del budget computazionale.

4. Risultati Sperimentali

Il metodo è stato valutato su prover di diverse dimensioni (Kimina-8B e Goedel-32B) su benchmark standard: MiniF2F, ProofNet, MathOlympiadBench e PutnamBench.

• Prestazioni Superiori: Il framework ha migliorato costantemente le capacità di ragionamento dei prover di base. Su PutnamBench, il metodo ha raggiunto prestazioni State-of-the-Art (SOTA) tra i modelli pubblici di dimensioni simili (~8B e ~32B parametri) con budget di test comparabili.
  • Esempio: Goedel-32B ha risolto 110 problemi su PutnamBench (vs 86 del modello originale Goedel-V2 e 91 di Ax-Prover).
  • Esempio: Kimina-8B ha risolto 25 problemi, posizionandosi primo nella sua categoria di dimensione.
• Efficienza: La strategia di ricerca guidata dal valore ha superato sia la ricerca random che la generazione diretta, dimostrando una maggiore efficienza nel trovare soluzioni corrette con meno campioni.
• Analisi delle Distribuzioni: Test statistici (Energy Distance) hanno confermato che le distribuzioni delle prove generate tramite raffinamento sono statisticamente distinte da quelle della generazione diretta, validando l'ipotesi della "Catena di Distribuzioni".
• Analisi degli Errori: Il raffinamento è più efficace per errori ricorrenti e strutturali (es. "unsolved goals", "type mismatch") rispetto a fallimenti semantici globali complessi.

5. Contributi Chiave

1. Nuova Prospettiva sul Feedback: Tratta l'output del compilatore non come un semplice segnale di errore, ma come una rappresentazione compressa e strutturata dello spazio delle prove fallite.
2. Framework Learning-to-Refine: Un approccio che internalizza la capacità di correzione degli errori, permettendo ai modelli di imparare strategie di riparazione generalizzabili basate sui modelli di fallimento.
3. Scalabilità: Il metodo è agnostico rispetto al modello e scala bene con le dimensioni del modello e il budget computazionale, offrendo un paradigma scalabile per il ragionamento guidato dal verificatore.
4. Riduzione del Contesto: Elimina la necessità di mantenere lunghe storie di interazione, riducendo i costi computazionali e permettendo un'esplorazione più profonda.

6. Significato e Impatto

Questo lavoro rappresenta un passo significativo verso prover formali più efficienti e scalabili. Dimostra che è possibile ottenere prestazioni di livello superiore senza ricorrere a modelli giganteschi o a costi di inferenza esponenziali, sfruttando invece la struttura logica intrinseca degli errori di compilazione.
Il framework offre una via d'uscita per superare i limiti attuali dei LLM nella dimostrazione di teoremi, trasformando il processo di "tentativo ed errore" in un percorso di raffinamento guidato e intelligente. Questo approccio è particolarmente promettente per l'integrazione in sistemi di ragionamento automatizzati di prossima generazione, dove l'efficienza e la precisione sono critiche.