Riepilogo Tecnico: Formalize Once, Edit the Rest (BASE)

1. Definizione del Problema

Man mano che i Large Language Models (LLM) vengono applicati sempre più al ragionamento matematico, essi generano spesso molteplici percorsi di ragionamento distinti e candidati risposte per un singolo problema. Una sfida critica sorge nella selezione della risposta: come verificare quale candidato sia corretto senza avere accesso alle etichette di verità (ground-truth) durante lo scaling al tempo di test.

Sebbene gli approcci esistenti, come il voto di maggioranza o i modelli di ricompensa appresi, offrano segnali statistici, essi mancano di garanzie formali. Ricerche recenti hanno sfruttato gli assistenti alla prova formale (specificamente Lean 4) per verificare i candidati. In questo paradigma, un "autoformalizzatore" traduce un problema e una risposta candidata in una dichiarazione di teorema in Lean che afferma la correttezza della risposta. Un prover (dimostratore) tenta quindi di verificare tale dichiarazione.

Tuttavia, esiste un collo di bottiglia significativo: per verificare $K$ risposte candidate, l'autoformalizzatore deve essere invocato $K$ volte indipendentemente. Ciò comporta un costo computazionale di $\Theta(K)$, che scala linearmente con il numero di campioni. Gli autori osservano che, per un singolo problema, le $K$ dichiarazioni formali sono quasi identiche, condividendo la stessa struttura del problema e differendo solo nell'espressione della risposta. Il problema centrale è come sfruttare questa struttura condivisa per ridurre i costi di formalizzazione da $\Theta(K)$ a $\Theta(1)$ senza sacrificare l'accuratezza della selezione.

2. Metodologia: La Pipeline BASE

Gli autori propongono BASE (Base-and-Substitute-Edit), una pipeline progettata per formalizzare un singolo candidato "base" e derivare le restanti $K-1$ dichiarazioni attraverso un editing localizzato.

2.1 Scoperta della Base (Base Discovery)

La pipeline inizia con un solver a monte che genera una lista ordinata di $K$ risposte candidate, $S(x) = (a_1, \dots, a_K)$, ordinate per confidenza del solver.

• Il sistema itera attraverso i candidati in ordine di rango.
• Per ogni candidato $a_i$, tenta di formalizzare la coppia problema-risposta $(x, a_i)$ in una dichiarazione Lean $F_i$.
• Il processo si ferma al primo candidato $a_b$ la cui formalizzazione $F_b$ viene verificata con successo (type-checks) in Lean.
• $F_b$ diventa la formalizzazione base, e $a_b$ è la risposta base.
• Se nessun candidato passa il controllo del tipo, il sistema ricade sul primo candidato in classifica $a_1$.

2.2 Cascata di Sostituzione (Substitution Cascade)

Una volta stabilita una base valida $F_b$, il sistema genera le restanti $K-1$ dichiarazioni modificando $F_b$ in loco per riflettere gli altri candidati. Questo è gestito da una cascata a due livelli:

1. Livello 1 (R1): Localizzazione Diretta Basata su Regole

   • Il sistema tenta di localizzare l'espressione della risposta in $F_b$ tramite un matching esatto di stringhe all'interno di una "regione recintata" (il corpo del teorema, escludendo commenti/header).
   • Se viene trovato un match unico, il sistema esegue una sostituzione diretta della stringa della risposta.
   • Se si verificano match multipli, un piccolo modello di disambiguazione seleziona lo slot corretto.
   • Questo livello è efficiente ma fallisce quando l'autoformalizzatore codifica la risposta in una forma sintatticamente diversificata (ad esempio, una tupla (3, 5) codificata come binding separati o un valore Prod) piuttosto che come una stringa letterale.

2. Livello 2 (R2): LEANSCRIBE (Riscrittore Appreso)

   • Nei casi in cui R1 fallisce, il sistema invoca LEANSCRIBE, un LLM specializzato e sottoposto a fine-tuning.
   • Input: Il problema $x$, la formalizzazione base $F_b$ e la risposta base $a_b$.
   • Output:
     • Un blocco locale $s$: Un segmento contiguo di $F_b$ che contiene l'espressione dipendente dalla risposta.
     • Una funzione di riempimento $f$: Una funzione Python leggera che mappa qualsiasi risposta informale $a_i$ alla corrispondente espressione Lean che sostituisce $s$.
   • Esecuzione: LEANSCRIBE viene eseguito una sola volta per problema. La funzione generata $f$ viene poi applicata a tutti i candidati rimanenti $a_i$ per produrre le loro dichiarazioni formali $F_i = f(a_i)$. Ciò ammortizza il costo della chiamata al modello su tutti i $K-1$ candidati.

2.3 Verifica e Selezione

La pipeline si affida alla verifica del tipo della dichiarazione (statement-level type-checking) come segnale primario di selezione.

• Un candidato è considerato "verificato" se la sua dichiarazione formale $F_i$ passa il controllo del tipo in Lean (ovvero, è una proposizione ben formata).
• Il sistema selezcorre il candidato con il rango più alto $a_j$ tale che $F_j$ passi il controllo del tipo.
• Se nessun candidato passa il controllo del tipo, si ricade sul primo candidato in classifica $a_1$.
• Gli autori notano che, sebbene la verifica a livello di prova (esecuzione di un prover) sia più rigorosa, gli attuali prover hanno bassi tassi di pass@1, rendendo il controllo del tipo a livello di dichiarazione un segnale più pratico per la selezione in questo contesto di budget limitato.

3. Contributi Chiave

1. Pipeline BASE: Il primo lavoro che ammortizza i costi di formalizzazione condividendo una singola dichiarazione base verificata tra più candidati, riducendo le chiamate all'autoformalizzatore da $\Theta(K)$ a $\Theta(1)$.
2. Modello LEANSCRIBE: Un riscrittore appreso addestrato per localizzare blocchi dipendenti dalla risposta e generare funzioni di editing riutilizzabili, gestendo variazioni sintattiche che la sostituzione basata su regole non può gestire.
3. Miglioramento di Pareto: Il metodo raggiunge un'accuratezza di selezione superiore riducendo significativamente il costo computazionale in tutte le configurazioni testate.

4. Risultati Sperimentali

Gli autori hanno valutato BASE su quattro benchmark (MATH-500, OlympiadBench, AMC-AIMO, AIME 2024) utilizzando tre diversi solver a monte (Gemini 3 Pro, Qwen3-8B, DeepSeek-R1-Qwen3-8B) con $K=8$ candidati.

• Accuratezza: BASE ha migliorato l'accuratezza di selezione (Acc) in tutti i 12 casi (dataset, solver) rispetto alla formalizzazione indipendente, con guadagni compresi tra +0,7 e +23,3 punti percentuali.
• Robustezza: Il tasso di "Passaggio della Risposta Oro" (GT-pass) — la frazione di problemi in cui la dichiarazione della risposta corretta supera il controllo del tipo — è aumentato significamente (fino a +33,3 punti), raggiungendo il 96–100% in molti casi. Ciò indica che condividere una base verificata rende la formalizzazione della risposta corretta più robusta.
• Efficienza dei Costi: A $K=8$, BASE ha ridotto il numero di chiamate all'autoformalizzatore di circa 5,4× (riduzione media di 4,7–6,5×). Il costo scala come $\Theta(1)$ invece di $\Theta(K)$.
• Ablazione: Rimuovere il riscrittore appreso (LEANSCRIBE) e fare affidamento esclusivamente sulla sostituzione basata su regole (R1) ha comportato un calo significativo della copertura dei candidati (8–22 punti percentuali), dimostrando la necessità della componente appresa per gestire diverse codifiche sintattiche.
• Analisi a Livello di Prova: Anche utilizzando un prover (DeepSeek-Prover-V2) con un singolo tentativo per candidato, BASE ha migliorato l'accuratezza a livello di prova in 11 configurazioni su 12, suggerendo che dichiarazioni formali meglio strutturate aiutano i prover a valle.

5. Significato e Rivendicazioni

Il documento afferma che BASE rappresenta un miglioramento di Pareto per la selezione delle risposte basata su Lean. Formalizzando una volta ed editando il resto, il metodo simultaneamente:

• Riduce i Costi: Abbassa drasticamente il costo di inferenza della formalizzazione, rendendo più fattibile lo scaling temporale del test con un grande $K$.
• Migliora l'Accuratezza: Aumenta l'affidabilità della selezione della risposta corretta, probabilmente perché la struttura base condivisa riduce la varianza e il tasso di fallimento dell'autoformalizzatore per il candidato corretto.

Gli autori sottolineano che questo approccio è un "sostituto diretto" (drop-in replacement) per la fase di formalizzazione nelle pipeline esistenti (dimostrato dall'integrazione nella pipeline FANS) e che i guadagni sono guidati dalla capacità del verificatore di trattenere le risposte corrette in modo più efficace quando viene utilizzata una struttura (scaffold) condivisa e verificata, piuttosto che da cambiamenti nella generazione del solver a monte.

Il lavoro riconosce i limiti, notando che si concentra sul controllo del tipo a livello di dichiarazione a causa delle attuali limitazioni dei prover e assume che le risposte candidate condividano una struttura lato problema. Non pretende di risolvere la fedeltà dell'autoformalizzazione (dove una risposta errata potrebbe comunque superare il controllo del tipo), ma suggerisce che combinare i segnali formali con i ranking del solver mitighi questo rischio.