Riepilogo Tecnico: Pythagoras-Prover

Definizione del Problema

I moderni dimostratori di teoremi Lean hanno raggiunto prestazioni elevate, ma dipendono pesantemente da un computo sostanziale durante l'addestramento e l'inferenza, richiedendo spesso modelli di frontiera (centinaia di miliardi di parametri) o procedure di inferenza computazionalmente intensive come la ricerca estensiva, l'auto-correzione e ampi budget di campionamento. Questa dipendenza è guidata dalla scarsità di dati di prova verificati e dai lunghi percorsi di ragionamento richiesti per la ricerca di prove formali, il che rende costosi il fine-tuning supervisionato (SFT) e il campionamento. Di conseguenza, esiste un divario significativo tra i piccoli dimostratori open-source e i loro omologhi più grandi, limitando l'accessibilità per ricercatori e professionisti privi di massicce risorse computazionali.

Metodologia

Gli autori introducono Pythagoras-Prover, una famiglia di dimostratori Lean 4 open-source computazionalmente efficienti. L'approccio si basa su una pipeline di dati a stadi e un risparmio di calcolo piuttosto che sulla scala bruta del modello.

1. Costruzione dei Dati e Apprendimento Curricolare (Curriculum Learning)

Il corpus di addestramento è costruito in tre livelli di difficoltà (Facile, Medio, Difficile), tutti controllati dal type-checker di Lean per garantirne la correttezza:

• Livelli Facile e Medio: Generati tramite una pipeline a tre stadi ispirata al concetto di "Theorem Prover as a Judge". Problemi in linguaggio naturale da dataset come DART-Math-Hard, DeepScaleR e OpenR1-Math vengono auto-formalizzati in enunciati Lean. Le prove fallite vengono analizzate e un processo di distillazione guidata da rubrica genera varianti sintetiche semplificate che mirano a specifiche categorie di errore (es. fallimenti dei tattici, discrepanze di tipo). Questo processo produce un miglioramento relativo del 30% nei tassi di successo dell'auto-formalizzazione.
• Livello Difficile: Tratto da problemi di livello competitivo (Olimpiadi, AIME, AMC) da Big-Math-RL-Verified. A differenza dei livelli più semplici, questi non vengono semplificati per preservarne la difficoltà ai fini dell'apprendimento per rinforzo (RL).
• Curriculum SFT: I modelli sono addestrati utilizzando un curriculum ordinato per difficoltà (Facile $\to$ Medio $\to$ Difficile) con LoRA (Low-Rank Adaptation) per mantenere l'efficienza dei parametri. Durante l'SFT viene applicato uno schema di filtraggio dinamico del ragionamento della prova per gestire il budget di contesto di 8k-token: se la catena di ragionamento più la prova eccedono il limite, il ragionamento viene scartato mantenendo la prova; se la sola prova eccede il limite, l'istanza viene scartata.

2. Formalizzazione Lean Aumentata (ALF) e Auto-distillazione

Per superare l'ostacolo del throughput di verifica di Lean, gli autori introducono la Formalizzazione Lean Aumentata (ALF).

• Meccanismo: ALF applica cinque operatori di mutazione strutturata (semplificazione, generalizzazione, proposta di lemma, decomposizione del passaggio di prova, riformulazione) a istanze seed verificate.
• Efficienza: Invece di verificare ogni istanza mutata con Lean (il che sarebbe computazionalmente proibitivo), ALF utilizza un controllo di allineamento dell'enunciato leggero. Verifica che la prova generata faccia riferimento allo statement mutato, garantendo la validità strutturale senza una compilazione completa.
• Auto-distillazione: Il modello post-RL genera prove per questi enunciati mutati. Questo espande il corpus di circa 2,5$\times$ (fino a ~2M di istanze) senza richiedere la verifica per singola istanza. Questo corpus espanso viene utilizzato per l'SFT continuato e per addestrare un dimostratore basato su diffusione.

3. Architetture dei Modelli

La famiglia comprende due paradigmi generativi:

• Dimostratori Autoregressivi: Modelli con 4B e 32B parametri addestrati con la pipeline sopra descritta.
• Dimostratore Basato su Diffusione: Pythagoras-Prover-Diffusion-4B, il primo dimostratore di teoremi basato su diffusione per Lean come prova di concetto. Utilizza il masking basato su tattiche, dove interi tattici Lean vengono mascherati e de-noizzati come unità, allineando l'obiettivo di de-noising ai passi di ragionamento discreti.

4. Apprendimento per Rinforzo (RL)

L'RL viene eseguito su problemi difficili tenuti fuori dal set di addestramento utilizzando GRPO (Group Relative Policy Optimization) con fine-tuning a parametri completi. La ricompensa è binaria (la prova compila e si allinea con l'enunciato). Gli autori osservano che l'RL produce solo guadagni modesti rispetto al modello curriculum-SFT, suggerendo che l'alta qualità del corpus supervisionato ha già interiorizzato un forte comportamento di ricerca della prova.

Contributi Chiave

1. Dimostratori Computazionalmente Efficienti: Una famiglia di dimostratori Lean open-source (4B, 32B e un modello di diffusione da 4B) che sfida l'assunto che il forte ragionamento formale richieda modelli di frontiera.
2. Pipeline di Dati ALF: Uno schema di mutazione strutturato che espande i corpora verificati di circa 2,5$\times$ utilizzando controlli di sanità leggera invece della verifica Lean per istanza, disaccoppiando l'espansione del corpus dal throughput del verificatore.
3. Benchmark MiniF2F-ALF: Un benchmark di perturbazione sensibile alla contaminazione creato applicando le mutazioni ALF al set MiniF2F-Test. Serve come test di stress per valutare se i modelli si affidano al richiamo esatto del benchmark o possiedono comportamenti di prova trasferibili.
4. Primo Dimostratore di Teoremi a Diffusione: Un viabile dimostratore basato su diffusione per Lean, che dimostra come la raffinazione iterativa sia una strategia di decodifica fattibile per le prove formali, sebbene con attuali limitazioni nella lunghezza del contesto.

Risultati Sperimentali

Valutati su MiniF2F-Test, PutnamBench e MiniF2F-ALF:

• MiniF2F-Test (Pass@32):
  • Pythagoras-Prover-4B raggiunge l'86,1%, superando DeepSeek-Prover-V2-671B (82,4%) nonostante sia circa 167$\times$ più piccolo. Supera anche Goedel-Prover-V2-8B (84,6%) e Kimina-Prover-70B (84,0%).
  • Pythagoras-Prover-32B raggiunge l'89,8%, guidando tutti i dimostratori open-source valutati senza auto-correzione.
• MiniF2F-Test (Pass@2048):
  • Pythagoras-Prover-32B raggiunge il 93,03%, stabilendo un nuovo stato dell'arte per i dimostratori neurali Lean a pesi aperti senza auto-correzione, superando Goedel-Prover-V2-32B (92,2% a Pass@8192) con un quarto del budget di campionamento.
• PutnamBench:
  • Pythagoras-Prover-32B risolve 93 su 672 problemi a Pass@2048, il miglior risultato open-source, superando Goedel-Prover-V2 (86 a Pass@184 con auto-correzione).
• MiniF2F-ALF (Robustezza):
  • Tutti i modelli valutati degradano su questo benchmark perturbato, confermando che l'alta accuratezza sullo split originale non garantisce la robustezza alle varianti strutturali.
  • Pythagoras-Prover-32B rimane il più forte (85,0%), e Pythagoras-Prover-4B (83,2%) raggiunge la parità con l'8$\times$ più grande Goedel-Prover-V2-32B (83,6%), degradando meno sotto perturbazione.
• Efficienza della Diffusione:
  • Pythagoras-Prover-Diffusion-4B raggiunge il 63,25% di Pass@32 su MiniF2F-Test. Sebbene meno accurato del suo controparte autoregressivo, genera prove 2,58$\times$ più velocemente (10,56 vs 4,10 token/sec), offrendo un maggiore throughput per GPU-secondo.

Significato e Rivendicazioni

L'articolo sostiene che il forte teorema di Lean non deve necessariamente affidarsi esclusivamente a modelli di frontiera. I risultati dimostrano che una costruzione attenta dei dati (apprendimento curricolare, aumento ALF, auto-distillazione) e ricette di addestramento efficienti (LoRA, filtraggio dinamico) possono sostituire, in parte, la scala bruta del modello.

Nello specifico, gli autori evidenziano:

• Efficienza: Pythagoras-Prover-4B supera un modello da 671 miliardi di parametri, suggerendo che la proposta ricetta di addestramento si trasferisce bene ai regimi di modelli piccoli dove i baselines da miliardi di parametri sono impraticabili.
• Robustezza: L'uso delle mutazioni ALF durante l'addestramento migliora la robustezza alle perturbazioni a livello di enunciato, come dimostrato dal minor calo di prestazioni su MiniF2F-ALF rispetto ai baselines.
• Nuovi Paradigmi: L'introduzione di un dimostratore basato su diffusione stabilisce un primo baseline per la raffinazione iterativa nelle prove formali, aprendo una direzione complementare dove i dimostratori possono essere confrontati per throughput e prove per GPU-secondo, non solo per accuratezza.

Gli autori concludono che la pipeline di dati "computazionalmente frugale" è il driver principale di questi risultati, consentendo prestazioni allo stato dell'arte sotto budget computazionali pratici.