Riepilogo Tecnico: OProver: Un Framework Unificato per la Dimostrazione Formale di Teoremi Agente

Enunciato del Problema

I recenti progressi nella dimostrazione formale di teoremi, in particolare all'interno dell'ecosistema Lean 4, hanno sfruttato la generazione di prove su larga scala e l'addestramento consapevole del verificatore per migliorare le prestazioni su benchmark come MiniF2F e PutnamBench. Tuttavia, persiste una limitazione critica: le capacità di dimostrazione agente (recupero, feedback del compilatore e riparazione iterativa) sono tipicamente trattate come euristiche applicate al momento dell'inferenza su un dimostratore fisso, piuttosto che come politiche apprese integrate nel processo di addestramento.

Ciò crea una disallineamento tra addestramento e inferenza. I modelli addestrati principalmente su prove finali e di successo incontrano il feedback del compilatore e il contesto recuperato solo durante la distribuzione, in distribuzioni per le quali non sono mai stati ottimizzati. Inoltre, i corpus formali esistenti si concentrano sui prodotti finali (enunciati e prove verificate), omettendo le storie di interazione multi-round—tentativi falliti, contesto recuperato e diagnosi del compilatore—essenziali per apprendere come riparare le prove. Di conseguenza, il segnale di supervisione che guida la riparazione delle prove nella pratica rimane in gran parte inutilizzato nell'addestramento del modello.

Metodologia

Il documento presenta OProver, un framework unificato che integra il recupero, il feedback del compilatore e la riparazione iterativa direttamente nella politica del dimostratore attraverso una pipeline di addestramento co-evolutiva.

1. Il Framework OProver

OProver tratta la dimostrazione di teoremi come un ciclo di raffinamento limitato e multi-round. Ad ogni round $t$, la politica $\pi$ si condiziona su uno stato compatto $X_t = (s, R_t, p_{t-1}, f_{t-1})$, dove:

• $s$: L'enunciato del teorema target.
• $R_t$: I top-$k$ prove recuperate e verificate dal compilatore da una memoria $M$.
• $p_{t-1}$: Il precedente tentativo di prova.
• $f_{t-1}$: Il feedback testuale grezzo del compilatore (diagnosi) dal verificatore Lean 4.

La politica genera un tentativo rivisto $p_t$. Se la verifica fallisce, il feedback grezzo viene passato alla politica per il round successivo. Crucialmente, la politica si condiziona solo sul tentativo e sul feedback più recenti, preservando i segnali di correzione locali mantenendo lo stato compatto.

2. OProofs: Un Corpus di Addestramento Unificato

Per supportare questo framework, gli autori costruiscono OProofs, un corpus su larga scala specificamente progettato per la dimostrazione agente. A differenza dei dataset precedenti che preservano solo le prove finali, OProofs registra traiettorie serializzate che includono:

• Contesto recuperato.
• Tentativi falliti.
• Feedback grezzo del compilatore.
• Riparazioni successive.

OProofs è costruito da tre fonti: risorse Lean pubbliche, sintesi di prove su larga scala (autoformalizzazione + verifica) e tracce dalla dimostrazione agente di OProver stesso. Contiene 1,77 milioni di enunciati Lean unici e 6,86 milioni di prove verificate dal compilatore, accoppiati a 1,07 milioni di traiettorie agenti.

3. Pipeline di Addestramento Co-evolutiva

Il processo di addestramento segue un ciclo iterativo (Algoritmo 1) in cui il dimostratore e il corpus co-evolvono:

1. Pretraining Continuo (CPT): Un modello base viene addestrato su un mix di codice Lean, matematica e dati di ragionamento a lungo contesto per creare OProver-Base.
2. Post-Training Iterativo:
   • Rollout Agente: La politica corrente esegue dimostrazioni multi-round su un pool di teoremi, recuperando dalla memoria corrente $M_k$ e verificando con il compilatore Lean.
   • Raccolta Dati: Le nuove prove verificate vengono aggiunte al corpus e indicizzate nella memoria di recupero. I tentativi falliti e le riparazioni di successo sono decomposti in esempi a livello di round $(s, R_t, p_{t-1}, f_{t-1}) \to p_t$.
   • Affinamento Supervisionato (SFT): Il modello viene aggiornato utilizzando gli esempi di riparazione raccolti.
   • Apprendimento per Rinforzo (RL): L'Ottimizzazione della Politica di Sequenza di Gruppo (GSPO) viene applicata ai casi irrisolti più difficili, utilizzando un segnale di ricompensa basato sul successo della verifica e sulla correttezza del formato.
   • Ricircolazione: Il corpus e la memoria aggiornati alimentano la prossima iterazione, permettendo alla politica di apprendere dalle proprie prove migliorate.

Contributi Chiave

1. Framework Unificato per la Dimostrazione Agente: OProver unifica recupero, feedback e riparazione iterativa in un'unica politica appresa, eliminando il disallineamento tra addestramento e inferenza addestrando il modello a utilizzare questi segnali come parte della sua strategia centrale piuttosto che come euristiche esterne.
2. Corpus OProofs: La costruzione di un corpus su larga scala (1,77 milioni di enunciati, 6,86 milioni di prove) che preserva esplicitamente le storie di interazione multi-turno, inclusi tentativi falliti e feedback grezzo del compilatore, fornendo una supervisione precedentemente non disponibile nei dataset formali.
3. Pipeline Co-evolutiva: Una metodologia di addestramento in cui il dimostratore genera nuovi dati (prove verificate e traiettorie di riparazione) che vengono immediatamente ripiegati nel corpus di addestramento e nella memoria di recupero, creando un ciclo di auto-miglioramento.
4. Prestazioni all'Avanguardia: OProver ottiene risultati di primo piano tra i dimostratori di prove complete a pesi aperti, dimostrando che le strategie di raffinamento agente possono superare modelli significativamente più grandi.

Risultati Sperimentali

OProver è stato valutato su cinque benchmark Lean 4: MiniF2F, MathOlympiadBench, ProofNet, ProverBench e PutnamBench.

• Prestazioni: Il modello OProver-32B ha ottenuto i migliori punteggi Pass@32 su tre benchmark (MiniF2F: 93,3%, ProverBench: 58,2%, PutnamBench: 11,3%) e il secondo migliore sugli altri due (MathOlympiad: 22,8%, ProofNet: 33,2%).
• Efficienza: OProver-32B (32 miliardi di parametri) ha superato il DeepSeek-Prover-V2 da 671 miliardi e il LongCat-Flash-Prover da 560 miliardi (con TIR) sulla maggior parte dei benchmark, nonostante abbia significativamente meno parametri. Anche la variante da 8 miliardi ha superato il Goedel-Prover-V2 da 32 miliardi su tutti i benchmark.
• Scalabilità al Tempo di Test: Le prestazioni sono migliorate costantemente con l'aumento dei budget computazionali (più campioni o round di raffinamento), sebbene con rendimenti decrescenti. L'allocazione ottimale tra profondità di raffinamento e larghezza di campionamento variava in base alla difficoltà del benchmark.
• Studi di Ablazione: La rimozione del feedback del compilatore multi-turno ha causato il degrado delle prestazioni più significativo, confermando il raffinamento iterativo come il principale motore dei guadagni. Anche la rimozione dell'aumento del recupero ha causato cali costanti, sebbene più piccoli, evidenziando il valore complementare del grounding tramite recupero.

Significato e Affermazioni

Il documento afferma che OProver dimostra che la dimostrazione formale di teoremi agente può essere appresa efficacemente come una politica unificata piuttosto che assemblata da moduli separati al momento dell'inferenza. Addestrandosi sull'intera traiettoria di costruzione della prova, fallimento e riparazione, il modello impara a sfruttare il feedback del compilatore e il contesto recuperato come parti intrinseche del suo processo di ragionamento.

Gli autori sottolineano che i guadagni di prestazioni non sono semplicemente il risultato della scala del modello, ma derivano dalla sinergia tra grounding aumentato dal recupero e raffinamento iterativo guidato dal compilatore. La co-evoluzione della politica OProver e del corpus OProofs permette al sistema di migliorare continuamente le proprie capacità di dimostrazione imparando dai propri tentativi di successo e falliti, stabilendo un nuovo paradigma per l'addestramento di sistemi di ragionamento formale.