Riepilogo Tecnico: VERITAS: Ricerca di Prove Guidata dal Verificatore per la Dimostrazione Formale Zero-Shot

Definizione del Problema

Gli attuali dimostratori di teoremi formali basati su Large Language Model (LLM) tipicamente collassano i segnali ricchi e strutturati dei verificatori formali (come Lean 4) in un esito binario di pass/fail. I verificatori forniscono feedback granulari che includono errori di sintassi, discrepanze di tipo, progresso parziale dell'obiettivo e stato di completamento della prova. Tuttavia, le pipeline standard scartano questi artefatti intermedi, riassumendoli in ricompense scalari o scartandoli del tutto. Ciò costringe l'algoritmo di ricerca a "reinsegnare" informazioni che il verificatore ha già fornito esplicitamente, un limite che diventa particolarmente oneroso nelle prove che richiedono catene di tattiche dipendenti, dove la correttezza di ogni passaggio dipende dall'effetto del precedente sullo stato dell'obiettivo.

Metodologia: Il Framework VERITAS

VERITAS è un framework zero-shot progettato per instradare ogni segnale del verificatore all'indietro nel processo di generazione della prova. Utilizza un'architettura a quattro agenti coordinata da uno stato di prova condiviso e un protocolo di ricerca a due fasi.

1. Quattro Agenti Specializzati

Tutti gli agenti operano su un ProofState condiviso contenente il teorema, l'obiettivo corrente, le ipotesi, la cronologia delle tattiche e quattro segnali strutturati da Lean:

• Strategist (Strategista): Mappa lo stato della prova in una delle sei strategie di alto livello (diretta, induzione, contraddizione, casi, riscrittura, apply_lemma) e stima la profondità, restringendo la ricerca a un sottospazio rilevante.
• Retriever (Recuperatore): Fa emergere i lemmi pertinenti di Mathlib scorando la sovrapposizione di parole chiave rispetto ai token dell'obiettivo, ai nomi dei lemmi e alle firme.
• Critic (Critico): Un modello leggero che valuta gli stati parziali della prova, suggerendo le prossime tattiche e raccomandazioni di pruning. Sostituisce i rollout casuali in MCTS con una stima del valore che integra il feedback a quattro vie di Lean.
• Tactician (Tattico): Genera $K$ candidati di tattica condizionati dalla strategia, dai lemmi recuperati, dalla guida del Critic e, crucialmente, da un elenco di tattiche precedentemente fallite con i relativi messaggi di errore specifici di Lean iniettati come esempi negativi.

2. Protocollo a Due Fasi con Garanzia di Monotonicità

Il framework utilizza un protocollo conservativo a due fasi per garantire che i guadagni siano attribuibili alla ricerca guidata dal feedback:

• Fase 1 (Best-of-N): Una scansione standard Best-of-N (ad esempio, $N=5$) genera tattiche in un unico batch. Se una qualsiasi ha successo, il teorema è risolto immediatamente.
• Fase 2 (Critic-Guided MCTS): Attivata solo se la Fase 1 fallisce. L'insieme dei fallimenti della Fase 1 (tattiche e i relativi errori) viene iniettato nel prompt di sistema del Tactician come esempi negativi. Il Critic guida un Monte Carlo Tree Search (MCTS) dove:
  • Selezione: Utilizza una formula UCB estesa che incorpora il valore del Critic e l'allineamento con la strategia.
  • Espansione: Gli agenti operano sequenzialmente; i candidati sono validati tramite un trucco di Validazione Lean Batchizzata.
  • Simulazione: Sostituisce i rollout casuali con il valore del Critic aumentato da segnali strutturati ($\sigma_A$ sintassi, $\sigma_B$ tipo, $\sigma_C$ progresso, $\sigma_D$ completamento).
  • Backpropagation: Trasporta i segnali strutturati verso l'alto invece di collassarli in un win/loss binario, preservando il credito per il progresso parziale.

Validazione Lean Batchizzata: Inveve di invocare Lean $K$ volte per ogni espansione, i candidati vengono compilati in un singolo file .lean come teoremi privati e validati in una singola chiamata. Ciò riduce il costo di verifica da $O(K)$ a $O(1)$, producendo un'accelerazione di circa $\sim10\times$.

Monotonicità: Il protocollo garantisce che l'insieme finale di teoremi risolti sia un sovrainsieme di quelli risolti solo dalla Fase 1 ($S \supseteq S_1$). Ciò isola il contributo della Fase 2, assicurando che qualsiasi soluzione aggiuntiva sia strettamente dovuta alla ricerca MCTS guidata dal verifier.

Contributi Chiave

1. Framework Zero-Shot a Quattro Agenti: Un sistema che instrada il feedback strutturato di Lean (sintassi, tipo, progresso, completamento) in ogni decisione di generazione senza fine-tuning del trace.
2. Protocollo a Due Fasi: Un design Best-of-N $\to$ Critic-MCTS con una garanzia interna di monotonicità che permette una pulita attribuzione dei contributi della ricerca.
3. Ottimizzazione dell'Efficienza: Un trucco di validazione Lean batchizzata che riduce l'overhead di verifica di circa $10\times$.
4. VERITAS-CombiBench: Un nuovo benchmark di 55 teoremi di combinatoria difficili, verificati dagli autori in Lean 4, rilasciato per esporre i limiti del campionamento non guidato.
5. Analisi di Attribuzione: Evidenza empirica che mostra come 11 teoremi di miniF2F fossero unicamente risolvibili dalla fase MCTS, che il campionamento piatto non riusciva a raggiungere.

Risultati Sperimentali

Gli esperimenti sono stati condotti su miniF2F (244 teoremi) e VERITAS-CombiBench (55 teoremi).

• Performance su miniF2F: VERITAS ha raggiunto un tasso di risoluzione del 40,6% (99/244), superando la baseline indipendente Best-of-5 (36,9%) e un Portfolio artigianale (26,2%).
  • La Fase 2 ha contribuito con 11 risoluzioni uniche che il campionamento piatto non poteva raggiungere, principalmente su problemi che richiedono 2–4 tattiche dipendenti.
  • Sui problemi "difficili" senza l'uso di sorry, VERITAS ha raggiunto il 28,9% rispetto al 25,9% del Best-of-5.
• Performance su VERITAS-CombiBench: Questo benchmark ha evidenziato il fallimento del campionamento non guidato. Il Best-of-5 ha ottenuto solo l'1,8%, scendendo al di sotto del Portfolio (3,6%) perché gli LLM hanno allucinato nomi errati di lemmi di Mathlib. VERITAS ha raggiunto il 7,3% correggendo iterativamente questi nomi utilizzando il feedback degli errori di Lean.
• Efficienza: VERITAS domina la frontiera di Pareto per i metodi basati solo sull'inferenza, raggiungendo un tasso di risoluzione del 40,6% con circa 27 chiamate a Lean per teorema a un costo API di circa $150 per sweep.
• Modalità di Fallimento: L'analisi ha mostrato che il 32% dei fallimenti era a livello di sintassi (nomi allucinati), il 17% era corretto dal punto di vista del tipo ma errato, e il 10% erano "near-misses" (progresso parziale dell'obiettivo) dove il Critic poteva fornire una guida di alto valore.

Significato e Rivendicazioni

Il documento pone un principio di design generale: quando un verificatore deterministico emette segnali intermedi strutturati, ripiegarli nella generazione amplifica l'LLM in modo sostanziale molto più di quanto faccia l'aggiunta di campionamento.

VERITAS dimostra che:

1. Segnali del Verificatore come Stato: I segnali deterministici del verificatore possono servire come stato di inferenza, non solo come controlli finali.
2. Sinergia dei Componenti: Accoppiare strettamente il verificatore con la generazione è più efficace che scalare l'LLM o la componente di ricerca in isolamento.
3. Correzione Iterativa: Per domini che richiedono un recupero preciso dei lemmi (come la combinatoria), la correzione iterativa dagli errori del verifier è superiore al campionamento piatto, che tende ad allucinare nomi lessicalmente errati.

Gli autori concludono che, sebbene VERITAS non sia una cura per la creatività di livello IMO o per la latenza interattiva, il suo contributo primario è il routing: raccogliere efficientemente le prove facili nella Fase 1 e spendere il budget computazionale nella Fase 2 solo dove i fallimenti del verifier possono guidare la tattica successiva. Il lavoro futuro è identificato nel miglioramento del recupero, nella creazione di critic più economici e nella distillazione dei trace della Fase 2 per scalare questo principio alla restante parte difficile dei problemi.