💻 computer science

Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study

Questo studio rivela che i provatori di teoremi Lean addestrati con RL soffrono di collasso della modalità al momento dell'inferenza, che può essere efficacemente mitigato applicando un programma fisso di scheletri di tattiche diversificati per recuperare significativi guadagni di prestazioni, mentre il parafrasare i prompt e i commenti irrilevanti si rivelano inefficaci o dannosi.

Autori originali: Zachary Burton

Pubblicato 2026-05-19

📖 5 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Zachary Burton

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immagina uno studente brillante che è stato addestrato a risolvere puzzle matematici molto difficili utilizzando un linguaggio informatico speciale chiamato Lean. Questo studente, chiamiamolo "DeepSeek", è incredibilmente intelligente ma ha una strana abitudine: quando gli viene chiesto di risolvere un puzzle, rimane bloccato in un vicolo cieco mentale.

Questo articolo è una relazione diagnostica sul perché ciò accade e su come risolverlo. Ecco la storia di ciò che i ricercatori hanno scoperto, raccontata in termini quotidiani.

1. Il Problema: L'Effetto "Disco Rotto"

I ricercatori hanno notato che quando chiedevano a DeepSeek di risolvere lo stesso puzzle matematico ripetutamente (solo con semi casuali leggermente diversi, come lanciare i dadi), lo studente continuava a tentare esattamente lo stesso primo passo.

L'Analogia: Immagina di cercare di aprire una porta chiusa a chiave. Provi la chiave nella serratura. Non funziona. Provi di nuovo. Ancora non funziona. Provi una terza volta, e una centesima volta. Anche se provi 64 volte, stai solo inserendo la stessa chiave nella stessa serratura nello stesso modo. Non stai esplorando altre chiavi o altri modi per aprire la porta.
Il Risultato: Nello studio, raddoppiare il numero di tentativi da 32 a 64 non ha risolto un solo nuovo puzzle. Lo studente aveva subito un "collasso del modello": era bloccato su un percorso ristretto e non riusciva a pensare a nient'altro.

2. La Soluzione: Dare un "Primo Passo" come Suggerimento

I ricercatori hanno capito che lo studente non era pigro; era semplicemente troppo bloccato nella sua routine. Quindi, hanno provato un nuovo trucco: prima di chiedere allo studente di risolvere il puzzle, gli hanno dato un'istruzione specifica su come iniziare.

L'Analogia: Invece di dire semplicemente "Risolvi questo puzzle", i ricercatori dicevano "Inizia semplificando i numeri" o "Inizia introducendo una nuova variabile". È come dare allo studente una chiave specifica da provare per prima, invece di lasciarlo indovinare.
Il Risultato: Questo semplice stimolo ha rotto il vicolo cieco. Lo studente ha improvvisamente iniziato a risolvere molti più puzzle. Il "vicolo cieco" non era dovuto al fatto che lo studente fosse scarso in matematica; era dovuto al fatto che era troppo rigido nel modo in cui iniziava.

3. Il "Perché": È un Problema di Addestramento, Non di Cervello

I ricercatori volevano sapere: lo studente è naturalmente scarso in matematica, o è l'addestramento ad averlo reso rigido?

L'Esperimento: Hanno testato lo studente prima che ricevesse l'addestramento matematico speciale (il modello "Base").
La Scoperta: Lo studente non addestrato non riusciva a risolvere nessun puzzle. Si arrendeva semplicemente o ripeteva la domanda.
La Conclusione: L'addestramento speciale (Apprendimento per Rinforzo) è ciò che ha insegnato allo studente a risolvere i puzzle in primo luogo. Ma, quello stesso addestramento è anche ciò che lo ha reso rigido e bloccato in un vicolo cieco. L'addestramento ha creato l'abilità, ma ha anche creato il problema del "disco rotto".

4. Chi Altro Ha Questo Problema?

I ricercatori hanno testato altri "studenti" (diversi modelli di intelligenza artificiale) per vedere se questo fosse un problema universale.

Lo Studente "SFT": Uno studente era stato addestrato in modo diverso (Affinamento Supervisionato). Questo studente era in realtà migliore nel risolvere i puzzle in generale, ma non aveva il problema del "vicolo cieco". Quando i ricercatori gli davano suggerimenti, in realtà lo rendevano leggermente peggiore. Era già abbastanza flessibile da trovare la propria strada.
Gli Studenti "RL": Gli studenti addestrati con il metodo speciale "Apprendimento per Rinforzo" (come DeepSeek) erano quelli che rimanevano bloccati. Avevano bisogno dei suggerimenti sul "primo passo" per uscire dal loro pensiero ristretto.

5. La Prova del "Primo Movimento"

Per dimostrare che non si trattava solo di una coincidenza, i ricercatori hanno esaminato i veri e propri "primi movimenti" compiuti dagli studenti.

La Scoperta: Su 64 tentativi per un singolo puzzle, lo studente "bloccato" utilizzava esattamente lo stesso primo movimento in quasi la metà dei casi. Era incredibilmente prevedibile.
La Metafora: Se chiedessi a un umano di scrivere una storia 64 volte, potrebbe iniziare con "C'era una volta", "Il sole splendeva" o "Era una notte buia". Ma questo studente AI avrebbe iniziato con "C'era una volta" 32 volte e "Il sole splendeva" 30 volte. Aveva quasi nessuna varietà nella sua apertura.

Riepilogo

L'articolo conclude che l'Apprendimento per Rinforzo (un modo specifico di addestrare l'IA) crea un'arma a doppio taglio:

Insegna all'IA come dimostrare prove matematiche formali (cosa che non poteva fare prima).
Ma rende anche l'IA così focalizzata su alcune strategie "vincenti" da smettere di esplorarne di nuove.

La soluzione non è dare all'IA più potenza di calcolo o più tempo per pensare; è darle guida strutturale — un semplice stimolo su come iniziare la dimostrazione. Questo costringe l'IA a rompere la sua routine ed esplorare nuovi percorsi, sbloccando soluzioni che prima era troppo ostinata a trovare.

Riepilogo Tecnico: Diversità al Momento dell'Inferenza nei Teoremi Lean Addestrati con RL

Enunciato del Problema

I recenti teoremi neurali, in particolare quelli addestrati con Apprendimento per Rinforzo (RL) e ricompense verificabili (RLVR), hanno ottenuto prestazioni elevate su benchmark di prove formali come miniF2F. L'ipotesi prevalente è che un sufficiente addestramento RL e un aumento della potenza di calcolo al momento dell'inferenza (tramite campionamento i.i.d.) permettano ai modelli di interiorizzare i prior strutturali necessari per le prove formali.

Questo lavoro mette in discussione tale ipotesi, diagnosticando un fenomeno di collasso modale al momento dell'inferenza nei provatori Lean addestrati con RL. Nello specifico, gli autori osservano che l'aumento del budget di campionamento ( $k$ ) produce rendimenti decrescenti molto prima del previsto. Sul benchmark miniF2F-test con DeepSeek-Prover-V1.5-RL, raddoppiare il budget di campionamento da $k=32$ a $k=64$ produce zero teoremi risolti aggiuntivi (bloccati a 42/244). Il modello converge su un insieme ristretto di strategie di prova e fallisce nell'esplorare alternative, anche quando vengono forniti campioni stocastici aggiuntivi.

Metodologia

Lo studio impiega un framework diagnostico controllato utilizzando DeepSeek-Prover-V1.5-RL e la sua variante base non-RL, affiancati da confronti cross-modello con DeepSeek-Prover-V2-7B (RL) e Goedel-Prover (solo SFT).

1. L'Intervento dello Schema Scheletrico

Per verificare se il plateau sia dovuto a una mancanza di diversità strutturale piuttosto che a una mancanza di potenza di calcolo, gli autori introducono un programma fisso e deterministico di 15 scheletri di tattica.

Struttura: Una griglia $15 \times 8 = 120$ che combina 15 scheletri di tattica Lean selezionati a mano (es. simp, intro, constructor, aesop) con 8 commenti di suggerimento per l'obiettivo (suggerimenti in linguaggio naturale).
Esecuzione: Per un budget $k$ , il modello tenta le prime $k$ voci di questa griglia. Questo costringe il modello ad iniziare le prove con aperture strategiche specifiche invece di affidarsi al campionamento casuale.
Ablazioni: Per isolare la fonte del miglioramento, gli autori confrontano:
- B-RL (Scheletro): Il programma strutturato a 15 scheletri.
- C1 (Parafrasi): 16 parafrasi semanticamente equivalenti delle istruzioni (nessuna struttura di tattica).
- C2 (Commenti Irrilevanti): 16 commenti Lean privi di contenuto.
- C3 (Solo NL): Una condizione dedicata che utilizza solo suggerimenti in linguaggio naturale senza prefissi di tattica.

2. Stratificazione della Difficoltà

Gli autori definiscono un punteggio empirico di difficoltà di formalizzazione ( $\sigma$ ) utilizzando una costruzione leave-one-out. Per un teorema target, $\sigma$ conta quanti altri modelli di baseline (Goedel-Prover, V2-7B) lo risolvono senza intervento. Questo stratifica i teoremi in bucket: Frontier (non risolti da altri), Difficile, Medio, Facile e Triviale.

3. Misurazione Diretta Distribuzionale

Per andare oltre i plateau comportamentali, gli autori analizzano la diversità della testa della prima tattica su 13.159 campioni stocastici. Contano il numero di identificatori di tattica principali distinti (es. have, rw, norm_num) generati per teorema.

Risultati Chiave

1. Rottura del Plateau tramite Guida Strutturale

Collasso di Baseline: DeepSeek-Prover-V1.5-RL con campionamento i.i.d. risolve 38 teoremi a $k=16$ , 42 a $k=32$ , e rimane a 42 a $k=64$ .
Efficacia dello Scheletro: Il programma fisso di scheletri rompe questo plateau, risolvendo 55 teoremi a $k=16$ (+45% di miglioramento relativo) e continuando a trovare nuove prove fino a $k=64$ (60 totali).
Risultati delle Ablazioni:
- Struttura vs. Diversità: Le parafrasi delle istruzioni (C1) producono lo stesso pass@16 della baseline (38/244), mentre i commenti irrilevanti (C2) degradano le prestazioni a 25/244. Questo conferma che i guadagni sono guidati dalla guida strutturale, non dalla mera diversità del prompt.
- NL vs. Tattiche: La condizione solo NL (C3) risolve 48/244, intermedia tra baseline e scheletri completi. Ciò indica che i suggerimenti in linguaggio naturale recuperano circa il 58% del divario, mentre i prefissi letterali di tattica contribuiscono per la parte restante.

2. Localizzazione del Guadagno

Il guadagno strutturale è concentrato nei bucket Facile e Triviale (teoremi risolvibili da altri provatori open-source ma persi dal campionamento i.i.d. di V1.5-RL).

Nella colonna combinata Facile+Triviale, l'intervento dello scheletro produce un guadagno netto di +15, mentre le parafrasi producono 0 e i commenti irrilevanti producono -14.
Nessuna perturbazione sblocca il bucket "Frontier" (teoremi non risolti da alcuna baseline), suggerendo che l'intervento rimedia alla sottoesplorazione di problemi risolvibili noti piuttosto che espandere la frontiera della capacità.

3. Specificità RL del Collasso Modale

Contrasto Modello Base: DeepSeek-Prover-V1.5-Base (non-RL) dimostra zero teoremi in qualsiasi condizione (i.i.d. o scheletri). Ciò stabilisce che l'RL è il locus sia della capacità di prova che del successivo collasso modale. Il modello base manca della capacità di generare prove valide; la fase RL crea la capacità ma la collassa in una politica ristretta.
Contrasto Cross-Modello:
- V2-7B (RL): Mostra un guadagno aggregato piatto (+1) ma sblocca +3 teoremi frontier irraggiungibili da qualsiasi baseline i.i.d.
- Goedel-Prover (SFT): Mostra un guadagno negativo (-10.0 $\pm$ 4.4) con gli scheletri. I modelli addestrati con SFT sembrano già esplorare un ampio insieme di steli di tattica, rendendo il programma fisso di scheletri ridondante o restrittivo.

4. Evidenza Diretta del Collasso

L'analisi distribuzionale rivela che il teorema mediano riceve solo 2 teste di tattica distinte su 64 campioni, con il 49% del benchmark che riceve un'unica apertura strategica deterministica. L'entropia di Shannon osservata è $\le 8\%$ della capacità teorica, confermando un grave collasso modale.

Significato e Affermazioni

Il lavoro riformula la narrazione da "gli scheletri di tattica migliorano le prestazioni" a "i provatori addestrati con RL esplorano gravemente insufficientemente lo spazio delle tattiche al momento dell'inferenza".

RL come Agente Duale: Gli autori affermano che l'RL gioca un doppio ruolo: è la fase che crea la capacità di prova (poiché il modello base non ne ha alcuna) e simultaneamente la fase che collassa tale capacità su una politica ristretta.
Scalabilità al Momento dell'Inferenza: I risultati suggeriscono che scalare semplicemente la potenza di calcolo inferenziale tramite campionamento i.i.d. produce rendimenti decrescenti molto prima del previsto. La diversità strutturale (variare le strategie di prova tramite prompt) è un asse di scalabilità più efficiente.
Rimediabilità: Il collasso modale è specifico dei modelli addestrati con RL. I modelli addestrati con SFT non esibiscono lo stesso collasso recuperabile tramite suggerimenti strutturali; anzi, ne soffrono. Ciò implica che gli interventi futuri (regolarizzazione dell'entropia al momento dell'addestramento o recupero di scheletri al momento dell'inferenza) devono navigare il compromesso tra la creazione di capacità e il mantenimento della diversità.

Lo studio conclude che il "collasso modale" è un fenomeno reale, contingente alla pipeline, intrinseco al processo di fine-tuning RL nei domini di verifica formale, e che interventi strutturali fissi possono recuperare efficacemente l'esplorazione perduta senza richiedere addestramento aggiuntivo.