Sintesi Tecnica: Apprendimento per Rinforzo Verificato dal Processo per la Dimostrazione di Teoremi tramite Lean

Definizione del Problema

La Dimostrazione Automatica di Teoremi (ATP) mira a generare dimostrazioni formali per teoremi matematici. Sebbene i Large Language Models (LLM) abbiano fatto progressi nei compiti di ragionamento, essi si affidano tipicamente al linguaggio naturale (NL) o a premi binari (corretto/errato) durante l'Apprendimento per Rinforzo (RL). Ciò crea un divario:

1. Feedback Sparso: Gli approoli standard di RL utilizzano spesso solo un segnale binario finale (dimostrazione superata/fallita), il che fornisce un assegnamento del credito scarso e fatica a guidare il modello attraverso lunghe catene di ragionamento.
2. Strutturato vs Non Strutturato: A differenza degli assistenti alla dimostrazione simbolica (es. Lean, Coq, Isabelle) che offrono una verifica fine-grained basata sulla teoria dei tipi di ogni passaggio del ragionamento, gli LLM sono addestrati su sequenze di token con ricompense scalari.
3. Modelli di Premio di Processo (PRM): Sebbene lavori recenti utilizzino i PRM per fornire ricompense a livello di passaggio, questi spesso richiedono dataset annotati massicci o si affidano a supervisioni CoT basate su NL, mancando della rigorosa correttezza della verifica simbolica.

La sfida centrale affrontata è come sfruttare il feedback ricco e strutturato di un assistente alla dimostrazione simbolica (Lean) per addestrare gli LLM senza fare affidamento su PRM esterni potenzialmente rumorosi o annotazioni umane.

Metodologia

Il documento propone il Process-Verified Reinforcement Learning, un framework che integra il feedback simbolico di Lean direttamente in un obiettivo di Group Relative Policy Optimization (GRPO). Il metodo consiste in tre componenti principali:

1. Oracolo di Processo Simbolico

Invece di trattare Lean solo come un verificatore finale, gli autori lo utilizzano come un oracolo di processo durante l'addestramento.

• Parsing: Le dimostrazioni generate vengono analizzate in sequenze di tattiche ($T_1, \dots, T_N$) basandosi sull'Albero di Sintassi Astratta (AST).
• Verifica: Il processo di elaborazione di Lean fornisce due tipi di segnali:
  • Segnale di Esito: Un punteggio binario globale $g(Y) \in \{0, 1\}$ che indica se l'intera dimostrazione è valida.
  • Segnale di Processo: Feedback fine-grained per ogni tattica, identificando i passaggi localmente corretti e la posizione specifica del primo errore.

2. Strategia di Assegnazione del Credito

Per colmare il divario tra il feedback simbolico e l'RL a livello di token, gli autori introducono regole di assegnazione specifiche:

• Propagazione del Primo Errore: Se una tattica $T_j$ fallisce, tutte le tattiche successive ($T_k$ dove $k \ge j$) sono considerate errate. Ciò riflette la natura causale delle dimostrazioni: un prefisso non valido invalida l'intera catena di ragionamento successiva.
• Scoring a Livello di Tattica ($\phi$):
  • Se la dimostrazione passa ($g(Y)=1$), tutte le tattiche ricevono un punteggio positivo (1).
  • Se la dimostrazione fallisce ($g(Y)=0$):
    • Le tattiche prima del primo errore ricevono un punteggio parziale ($d_1$).
    • La prima tattica errata e tutte le successive ricevono un punteggio di penalità ($d_2$).
• Mappatura a Livello di Token: L'advantage a livello di tattica viene assegnato solo al primo token di ogni tattica (la parola chiave, es. intro, apply). Ciò si allinea al punto decisionale semantico in cui viene determinata la strategia di dimostrazione.

3. Obiettivo di RL (Integrazione GRPO)

Il framework combina gli advantage di esito e di processo in un unico obiettivo GRPO:

• Advantage di Esito ($A_{outcome}$): Calcolato in base allo stato globale di successo/fallimento rispetto alla media del gruppo.
• Advantage di Processo ($A_{process}$): Calcolato in base ai punteggi a livello di tattica, normalizzati rispetto alla media del gruppo per tenere conto della difficoltà del problema.
• Advantage Combinato: Per un token $t$ appartenente al primo token della tattica $j$ nella risposta $i$:
  $$A_{i,t} = A_{outcome, i, t} + A_{process, i, j}$$
  Per i token non-primi, viene applicato solo l'advantage di esito. Questa formulazione evita la necessità di un modello di valore o di un PRM ausiliario, affidandosi esclusivamente al ground truth del verificatore.

Contributi Chiave

1. Formalizzazione del Feedback Simbolico: Gli autori formalizzano il feedback a livello di tattica di Lean in segnali di addestramento scalari, consentendo un assegnamento del credito fine-grained a livello di token senza guida in linguaggio naturale.
2. RL Guidato da Verificatore Simbolico: Integrano ricompense di esito e di tattica derivate direttamente da Lean in un framework di RL, fornendo un assegnamento del credito denso e verificabile.
3. Miglioramenti Stabili dei Benchmark: L'approccio dimostra miglioramenti costanti sui benchmark MiniF2F e ProofNet, superando l'RL basato solo sull'esito e i baseline vanilla senza richiedere PRM esterni o notazione NL.

Risultati Sperimentali

Gli esperimenti sono stati condotti utilizzando STP-Lean e DeepSeek-Prover-V1.5 (modelli da 7B) sui benchmark MiniF2F-Test e ProofNet-Test.

• Guadagni di Performance:
  • STP-Lean: Il metodo proposto ha migliorato il pass@64 di MiniF2F del +2,5% (da 56,7% a 59,2%) e il pass@32 di ProofNet del +1,4%.
  • DeepSeek-Prover-V1.5: Sono stati osservati miglioramenti costanti, seppur marginali, in tutte le configurazioni.
• Confronto con i Baseline:
  • Il metodo ha superato il GRPO "Outcome-only", che mostrava instabilità e non riusciva a migliorare su ProofNet in alcune configurazioni.
  • Ha ottenuto risultati competitivi rispetto a forti baseline di ricerca ad albero (es. InternLM2.5-StepProver, DeepSeek-Prover-RL+RMaxTS) utilizzando un approccio di generazione single-shot senza enormi budget di ricerca durante l'inferenza.
• Studi di Ablazione:
  • Assegnazione del Token: L'assegnazione del credito al primo token di una tattica ha prodotto i risultati più stabili rispetto alla distribuzione del credito su tutti i token o sull'ultimo token.
  • Propagazione del Primo Errore: La rimozione di questa regola ha degradato significativamente le prestazioni, confermando la necessità di trattare i passaggi successivi come non validi dopo un errore.
  • Timeout: Un timeout di verifica di 15 secondi ha fornito il miglior equilibrio, incoraggiando dimostrazioni concise senza scartare quelle complesse ma valide.

Significato e Rivendicazioni

L'articolo sostiene che gli assistenti alla dimostrazione simbolica non debbano essere visti solo come strumenti di valutazione, ma come oracoli attivi di premio a livello di processo durante l'addestramento. Sfruttando il "feedback strutturato ricco e fine-grained" intrinseco nei sistemi di ragionamento formale, gli autori dimostrano una strada verso i framework di RL che combinano la scalabilità degli LLM con l'affidabilità della verifica simbolica.

Lo studio evidenzia che:

• Segnali Densi e Verificabili: L'uso dei log di errore e degli alberi di elaborazione del prover fornisce un segnale di ricompensa denso e solido, superiore ai risultati binari sparsi o ai PRM appresi.
• Stabilità: La combinazione di ricompense di esito globale e ricompense di tattica locale stabilizza l'addestramento, prevenendo la convergenza prematura vista nel training solo su tattiche e i problemi di scarsità dell'addestramento basato solo sull'esito.
• Efficienza: Questo approccio raggiunge prestazioni allo stato dell'arte o competitive senza l'overhead computazionale della ricerca ad albero o i requisiti di dati per l'addestramento di separati PRM.

Gli autori rimangono modesti riguardo ai limiti, notando che il loro metodo si affida a punteggi di ricompensa fissi ($d_1, d_2$) piuttosto che a stimatori di advantage appresi e si concentra attualmente su dimostrazioni Lean pure e non-CoT, lasciando aperto il design dei premi per il ragionamento in linguaggio naturale a lungo formato.