Sintesi Tecnica: Misurazioni Geometriche dell'Assioma della Scelta negli Embedding di Prove Neurali

Definizione del Problema

L'assioma della scelta (AC) ha storicamente diviso le fondamenta matematiche in campi classici e costruttivi, una distinzione che rimane in gran parte filosofica e metodologica. Mentre le prove classiche utilizzano scorciatoie non costruttive consentite dall'AC, e le prove costruttive richiedono testimoni espliciti, non è stato chiaro se questi due paradigmi differiscano strutturalmente in modi rilevabili oltre la semplice dipendenza dagli assiomi. Questo articolo investiga se l'assioma della scelta lasci una "firma geometrica" misurabile nello spazio delle prove formali, specificamente all'interno della libreria Mathlib di Lean 4, e se tale firma abbia conseguenze operative per i dimostratori di teoremi neurali.

Metodologia

Partizionamento dei Dati e Tracciamento delle Dipendenze

Gli autori utilizzano il tracciamento della dipendenza dagli assiomi a livello di kernel di Lean 4 per partizionare la libreria Mathlib, che contiene 471.260 dichiarazioni certificate meccanicamente. Eseguendo una ricerca in ampiezza sul grafo delle dipendenze, classificano le dichiarazioni in due set:

1. Prove Classiche: Quelle che dipendono transitivamente da Classical.choice.
2. Prove Costruttive: Quelle che non vi dipendono.

La "distanza" di una prova classica è definita come la lunghezza della catena di dipendenza più breve da quella prova a Classical.choice. Ciò crea un dataset stratificato in cui le prove sono raggruppate per la loro profondità rispetto all'assioma. Lo studio si concentra su una popolazione filtrata di 42.355 teoremi (31.144 classici, 11.211 costruttivi) con tracce di tattiche compresi tra 2 e 200 passi.

Apprendimento di Rappresentazione Senza Etichette (Label-Free)

Per misurare le proprietà geometriche di queste prove senza pregiudizi, gli autori addestrano un autoencoder di denoising auto-supervisionato esclusivamente su prove costruttive.

• Input: Le prove sono rappresentate come sequenze di teste di tattiche (es. intro, rw, simp), scartando gli argomenti specifici per concentrarsi sulla composizione della prova.
• Architettura: Un encoder Transformer a 4 strati accoppiato con un decoder a 2 strati. Il modello è addestrato a ricostruire i token di tattica mascherati (corruzione del 20%) dalla sequenza di input.
• Embedding: L'embedding della prova è la media degli stati nascosti dell'encoder (escluso il padding), normalizzata sulla sfera unitaria.
• Vincolo Label-Free: L'encoder non vede mai prove classiche durante l'addestramento, la costruzione del vocabolario o la selezione degli iperparametri. Le prove classiche servono esclusivamente come popolazione di controllo (held-out).

Misurazioni Geometriche

Tre metriche complementari vengono utilizzate per misurare la divergenza delle prove classiche dalla distribuzione di addestramento delle prove costruttive in funzione della loro profondità di dipendenza:

1. Punteggio di Anomalia (k-NN): La distanza euclidea dai $k$ vicini costruttivi più prossimi.
2. Perdita di Ricostruzione (Reconstruction Loss): La perdita di cross-entropy incorreva quando il modello addestrato sulle costruttive tenta di predire i token mascherati in una prova classica.
3. Contenimento del Superlivello di Densità: La frazione di prove classiche che ricadono al di fuori della regione ad alta densità (superlevel set) definita dalla distribuzione di addestramento costruttiva.

Valutazione Operativa

Lo studio valuta l'impatto di queste scoperte geometriche sulle prestazioni del dimostratore di teoremi utilizzando due sistemi:

1. aesop: Un dimostratore di ricerca best-first simbolica.
2. Ibrido (ReProver + aesop): Un approccio guidato neuralmente dove un generatore di tattiche propone la prima mossa, seguito da aesop.

Risultati Chiave

La Legge della Profondità (The Depth Law)

Il principale risultato è l'esistenza di una "legge della profondità": la distinzione geometrica tra prove classiche e costruttive decade in modo prevedibile con la distanza da Classical.choice.

• Separazione Netta a Profondità Ridotte: Alla profondità 2 (prove che invocano direttamente lemmi classici), la separazione è forte. Il punteggio di anomalia k-NN raggiunge un AUC di 0,847, la perdita di ricostruzione è del 34,5% superiore rispetto alla baseline costruttiva, e il 43% delle prove classiche ricade al di fuori della regione di densità al 90% delle costruttive.
• Decadimento verso l'Indistinguibilità: All'aumentare della profondità, le metriche convergono verso la baseline costruttiva. Alla profondità 9+, tutte e tre le metriche si avvicinano ai livelli del caso (AUC $\approx$ 0,5, perdita $\approx$ baseline, contenimento $\approx$ 90%), rendendo le prove classiche profonde geometricamente indistinguibili da quelle costruttive.
• Legge di Miscelazione a Un Parametro: Gli autori modellano questo gradiente come una miscela di due distribuzioni: una distribuzione costruttiva $P$ e una distribuzione direttamente classica $R$. La distribuzione di profondità $d$, $Q_d$, è modellata come $Q_d = (1 - \lambda_d)P + \lambda_d R$, dove $\lambda_d$ è un peso di miscelazione che decresce con la profondità. Le tre misurazioni distinte collassano su un'unica curva quando normalizzate, supportando questa legge a un parametro.

Controlli di Robustezza

La firma è robusta rispetto a diversi potenziali fattori di confondimento:

• Parole Chiave: Rimuovere espliciti marcatori di tattiche classiche (es. classical, by contra) riduce l'AUC alla profondità 2 solo leggermente (da 0,847 a 0,754), indicando che il segnale è strutturale, non meramente lessicale.
• Lunghezza: La residualizzazione degli embedding rispetto alla lunghezza della prova non elimina il gradiente.
• Autore/File/Argomento: Modelli a effetti misti che controllano per autore, file e sottocampo matematico confermano che il segnale persiste all'interno di contesti specifici.
• Enunciato vs Prova: Gli enunciati dei teoremi mostrano un gradiente di profondità molto più debole (AUC 0,604 aggregato) rispetto alle prove (AUC 0,675 aggregato), confermando che il segnale è principalmente compositivo (struttura della prova) piuttosto che topico (contenuto del teorema).
• Specificità dell'Assioma: Sebbene propext e Quot.sound mostrino anch'essi gradienti di profondità, Classical.choice produce il gradiente più ripido, suggerendo un accoppiamento operativo unico con il ragionamento classico.

Conseguenze Operative

La firma geometrica correla con le prestazioni del dimostratore:

• Fallimento di aesop: aesop risolve il 20,0% dei teoremi costruttivi ma solo l'1,5% di quelli classici (un divario di 13×). A differenza del segnale geometrico, questo divario operativo non si smussa con la profondità; le prove classiche rimangono difficili per aesop indipendentemente dalla loro distanza dall'assioma.
• Guida Neurale: L'aggiunta di un generatore di tattiche neurale (ReProver) comprime il divario a circa 5× (22,0% vs 4,5%), ma non lo chiude.
• Potere Predittivo: Il punteggio di anomalia geometrica predice il fallimento di aesop significativamente meglio della sola lunghezza della prova (l'AUC aumenta da 0,766 a 0,841 aggiungendo il punteggio di anomalia).

Significato e Rivendicazioni

L'articolo sostiene di fornire la prima evidenza empirica che l'assioma della scelta abbia un correlato geometrico misurabile nello spazio delle prove. Gli autori argomentano che:

1. Distinzione Strutturale: La divisione classico/costruttivo non è solo una posizione filosofica, ma una proprietà strutturale della composizione delle prove che è visibile negli embedding neurali.
2. Rilevanza Operativa: Questa firma geometrica non è una mera curiosità astratta; predice le prestazioni dei dimostratori di teoremi automatizzati. La "legge della profondità" suggerisce che, man mano che le prove si allontanano dall'assioma, diventano strutturalmente più simili alle prove costruttive, eppure la barriera operativa per i dimostratori simbolici come aesop rimane specifica per la presenza di Classical.choice.
3. Contributo Metodologico: Il lavoro dimosta che l'apprendimento auto-supervisionato label-free su una singola classe (prove costruttive) può rivelare i confini strutturali di una classe tenuta in riserva (prove classiche) definita dalla dipendenza logica, offrendo un nuovo strumento per l'analisi meta-matematica.

Gli autori rimangono modesti riguardo ai meccanismi causali, notando che, sebbene il segnale geometrico e il divario operativo siano fortemente associati, la causa specifica della difficoltà del dimostratore (barriera strutturale vs configurazione dell'insieme di regole) richiede ulteriori indagini. Il lavoro è presentato come un invito alla comunità per identificare assi strutturali simili nelle librerie formali.