DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent

1. Enunciato del Problema

La dimostrazione automatica di teoremi (ATP) ha fatto progressi significativi grazie ai Large Language Models (LLM) e agli assistenti di prova formale come Lean. Tuttavia, i sistemi attuali all'avanguardia affrontano due limitazioni critiche:

• Mancanza di Generalizzazione: La maggior parte degli approcci tratta ogni teorema in isolamento. Sebbene possano decomporre i problemi in passaggi intermedi, questi passaggi sono spesso altamente specifici per il singolo problema e non si generalizzano attraverso teoremi diversi.
• Inefficienza: I metodi esistenti si affidano o a librerie di lemmi fisse e statiche (limitando l'adattabilità) o sintetizzano nuovi lemmi intermedi per ogni singola istanza di problema. Ciò porta a calcoli ridondanti, lunghezze di prova maggiori e un maggiore utilizzo di token, poiché il sistema non riesce ad accumulare e riutilizzare le "abilità" (lemmi) apprese dalle prove precedenti.

Il paper sostiene che i sistemi attuali non riescono a imitare la pratica matematica umana, dove i matematici accumulano sistematicamente, astraggono e riutilizzano un insieme fondamentale di lemmi trasferibili per risolvere nuovi problemi in modo efficiente.

2. Metodologia: Il Framework DreamProver

DreamProver è un framework agenziale progettato per apprendere ed evolvere una libreria riutilizzabile di lemmi attraverso un paradigma iterativo "Wake-Sleep" (Veglia-Sonno), ispirato alle teorie dell'apprendimento cognitivo e all'algoritmo DreamCoder. Il sistema opera in cicli alternati:

A. La Fase di Veglia (Scoperta e Decomposizione dei Teoremi)

In questa fase, l'agente tenta di dimostrare teoremi da un set di addestramento utilizzando la libreria di lemmi corrente.

• Identificazione di Teoremi Apprendibili: Il sistema tenta di dimostrare i teoremi direttamente utilizzando la libreria. Se ha successo, il teorema viene contrassegnato come "apprendibile", implicando che la libreria è sufficiente per quel dominio.
• Scoperta di Teoremi Intermedi: Se un teorema non può essere dimostrato direttamente, il sistema lo decompone ricorsivamente in sottoproblemi più semplici (sottoteoremi).
  • Genera una bozza formale di prova.
  • Estrae gli obiettivi intermedi non dimostrati (segnalati da sorry) come teoremi autonomi.
  • Convalida questi teoremi estratti tentando di riassemblare la prova completa utilizzando la bozza e i nuovi candidati.
• Risultato: Il sistema accumula un insieme di "teoremi apprendibili" (risultati intermedi) derivati dai dati di addestramento.

B. La Fase di Sonno (Astrazione dei Lemmi e Ottimizzazione della Libreria)

In questa fase, il sistema elabora le esperienze accumulate per evolvere la libreria di lemmi.

• Clustering Semantico: Il sistema annota i teoremi intermedi raccolti con descrizioni in linguaggio naturale (sottodominio, difficoltà, concetti rilevanti). Successivamente, incorpora queste descrizioni e le raggruppa utilizzando K-Means basato sulla similarità semantica.
• Astrazione dei Lemmi: Per ogni cluster, un LLM viene sollecitato a generare un lemma candidato che generalizzi i teoremi specifici in quel cluster.
• Convalida Strutturale: Per garantire che i lemmi astratti siano applicabili, il sistema calcola la similarità strutturale (utilizzando la distanza di modifica degli alberi sugli alberi di espressione logica del primo ordine) tra il lemma candidato e i teoremi nel cluster. I lemmi che superano una soglia di similarità vengono mantenuti.
• Aggiornamento della Libreria (Dimenticanza e Duplicazione):
  • Deduplicazione: I nuovi lemmi vengono confrontati con la libreria esistente utilizzando la distanza di modifica degli alberi; i lemmi altamente simili (duplicati) vengono scartati.
  • Dimenticanza: Per mantenere una libreria compatta, il sistema impiega una strategia "Least Recently Used" (LRU, meno recentemente usato). I lemmi che non sono stati utilizzati frequentemente nelle recenti fasi di veglia vengono eliminati una volta che la libreria raggiunge la capacità massima.
  • Verifica: I lemmi candidati rimanenti vengono formalmente verificati per garantire che siano dimostrabili.

C. Inferenza

Durante l'inferenza su problemi di test non visti, DreamProver utilizza la libreria evoluta. Tenta prima la generazione diretta della prova. Se ciò fallisce, impiega un flusso di lavoro "Sketch-and-Prove" (Bozza e Prova), utilizzando la libreria per guidare la generazione delle bozze di prova e la risoluzione dei sottobiettivi.

3. Contributi Chiave

1. Paradigma Wake-Sleep per l'ATP: La prima applicazione di un ciclo continuo e iterativo veglia-sonno specificamente per l'evoluzione di librerie di lemmi trasferibili nella dimostrazione formale di teoremi.
2. Apprendimento di Lemmi Trasferibili: A differenza di lavori precedenti (ad esempio LEGO-Prover) che faticavano a dimostrare un riutilizzo efficace, DreamProver raggruppa e astrae esplicitamente i risultati intermedi in lemmi generali, creando una base di conoscenza persistente e di alta qualità.
3. Meccanismi di Efficienza: L'introduzione di un meccanismo di "dimenticanza" (potatura LRU) e della deduplicazione strutturale garantisce che la libreria rimanga compatta (<100 lemmi), prevenendo l'overflow della finestra di contesto e mantenendo un'elevata pertinenza nel recupero.
4. Generalizzazione del Dominio: Il framework è progettato per funzionare attraverso diversi domini matematici, inclusi quelli sottorappresentati nei dati di addestramento degli LLM.

4. Risultati Sperimentali

Gli autori hanno valutato DreamProver su cinque domini matematici: Disuguaglianze, Teoria dei Numeri, Combinatoria, Geometria Piana e Teoria dell'Apprendimento Automatico.

• Miglioramenti delle Prestazioni:

  • DreamProver ha migliorato i tassi di successo delle prove in media del 61% rispetto ai sistemi precedenti all'avanguardia (SOTA) come Hilbert e Goedel-Prover-V2.
  • In domini specifici, i miglioramenti sono stati drastici: 114% in Teoria dei Numeri e 50% in Combinatoria.
  • In domini sottorappresentati (Geometria Piana, Teoria ML), DreamProver ha risolto significativamente più istanze rispetto agli LLM proprietari (ad esempio, risolvendo 14-16 problemi di geometria di livello Olimpico dove gli LLM di base ne risolvevano 0-3).

• Efficienza e Qualità:

  • Riduzione dei Token: DreamProver ha ridotto l'utilizzo dei token di output in media del 48% rispetto ai sistemi agenziali SOTA.
  • Concisione delle Prove: Le prove generate erano in media 50% più brevi, indicando una qualità superiore e una migliore struttura.
  • Riutilizzo dei Lemmi: L'analisi ha mostrato che il 58% dei lemmi generati durante l'addestramento è stato riutilizzato nei set di test, contribuendo al 71% di tutti i teoremi dimostrati con successo.

• Studi di Ablazione:

  • Rimuovere il raffinamento iterativo veglia-sonno (evoluzione a passaggio singolo) ha fatto crollare significativamente i tassi di successo (da 104 a 76 problemi risolti).
  • Rimuovere il clustering semantico ha portato a una libreria sovradimensionata e ingestibile, riducendo le prestazioni anche al di sotto di una baseline senza libreria.

5. Significato

DreamProver rappresenta un passaggio dalla dimostrazione di teoremi "one-shot" o a "libreria statica" verso un apprendimento continuo e auto-migliorante.

• Colmare il Divario: Colma efficacemente il divario tra il potere di ragionamento grezzo degli LLM e la conoscenza strutturata e riutilizzabile necessaria per il ragionamento matematico complesso.
• Scalabilità: Imparando una libreria compatta e trasferibile, il sistema riduce il costo computazionale della dimostrazione di nuovi teoremi, rendendo la verifica formale di alto livello più accessibile.
• Apprendimento Simile all'Uomo: Il framework imita i processi cognitivi umani (acquisizione di esperienza, astrazione di principi e dimenticanza di dettagli irrilevanti), suggerendo una strada percorribile verso sistemi di ragionamento AI più robusti e generalizzabili.

In conclusione, DreamProver dimostra che apprendere e raffinare esplicitamente una libreria di lemmi riutilizzabili è un fattore critico per raggiungere prestazioni all'avanguardia nella dimostrazione automatica di teoremi, in particolare in domini matematici complessi e con scarsità di dati.