Riepilogo Tecnico: Leggi di Scalatura Saturanti per la Scoperta Equazionale

Enunciato del Problema

Il documento indaga se i sistemi deterministici di scoperta simbolica, in particolare quelli che crescono aggiungendo regole di riscrittura equazionale, obbediscano a leggi di scalatura empiriche analoghe a quelle riscontrate nei grandi modelli linguistici (LLM). Sebbene le leggi di scalatura per i modelli neurali (Kaplan et al., 2020; Hoffmann et al., 2022) siano ben consolidate, rimane una questione aperta se i substrati deterministici, come quelli utilizzati nella programmazione logica induttiva, nella saturazione dell'uguaglianza e nella sintesi di programmi, seguano dinamiche di crescita comparabili. Gli autori mirano a caratterizzare la fenomenologia della crescita in questi sistemi, testando se una semplice legge di potenza o una funzione saturante più complessa descriva meglio l'accumulo di regole scoperte nel tempo.

Metodologia

Lo studio impiega un quadro sperimentale controllato che coinvolge tre substrati deterministici "di esempio" (toy) di crescente complessità di tipizzazione:

1. Aritmetica (arith): Identità equazionali su una grammatica tipizzata con addizione, moltiplicazione e variabili libere.
2. Booleana (bool): Identità su operatori logici (and, or, not).
3. Lista di Ordine Superiore (list): Un dominio ispirato a DreamCoder con primitive come map, fold e cons.

Il Ciclo di Scoperta:
Il sistema fa crescere un substrato $S$ (un insieme di regole di riscrittura) in passi discreti $t$. Ad ogni passo:

• Un generatore propone equazioni candidate basate sullo stato corrente di $S$ (utilizzando strategie come casuale, composizionale, ponderata per frequenza o MDL-greedy).
• I candidati sono testati per correttezza semantica tramite istanziazione casuale.
• Le coppie accettate sono generalizzate (sostituendo le variabili libere con variabili di pattern).
• Un filtro di accettazione configurabile ("qualsiasi" o "novità") determina se la regola viene assegnata a $S$.

Raccolta Dati:
Gli autori hanno generato 592 traiettorie di scoperta indipendenti su questi substrati, variando cinque caratteristiche architetturali: tipo di generatore, rigidità del filtro, profondità di ricorsione, dimensione del batch e seed casuale. Hanno misurato il conteggio totale delle regole $|S(t)|$ nel tempo.

Approccio di Modellazione:
Gli autori propongono un modello euristico di chiusura di campo medio derivato da assunzioni di copertura uniforme e indipendenza approssimata. Ciò produce un'equazione differenziale per la crescita:
$$\frac{dN}{dt} = K \cdot N^k \cdot e^{-\mu N}$$
dove $N$ è la dimensione del substrato, $k$ è correlata alla profondità di ricombinazione del generatore e $\mu$ rappresenta la frazione di copertura dello spazio dei candidati.

• Breve raggio ($\mu N \ll 1$): L'equazione approssima una pura legge di potenza $N(t) \propto t^b$, dove $b = 1/(1-k)$.
• Lungo raggio ($\mu N \gtrsim 1$): Il termine esponenziale induce saturazione, modellata da una forma di legge di potenza logistica.

Lo studio adatta tre modelli candidati (pura legge di potenza, esponenziale allungato, legge di potenza saturante) ai dati utilizzando l'AIC per la selezione del modello e la regressione con gradient boosting per prevedere l'esponente $b$ dalle caratteristiche architetturali.

Contributi e Risultati Chiave

1. Dinamiche di Legge di Potenza a Breve Raggio

Su 592 traiettorie, la crescita della dimensione del substrato $|S(t)|$ a brevi distanze (fino a 30 epoche) si adatta coerentemente a una forma di legge di potenza $t^b$. L'esponente $b$ varia continuamente tra 0 e 1,15 a seconda del dominio e dell'architettura.

• Sensibilità Architetturale: All'interno di un singolo substrato, l'esponente $b$ è altamente sensibile alle scelte architetturali. Un regressore con gradient boosting che utilizza cinque caratteristiche architetturali prevede $b$ con un $R^2$ convalidato incrociatamente $\approx 0,82$ sia per i domini aritmetici/booleani che per quello delle liste.
• Fallimento del Trasferimento Cross-Substrato: Un modello addestrato per prevedere $b$ su dati aritmetici e booleani fallisce completamente quando applicato al dominio delle liste ($R^2 \approx -0,84$). L'architettura ottimale per la crescita composta in substrati a tipizzazione piatta (ad esempio, filtri di novità) sopprime la crescita nei substrati a tipizzazione di ordine superiore. Ciò indica che le dinamiche di crescita sono condizionate dal substrato, non universali.

2. Ipotesi di Saturazione a Lungo Raggio

Gli autori hanno testato se la crescita satura eventualmente come previsto dal loro modello di chiusura.

• Dati di Esempio (Dominio delle Liste): Estendendo cinque traiettorie del dominio delle liste a 500 epoche, il modello di legge di potenza saturante vince nei confronti AIC in-sample per traiettorie superiori a 200 epoche. Tuttavia, la previsione out-of-sample (adattamento sui primi 100 epoche e previsione delle successive 400) è vinta dalla pura legge di potenza in tutti i 5 casi. Gli autori concludono che le traiettorie di esempio non raggiungono effettivamente il regime di saturazione entro 500 epoche; la preferenza del modello saturante in-sample è probabilmente un artefatto di adattamento che extrapola male.
• Dati Reali (Mathlib4): L'analisi degli aggiustamenti mensili di nuovi file .lean nella libreria Mathlib4 (60 mesi, 9.701 file) supporta la forma saturante. Il modello saturante supera la pura legge di potenza nella previsione out-of-sample di un fattore di $\sim 7\times$ (RMSE 3.279 contro 23.896), suggerendo che Mathlib4 ha raggiunto un regime di saturazione.
• Dati Reali (Coq Mathcomp): L'analisi dei commit mensili nella libreria Coq Mathcomp (129 mesi) favorisce la pura legge di potenza. Il parametro di saturazione $\mu$ collassa a zero e la pura legge di potenza supera il modello saturante nella previsione out-of-sample di $\sim 67\times$. Ciò suggerisce che Mathcomp non ha ancora raggiunto un regime di saturazione.

3. Inquadramento Fenomenologico

Il documento propone un inquadramento operativo: "Crescita a legge di potenza saturante con $(k, \mu)$ condizionati dal substrato, osservabile quando il substrato ha raggiunto il proprio regime di saturazione". Le dinamiche sono condizionate a due livelli:

1. I parametri architetturali che prevedono l'esponente di crescita non si trasferiscono tra diversi tipi di substrato.
2. La famiglia funzionale che descrive la crescita (pura vs. legge di potenza saturante) dipende dallo specifico stadio del ciclo di vita del substrato.

Significato e Affermazioni

Il documento si posiziona come la prima indagine empirica e teorica sulle leggi di scalatura della scoperta equazionale deterministica, offrendo una fenomenologia piuttosto che una teoria definitiva.

• Portata Modesta: Gli autori dichiarano esplicitamente che le prove sono limitate a tre substrati di esempio e due proxy reali (che sono grossolani, basati su conteggi di commit/file). Riconoscono che i risultati a lungo raggio sui dati di esempio sono "coerenti con, non confermati" a causa del fallimento della previsione out-of-sample sui dati di esempio.
• Insight Chiave: La scoperta principale è che le dinamiche di scoperta simbolica sono condizionate dal substrato. A differenza delle leggi di scalatura neurali che spesso assumono universalità tra le architetture, il comportamento di crescita qui dipende fortemente dalla specifica "geometria di chiusura" (parametro di copertura $\mu$) del sistema di tipi del substrato.
• Direzioni Future: Gli autori identificano tre aggiornamenti concreti necessari per elevare questo lavoro da "fenomenologia di esempio" a "fenomeno genuino":
  1. Riproduzione su un substrato non di esempio con granularità a livello di traiettoria (non solo conteggi di commit).
  2. Previsione predittiva out-of-sample di successo per il modello saturante.
  3. Una derivazione teorica del parametro di saturazione $\mu$ dalla combinatoria del substrato (ad esempio, entropia dei tipi) per rendere falsificabile il trasferimento cross-substrato.

Il documento conclude che, sebbene il quadro della legge di potenza saturante sia coerente con i dati osservati in regimi in cui la saturazione è plausibile, non è una legge universale per tutti i sistemi di scoperta simbolica. Il lavoro serve come punto di partenza per una potenziale "meccanica statistica della scoperta simbolica".