Riepilogo Tecnico: Lean-as-Judge Controllato dal Rischio per il Ragionamento Matematico in Linguaggio Naturale

1. Enunciato del Problema

Il documento affronta la sfida di utilizzare assistenti di prova formale (in particolare Lean) come giudici per il ragionamento matematico in linguaggio naturale generato da Modelli Linguistici su Larga Scala (LLM). Sebbene una prova Lean riuscita fornisca una forte evidenza positiva per un'affermazione formale, l'assenza di una prova è un segnale ambiguo. Un fallimento della prova può indicare una risposta matematicamente errata, ma può ugualmente derivare da una formalizzazione mal tipizzata, fatti di libreria mancanti o timeout nella ricerca della prova.

Gli approcci attuali trattano spesso il fallimento della prova come un segnale negativo di correttezza, rischiando di confondere l'erroneità matematica con una mancanza di copertura formale. Gli autori identificano una "scogliera di copertura" (coverage cliff): l'affidabilità della selezione formale dipende in modo acuto dalla proporzione di risposte candidate che possono essere formalizzate e provate con successo. Quando la copertura è alta, la selezione formale è altamente accurata; quando la copertura è bassa, il segnale diventa inaffidabile.

Il problema centrale è determinare quando un sistema a valle dovrebbe fidarsi di un segnale formale Lean e quando dovrebbe trattare il segnale come fuori copertura (cioè irrisolto) piuttosto che errato, fornendo al contempo una garanzia di rischio su campioni finiti per le risposte accettate.

2. Metodologia: COVCAL

Gli autori propongono COVCAL (Coverage-Calibrated Lean), un wrapper selettivo controllato dal rischio che decide se accettare una risposta formale o astenersi sulla base di diagnosi di copertura.

2.1 Framework di Osservazione Parziale

Il sistema tratta la pipeline formale come un meccanismo di osservazione parziale. Non osserva la verità di ogni risposta candidata, ma osserva solo:

1. Quali classi di risposte normalizzate raggiungono un'affermazione Lean ben formata (Copertura Tipizzata).
2. Quali di queste classi vengono provate con successo (Copertura Provata).
3. Il peso della classe provata con il peso più alto rispetto al rivale irrisolto con il peso più alto (Margine Formale).

Una classe di risposta è definita come un gruppo di stringhe candidate che denotano la stessa risposta finale (ad esempio, $1/2$, $0.5$, $2/4$). Le classi che non vengono formalizzate o non vengono provate sono considerate irrisolte, non automaticamente errate.

2.2 Diagnosi di Copertura

COVCAL calcola quattro metriche chiave per un dato problema $x$:

• Copertura Tipizzata ($C_{typ}$): Il peso totale delle classi candidate che hanno raggiunto un'affermazione Lean ben formata (stato: proved, typechecked o timeout).
• Copertura Provata ($C_{prf}$): Il peso totale delle classi candidate che hanno ricevuto una prova verificata dal kernel.
• Massa del Rivale Irrisolto ($R_{unres}$): Il peso della classe di risposta con il peso più alto che non è stata provata.
• Margine Formale ($M$): La differenza tra il peso della classe provata con il peso più alto e la massa del rivale irrisolto.

2.3 Selezione e Certificazione

COVCAL accetta la classe provata con il peso più alto solo se è soddisfatta una regola pre-dichiarata basata su soglie $(\tau_{typ}, \tau_{prf}, \tau_M)$. Se la regola non è soddisfatta, il sistema si astiene (o ricade su un metodo non formale come la coerenza interna).

Per garantire l'affidabilità, COVCAL impiega una certificazione del rischio selettivo su campioni finiti. Garantisce che, con probabilità $1-\delta$, il rischio selettivo (tasso di errore) delle risposte accettate sia al massimo $\epsilon$. Vengono proposti due regimi di certificazione:

1. Regime di Bonferroni: Cerca su una griglia di soglie su una partizione di calibrazione e applica una correzione del limite di unione ($\delta/|T|$) per tenere conto dei confronti multipli. Questo è conservativo e richiede un'alta densità di segnale per essere fattibile.
2. Regime Dev-then-Cal: Seleziona la soglia su una partizione di sviluppo indipendente e la certifica una volta sulla partizione di calibrazione utilizzando un singolo limite di Clopper-Pearson ($\delta$). Questo è più efficiente in termini di campioni ma richiede una separazione rigorosa tra i dati di sviluppo e quelli di calibrazione.

2.4 Limiti Teorici

Il documento dimostra che senza diagnosi di copertura (cioè, affidandosi esclusivamente all'esistenza di una prova), non può essere derivato alcun certificato di correttezza puntuale non banale se esiste una classe rivale irrisolta e non equivalente. L'assenza di prove formali non è prova di falsità matematica; è prova di uno stato irrisolto.

3. Contributi Chiave

1. Caratterizzazione della Scogliera di Copertura: Sul dataset MATH-500, gli autori dimostrano che la risposta "vincitrice della prova" è corretta il 96% delle volte ad alta copertura provata, ma solo il 20% a bassa copertura. Ciò stabilisce che le prove Lean sono affidabili solo quando copertura e margine sono elevati.
2. Sparsità del Segnale e Fedeltà: Il segnale formale è sparso e imperfetto. Un auto-formalizzatore da 7B prova una classe per solo il 28% dei problemi. Inoltre, un audit manuale rivela che solo circa il 43% di queste prove è fedele al problema originale (il resto sono identità banali o affermazioni vere ma irrilevanti).
3. Metodo COVCAL: Un framework di previsione selettiva che certifica il rischio sotto osservazione parziale. Gestisce esplicitamente l'asimmetria del fallimento della prova e fornisce garanzie su campioni finiti per le previsioni accettate.
4. Fattibilità Dipendente dal Formalizzatore: Il documento dimostra che la fattibilità del certificato è governata dalla copertura dell'auto-formalizzazione. Un formalizzatore da 7B produce un segnale troppo sparso per il regime conservativo di Bonferroni (rifiutando tutte le 20 partizioni bootstrap), mentre un formalizzatore specializzato nel prover (Goedel-Prover-V2-8B) che raggiunge il 79% di copertura rende il metodo fattibile su 17/20 partizioni.

4. Risultati Sperimentali

Gli esperimenti sono stati condotti su un sottoinsieme filtrato di MATH-500 (378 esempi) utilizzando Qwen2.5-Math-7B per la generazione e vari formalizzatori per l'auto-formalizzazione.

• Prestazioni di Base: La sola coerenza interna raggiunge il 91% di accuratezza senza astensione.
• Prestazioni di COVCAL:
  • Sotto il regime di Bonferroni con un formalizzatore da 7B, il metodo rifiuta tutti gli input (0/20 partizioni) perché il segnale è troppo sparso per soddisfare il rigido limite di unione.
  • Sotto il regime dev-then-cal con il formalizzatore da 7B, 12/20 partizioni sono certificate. La frazione accettata è circa il 21%, con un'accuratezza accettata di 0,93.
  • Con Goedel-Prover-V2-8B (formalizzatore specializzato), la copertura provata sale al 79%. Bonferroni diventa fattibile su 17/20 partizioni, accettando circa il 48% dei problemi con un'accuratezza accettata di 0,98.
• Audit di Fedeltà: Un audit manuale di 45 esempi stratificati ha mostrato che, sebbene il 73,6% delle affermazioni provate fosse non banale e corretto, solo il 43% era fedele all'affermazione del problema. Molte affermazioni "provate" erano fatti collaterali veri o identità banali che non catturavano i vincoli del problema.

5. Significato e Affermazioni

Il documento afferma che il suo contributo principale è un resoconto preciso di quando e con quale formalizzatore un segnale formale parziale può essere affidato sotto controllo del rischio, piuttosto che semplicemente migliorare l'accuratezza grezza.

• Controllo del Rischio sull'Accuratezza Grezza: Poiché la coerenza interna è già accurata al 91%, il valore di COVCAL risiede nella sua capacità di fornire un certificato per il sottoinsieme di risposte che accetta, distinguendo tra "verificate" e "irrisolte" piuttosto che tra "corrette" e "errate".
• Gestione delle Osservazioni Parziali: Il lavoro riformula la verifica formale come un problema di previsione selettiva in cui le prove mancanti sono trattate come candidati irrisolti, prevenendo l'etichettatura errata di ragionamenti corretti come errati a causa di fallimenti di formalizzazione.
• Dipendenza dalla Specializzazione: I risultati evidenziano che la scala grezza del modello non è un sostituto per la specializzazione. Un formalizzatore specializzato nel prover supera significativamente un modello generalista più grande in termini di copertura di prova, che è il vincolo vincolante per il controllo del rischio certificabile.

Gli autori concludono che COVCAL funge da interfaccia conservativa per l'uso di Lean come giudice: è fattibile e informativa solo quando l'auto-formalizzatore copre una massa di risposte sufficiente a supportare un certificato di rischio, ma non garantisce che tutte le risposte siano verificate.