DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems

1. Il Problema: Le Limitazioni dell'Autoformalizzazione Attuale

L'autoformalizzazione, ovvero la traduzione di enunciati matematici in linguaggio naturale verso linguaggi formali verificabili (come Lean 4), rimane una sfida significativa per i Large Language Models (LLM). Nonostante i progressi nel ragionamento informale, i modelli faticano a:

• Identificare e utilizzare le conoscenze prerequisito: I modelli spesso non riescono a reperire le definizioni formali corrette necessarie per costruire un teorema.
• Gestire la complessità delle query: I metodi di retrieval-augmented generation (RAG) esistenti trattano l'intero enunciato informale come una singola query "monolitica". Questo approccio è subottimale perché gli enunciati matematici sono densi e multifaccettati; una singola embedding vettoriale perde le sfumature dei concetti atomici distinti.
• Mancanza di contesto d'uso: Anche quando le definizioni formali corrette vengono recuperate, i modelli spesso non sanno come integrarle sintatticamente o come utilizzarle in contesti specifici, portando a errori strutturali.

2. Metodologia: Il Framework DRIFT

Il paper introduce DRIFT, un framework a quattro stadi progettato per colmare il divario tra la definizione formale e il suo utilizzo sintattico. Il processo è illustrato in Figura 1 del paper:

A. Decompose (Decomposizione)

Invece di inviare l'intero enunciato informale al retriever, un LLM (Decomposer) scompone l'enunciato in una serie di sotto-query atomiche focalizzate sui concetti.

• Ogni sotto-query $Q_i$ è composta da una descrizione in linguaggio naturale del concetto e una rappresentazione formale predetta (es. "Un numero primo $p$ della forma $4t+3$" $\rightarrow$ p : ℕ con Nat.Prime p e p % 4 = 3).
• Questa decomposizione trasforma un problema di retrieval complesso in ricerche mirate e precise, allineandosi alla struttura di dipendenza della matematica formale.

B. Retrieve (Recupero)

Per ogni sotto-query generata, un retriever denso (basato su BGE-M3 e finetunato sul task di "dependency retrieval") identifica le premesse fondamentali (definizioni, teoremi, strutture) dalla libreria formale (es. Mathlib).

• Il sistema recupera la premessa migliore (top-1) per ogni sotto-query e aggrega i risultati rimuovendo i duplicati.
• Questo approccio supera i metodi basati su $k$-NN o ricerca per parole chiave, garantendo una corrispondenza semantica più precisa tra i concetti naturali e le dipendenze formali.

C. Illustrate (Illustrazione)

Questa è una componente innovativa. Una volta recuperate le definizioni, il sistema seleziona un piccolo insieme di teoremi esemplificativi che dimostrano l'uso pratico di quelle definizioni.

• Viene utilizzato un algoritmo greedy per massimizzare la copertura delle premesse recuperate.
• L'obiettivo è fornire al modello esempi concreti di sintassi e pattern di applicazione, colmando il divario tra "sapere cosa è una definizione" e "sapere come usarla".

D. Formalize Theorems (Formalizzazione)

L'LLM finale (Formalizer) genera l'enunciato formale (in Lean 4) condizionato su:

1. L'istruzione di formalizzazione.
2. L'enunciato informale originale.
3. L'insieme delle premesse recuperate ($R_{DRIFT}$).
4. L'insieme dei teoremi illustrativi ($T$).

3. Contributi Chiave

1. Framework DRIFT: Un approccio guidato dalla decomposizione che rompe gli enunciati informali in sotto-query atomiche e contestualizza le premesse recuperate con esempi di teoremi. Questo supera il limite delle query monolitiche.
2. Nuovi Record (SOTA): Il framework stabilisce nuovi stati dell'arte nel recupero delle dipendenze e nell'autoformalizzazione su benchmark diversi (ProofNet, ConNF, MiniF2F-test), utilizzando sia modelli LLM all'avanguardia (GPT-4.1, DeepSeek-V3.1) che modelli open-source specializzati (Goedel-V2-8B).
3. Analisi delle Conoscenze Parametriche: Lo studio dimostra che l'efficacia del retrieval dipende fortemente dal divario tra le conoscenze interne del modello e la complessità dell'enunciato. DRIFT è particolarmente cruciale per i modelli che non possiedono le definizioni formali necessarie nel loro training set (out-of-distribution).

4. Risultati Sperimentali

Il framework è stato valutato su tre benchmark distinti:

• ProofNet (In-Distribution): DRIFT ha migliorato costantemente il recupero delle premesse, raddoppiando quasi il punteggio F1 rispetto alla baseline DPR su ProofNet. In termini di autoformalizzazione (metrica BEq+@10), DRIFT ha superato la baseline DPR del 2.74% con GPT-4.1.
• ConNF (Out-of-Distribution - OOD): Questo è il risultato più significativo. ConNF utilizza una libreria (con-nf) non presente nel training set dei modelli.
  • Senza retrieval, i modelli falliscono quasi completamente (<10% BEq+).
  • DRIFT ha portato a un miglioramento massiccio: +55.57% nel punteggio BEq+@10 per GPT-4.1 e +43.18% per DeepSeek-V3.1.
  • Notevolmente, DRIFT ha superato persino la baseline "Oracle*" (che fornisce le dipendenze corrette ma senza esempi di uso), dimostrando che gli esempi di utilizzo sono critici quanto le definizioni stesse.
• MiniF2F-test (Self-Contained): Su problemi con poche dipendenze esterne, l'aggiunta di contesto può talvolta agire come distrazione. Tuttavia, DRIFT mantiene prestazioni competitive, evidenziando la necessità di strategie di retrieval adattive.

Analisi Ablativa:
Lo studio ha mostrato che rimuovere il modulo "Illustrate" degrada significativamente le prestazioni su benchmark complessi (ConNF, ProofNet), confermando che gli esempi di uso sono essenziali per la correttezza semantica. Rimuovere la "Decomposizione" non peggiora ulteriormente le prestazioni in alcuni casi, suggerendo una sinergia: la decomposizione recupera informazioni più diversificate, ma il modulo Illustrate funge da "impalcatura" (scaffold) per guidare il modello attraverso questa diversità.

5. Significato e Implicazioni

Il lavoro DRIFT evidenzia che l'autoformalizzazione automatica non può basarsi solo sul recupero di definizioni statiche. La sintassi e l'uso contestuale sono altrettanto importanti.

• Adattabilità: DRIFT dimostra che i sistemi RAG per la matematica devono essere adattivi, considerando le capacità specifiche del modello (conoscenza parametrica vs. capacità di ragionamento in-context).
• Scalabilità: Il metodo è agnostico rispetto al modello e al linguaggio formale, funzionando efficacemente sia su modelli generalisti che su modelli specializzati.
• Futuro: Il paper suggerisce che le future ricerche dovrebbero focalizzarsi su strategie di retrieval dinamiche e su framework "agentic" che possano valutare l'utilità del contesto recuperato e iterare in base al feedback del compilatore, superando i limiti delle strategie statiche attuali.

In sintesi, DRIFT rappresenta un passo avanti fondamentale verso l'automazione della formalizzazione matematica, trasformando il processo da una semplice traduzione di testo a un ragionamento strutturato guidato dalla conoscenza e dall'esempio.