Riassunto Tecnico: ProofWala

Problematica

La dimostrazione automatica di teoremi mediante metodi neurali richiede un'infrastruttura robusta per interfacciarsi con i Teoremi Interattivi (ITP), estrarre dati strutturati sulle dimostrazioni ed eseguire la ricerca delle dimostrazioni su larga scala. Gli strumenti esistenti sono spesso frammentati, specifici per un singolo assistente e orientati all'esecuzione interattiva a livello di file tramite interfacce REPL (Read-Eval-Print Loop). Questa architettura presenta limitazioni significative:

• Scalabilità: Ostacola l'analisi su scala di repository e la sperimentazione parallela.
• Estrazione dei Dati: Fornisce un accesso limitato ai metadati a livello di dichiarazione (es. definizioni induttive, costanti, namespace) e rende difficile, se non impossibile, la costruzione di grafi di dipendenza su tutto il repository.
• Lacune tra gli Assistenti: La mancanza di strumenti unificati rende difficile sfruttare i potenziali vantaggi cross-lingua e cross-dominio derivanti dall'addestramento su corpora formali multilingue (es. Lean e Rocq).

Metodologia

Gli autori presentano ProofWala, un framework di ingegneria delle dimostrazioni multilingue progettato per unificare interazione, estrazione dati, addestramento e ricerca tra diversi ITP. Il framework si basa su tre componenti principali:

1. Il Modulo di Interfaccia (itp-interface)

Questa è una libreria riutilizzabile per l'interazione programmatica con gli ITP, che fornisce un'astrazione unificata per Lean 4 e Rocq (versioni multiple).

• Backend Lean 4: Invece di fare affidamento su un'architettura basata su REPL, gli autori hanno implementato meta-programmi che vengono eseguiti direttamente all'interno dell'elaboratore di Lean. Ciò consente:
  • Una tracciatura dei livelli di tattica semanticamente fedele.
  • L'estrazione di metadati a livello di dichiarazione e la costruzione di grafi di dipendenza su tutto il repository.
  • Una migliore gestione delle costrutti tattici annidati (es. blocchi have).
  • Clonazione dell'Ambiente: La capacità di clonare gli ambienti di dimostrazione per l'esecuzione parallela, operazione difficile con i flussi di lavoro REPL standard.
  • Robustezza della Versione: Un sottile livello di compatibilità garantisce la compatibilità futura attraverso le versioni di Lean 4 a partire dalla 4.15.0.
• Backend Rocq: Costruito su coq_serapy, estendendolo per supportare l'estrazione sistematica di stati di dimostrazione e tracce di tattica, mappandoli nello stesso formato unificato utilizzato per Lean.
• Modello di Stato Unificato: Entrambi gli assistenti sono mappati su un sistema di transizione di stato standardizzato in cui uno stato di dimostrazione è un insieme di obblighi (obiettivi e ipotesi) e le tattiche transitano questi stati.

2. Modulo Dati e Modello

• Estrazione dei Dati: Il framework estrae coppie stato-dimostrazione–tattica dai principali repository (CompCert, MathComp, GeoCoq, Mathlib, CategoryTheory) riproducendo gli script delle tattiche all'interno del kernel dell'assistente.
• Formato Unificato: I dati estratti sono memorizzati in un formato JSON unificato che astrae i dettagli specifici dell'assistente preservando al contempo le informazioni semantiche. Il formato del prompt per l'addestramento è identico per Lean e Rocq, omettendo i token specifici dell'assistente per facilitare l'addestramento cross-assistente.
• Addestramento: Gli autori hanno effettuato il fine-tuning di un modello CodeT5-Base (220 milioni di parametri) su tre configurazioni:
  1. ProofWala-Rocq: Addestrato su repository Rocq.
  2. ProofWala-Lean: Addestrato su repository Lean.
  3. ProofWala-Multilingual: Addestrato congiuntamente su entrambi gli assistenti.

3. Modulo di Ricerca Parallela delle Dimostrazioni

• Pool di Ambienti: Un'innovazione chiave è il pool di ambienti, che mantiene molteplici ambienti di dimostrazione clonati e inizializzati a stati di frontiera identici.
• Esecuzione Parallela: Le tattiche candidate vengono eseguite concorrentemente attraverso queste istanze clonate. Questo pool si integra con Ray per l'esecuzione distribuita, consentendo una ricerca delle dimostrazioni scalabile e un'annotazione su larga scala.
• Algoritmi di Ricerca: Il modulo supporta la ricerca best-first e beam parallelizzata. Mantiene un albero di dimostrazione annotato registrando solo transizioni di stato valide e compilabili, consentendo un'analisi fine-grained della dinamica di ricerca.

Contributi Chiave

1. Framework Standardizzato e Libreria di Ingegneria: ProofWala fornisce un framework unificato per estrarre e organizzare dati a livello di tattica e supportare lo sviluppo di strumenti. Introduce una pipeline di strumentazione meta-programmata per Lean che supporta la traversata del repository consapevole delle dipendenze e la clonazione dell'ambiente, capacità precedentemente difficili da ottenere tramite REPL.
2. Supporto per il Completamento Parallelo delle Dimostrazioni: Il framework è il primo sistema open-source che fornisce ricerca parallela delle dimostrazioni supportando esplicitamente ambienti di dimostrazione clonati e l'valutazione concorrente delle tattiche all'interno di un'interfaccia unificata multi-ITP.
3. Dataset e Modelli Multilingue: Gli autori rilasciano un dataset multilingue (~450K datapoint, 270 milioni di token) e modelli addestrati (Lean, Rocq e Multilingual) che facilitano la ricerca delle dimostrazioni end-to-end.

Risultati

Gli autori hanno valutato i modelli su split di test da CompCert, MathComp, GeoCoq, CategoryTheory e Lean/Mathlib, nonché sul benchmark MiniF2F.

• Trasferimento Cross-Lingua: Il modello ProofWala-Multilingual generalmente eguaglia o migliora i baseline monolingue.
  • Miglioramenti Statisticamente Significativi: Osservati sul benchmark più grande (Lean/Mathlib) e nel setting di adattamento del dominio CategoryTheory (dove il modello multilingue è stato sottoposto a fine-tuning sui dati di CategoryTheory).
  • Trend: Altri dataset hanno mostrato trend coerenti ma non statisticamente significativi a favore dell'addestramento multilingue.
• Adattamento del Dominio: Nel dominio CategoryTheory, il modello multilingue ha ottenuto punteggi pass-at-k sostanzialmente più alti dopo il fine-tuning rispetto al baseline solo-Rocq, suggerendo che il pre-training su dati di linguaggio misto aiuta l'adattamento anche quando il dominio target è rappresentato in un solo assistente.
• Dinamiche di Ricerca: L'analisi degli alberi di dimostrazione ha rivelato che i modelli multilingue producono spesso alberi più grandi con fattori di ramificazione più elevati, indicando che propongono un numero maggiore di tattiche valide per stato.
• Scalabilità: L'esecuzione parallela tramite pool di ambienti ha migliorato significativamente il throughput. L'aumento dei worker CPU da 8 a 20 ha migliorato il pass@5 su MiniF2F dal 22,54% al 26,23% riducendo contemporaneamente il tempo medio di dimostrazione.

Significato e Rivendicazioni

L'articolo sostiene che ProofWala rappresenti un passaggio da strumenti frammentati e specifici per assistente a un'infrastruttura unificata e scalabile per la dimostrazione neurale di teoremi.

• Unificazione Architetturale: Unificando esecuzione, raccolta dati, analisi delle dipendenze e ricerca, il framework consente un'analisi sistematica, riproducibile e fine-grained della ricerca di dimostrazioni neurali attraverso molteplici ITP.
• Evidenza di Trasferimento: Il lavoro fornisce prove empiriche del fatto che l'addestramento multilingue produce un trasferimento cross-lingua e cross-dominio positivo nella ragione formale, particolarmente in regimi ad alto volume di dati e scenari di adattamento del dominio.
• Fondazione per la Ricerca: Gli autori posizionano ProofWala non solo come un sistema di ricerca di dimostrazioni, ma come un framework di ricerca che trasforma la ricerca di dimostrazioni da una valutazione "black-box" a una pipeline analizzabile. Ciò consente ai ricercatori di studiare il trasferimento strutturale, le dimensioni degli alberi, i fattori di ramificazione e la latenza di esecuzione in modi precedentemente difficili da ottenere.

Gli autori osservano che, sebbene siano probabilmente necessari modelli più grandi e infrastrutture aggiuntive (es. retrieval, verifier) per ottenere prestazioni allo stato dell'arte sui benchmark, il loro contributo primario è il framework stesso, che isola gli effetti dell'addestramento multilingue e delle strategie di ricerca parallela. Essi vedono l'estensione agli assistenti orientati ai documenti (come Isabelle) come una sfida ingegneristica piuttosto che un limite concettuale, lasciandola come lavoro futuro.