Riepilogo Tecnico: Mantenere lo Stato di Prova Attivo

Enunciato del Problema

I sistemi di dimostrazione automatica di teoremi che utilizzano Modelli Linguistici su Grande Scala (LLM) e la pipeline Draft–Sketch–Prove (DSP) fanno sempre più affidamento sulla ricerca basata su portafoglio. Questo approccio consiste nel fissare un insieme di tattiche candidate e tentarle in parallelo su ogni "buco di prova" (rappresentato dai token sorry) in una prova parzialmente specificata.

Nell'attuale ecosistema Lean 4 con Mathlib, questa ricerca parallela è gravemente ostacolata dall'overhead di avvio dei rami. Ogni ramo di ricerca ricostruisce attualmente lo stato della prova da zero, sostenendo due costi massicci:

1. Caricamento delle Importazioni: Deserializzazione delle librerie .olean precompilate (Mathlib), che richiede circa 60 secondi per ramo.
2. Elaborazione del Corpo del Teorema: Ricontrollamento del tipo dell'intestazione del teorema e di tutti i passaggi intermedi fino all'obiettivo finale. Questo scala con la complessità della prova, variando da 18 a 735 secondi per ramo.

Insieme, questi componenti consumano >99% del tempo reale per ramo. Per un portafoglio standard di 7 tattiche applicate a 4 buchi (28 rami), l'overhead può superare i 17 minuti su una singola macchina, rendendo la ricerca basata su portafoglio non fattibile alla scala delle pipeline DSP (che possono proporre 100+ candidati bozza per teorema). La causa radice è un disallineamento tra la gestione dello stato interno di Lean (che memorizza nella cache gli stati elaborati per la diagnostica dell'IDE) e l'accesso esterno (che impone una ricostruzione completa per ogni nuovo ramo).

Metodologia

Gli autori introducono lo Snapshotting dello Stato di Prova, un meccanismo che cattura lo stato della prova elaborato una sola volta e lo riutilizza attraverso molteplici rami paralleli, invece di ricostruirlo per ogni tentativo.

Architettura del Sistema

La soluzione comporta un'estensione minima al Language Server di Lean 4 (LSP) e un livello di orchestrazione Python:

1. Estensioni del Server Lean: Tre nuovi metodi JSON-RPC sono stati aggiunti a Lean.Server.FileWorker:

   • dspSnapshotPing: Un handshake per verificare il supporto degli snapshot.
   • dspSnapshotCapture: Data una URI del file e una posizione sorry, questo blocca l'esecuzione fino a quando l'elaborazione non raggiunge quel punto, registra un riferimento allo snapshot e restituisce un snapshotId stabile.
   • dspSnapshotBranch: Accetta un snapshotId e un array di configurazioni di tattiche. Avvia task paralleli (IO.asTask) per ogni tattica, sostituendo la tattica al sorry ed eseguendola contro lo stato dell'obiettivo catturato.

2. Meccanismo di Forking Efficiente:

   • Ambiente Condiviso: L'Environment (contenente tutte le costanti di Mathlib, le istanze di classi di tipo e gli insiemi simp, circa 2–4 GB) è immutabile. È condiviso tra tutti i rami per riferimento e mai copiato.
   • Contesto Copiato: Solo il MetavarContext (obbligazioni di prova aperte, tipicamente pochi kilobyte) viene copiato per ramo.
   • Risultato: Il forking di un ramo costa solo il tempo necessario per copiare pochi kilobyte di memoria, riducendo l'overhead di memoria per ramo da O(GB) a O(KB) ed eliminando la RAM come collo di bottiglia per il parallelismo.

3. Integrazione con DSP:

   • L'orchestratore Python rileva le posizioni sorry in una bozza generata da un LLM.
   • Cattura uno snapshot per ogni buco.
   • Invia l'intero portafoglio di tattiche (ad esempio aesop, norm_num, omega, ring, linarith, decide, simp) in una singola chiamata RPC in batch.
   • Il server distribuisce questi rami in parallelo utilizzando il pianificatore di stealing del lavoro di Lean.

Posizionamento

Questo lavoro definisce l'ottimizzazione di Livello 2 nella gerarchia dell'accelerazione della ricerca di prove:

• Livello 0 (DSP Standard): Ricostruzione completa per ramo.
• Livello 1 (ad es. Kimina): Memorizza nella cache l'Environment post-importazione tra i teoremi ma elabora ancora il corpo del teorema per ramo.
• Livello 2 (Snapshot-DSP): Memorizza nella cache lo stato post-elaborazione (incluso il corpo del teorema) e lo fork per i rami all'interno dello stesso teorema.
• Nota: Questo è ortogonale ai meccanismi di backtracking intra-ramo come SavedState utilizzati da Aesop.

Contributi Chiave

1. Implementazione del Sistema: Un sistema di snapshotting dello stato di prova composto da estensioni LSP di Lean 4 e un livello di orchestrazione Python che abilita il forking leggero degli stati di prova per l'esecuzione parallela delle tattiche.
2. Valutazione: Misure complete di accelerazione su 48 problemi miniF2F-v2, dimostrando che >99% del tempo reale per ramo è overhead eliminato da questo approccio.
3. Rilascio Open Source: Il binario Lean patchato, la pipeline Snapshot-DSP e la suite di valutazione sono rilasciati come open source.

Risultati

Gli esperimenti sono stati condotti su 48 problemi miniF2F-v2 (45 benchmark creati a mano e 3 esecuzioni complete end-to-end) su un MacBook Pro (8 GB di RAM).

• Accelerazione del Tempo Reale: L'approccio raggiunge un'accelerazione di 5,6–50× rispetto al fallback standard (build lake per ramo).
  • Media: 14× di accelerazione.
  • Mediana: 9,7× di accelerazione (su 45 benchmark creati a mano).
• Comportamento di Scalabilità: L'accelerazione scala monotonicamente con il numero di rami di prova (buchi × tattiche).
  • 1 buco (7 rami): ~7,9× di accelerazione.
  • 5 buchi (35 rami): ~29,8× di accelerazione.
• Decomposizione dei Costi:
  • Esecuzione della Tattica: Rappresenta solo pochi millisecondi fino a 500 ms per ramo (95° percentile: 289 ms).
  • Overhead: Il restante >99% del tempo di esecuzione nel fallback è overhead di elaborazione, che lo snapshotting elimina completamente.
  • Costo Nativo: L'approccio nativo di snapshot aggiunge solo 4–13 secondi di overhead combinato LSP ed esecuzione della tattica oltre al costo di cattura una tantum.

Significato e Affermazioni

Il documento afferma che lo snapshotting dello stato di prova è un'architettura di pura accelerazione che non altera l'accuratezza delle prove o le strategie di ricerca, ma rimuove la barriera di scalabilità che impedisce l'uso di grandi portafogli di tattiche su singole macchine.

• Fattibilità: Trasforma scenari di ricerca non fattibili (ad esempio, 2.800 rami che richiedono 29 ore) in scenari gestibili (3,5 ore) su hardware standard.
• Cambiamento Architettonico: Il lavoro funge da "prova di esistenza" che il confine tra la gestione dello stato interno di Lean e i sistemi AI esterni può essere ridisegnato. Esponendo lo snapshot-e-fork come operazione server di prima classe, dimostra che il riutilizzo dello stato a livello di elaborazione è realizzabile con una patch minima sulle toolchain di produzione.
• Complementarietà: Il meccanismo è ortogonale alla memorizzazione nella cache a livello di importazione (Livello 1). Mentre il Livello 1 evita il riavvio del server tra i teoremi, il Livello 2 elimina la rielaborazione del corpo del teorema tra i rami. Una futura variante del server persistente che combina entrambi potrebbe produrre ulteriori guadagni, ma l'implementazione attuale si concentra sul collo di bottiglia della distribuzione dei rami.

Gli autori sottolineano che questo è un intervento mirato per esporre la catena degli snapshot di elaborazione per il riutilizzo esterno, motivato dall'osservazione che il server Lean calcola e memorizza già questo stato nella cache per la diagnostica dell'IDE ma non riesce a esporlo agli orchestratori esterni di ricerca di prove.