Sintesi Tecnica: Scoperta Auto-Supervisionata di Teoremi in un Sistema Assiomatico Formale

Definizione del Problema

Sebbene i recenti sistemi di IA, in particolare i Large Language Models (LLM), abbiano dimostrato progressi significativi nel ragionamento matematico, essi si affidano ampiamente a conoscenze pregresse fornite dall'uomo, come testi matematici, codice e librerie di teoremi esistenti. Una questione aperta critica rimane: un agente può scoprire autonomamente teoremi utili partendo esclusivamente dalle regole primitive di un sistema assiomatico formale, senza accesso a conoscenze pregresse umane, librerie di teoremi esistenti o set di problemi di addestramento?

I metodi attuali spesso dipendono dalla conoscenza costruita dall'uomo per avviare il ragionamento. Anche gli agenti auto-migliorabili in domini assiomatici spesso si affidano a giudici esterni per valutare l'utilità dei teoremi scoperti. Questo articolo investiga se un agente possa non solo scoprire teoremi, ma anche identificare e utilizzare quelli "utili" per migliorare la propria ricerca di prove e le prestazioni di sistemi di ragionamento esterni, basandosi esclusivamente su assiomi e regole di inferenza.

Metodologia

1. Impostazione Formale: Sistema di Hilbert come Macchina a Stack

Gli autori istanziano il problema all'interno di un sistema assiomatico di Hilbert per la logica proposizionale. Il sistema è deliberatamente minimale, composto da:

• Tre Assiomi:
  • $Ax1: A \to (B \to A)$ (Debolezza)
  • $Ax2: (A \to (B \to C)) \to ((A \to B) \to (A \to C))$ (Distribuzione)
  • $Ax3: (\neg A \to \neg B) \to (B \to A)$ (Contrapposizione)
• Una Regola di Inferenza: Modus Ponens (MP), derivando $Y$ da $X$ e $X \to Y$.

Per facilitare l'apprendimento, gli autori formulano la dimostrazione di teoremi come un processo decisionale deterministico, condizionato dall'obiettivo, di tipo macchina a stack $(S, A, s_0, P)$:

• Stato ($S$): Uno stack finito di formule.
• Azioni ($A$): Inserire istanze di $Ax1, Ax2, Ax3$ nello stack, oppure applicare il Modus Ponens (MP).
• Meccanismo: L'azione MP utilizza l'unificazione di Hindley–Milner. Se l'elemento in cima allo stack si unifica con $X \to Y$ e l'elemento sottostante si unifica con $X$, entrambi vengono rimossi dallo stack (pop) e $Y$ viene inserito (push).
• Successo: Una dimostrazione è considerata riuscita se lo stack contiene una singola formula che corrisponde all'obiettivo target.

2. Algoritmo di Scoperta di Teoremi Auto-Supervisionato

Il contributo principale è un algoritmo che alterna tra ricerca di prove ed estrazione di teoremi utili, costruendo una libreria di teoremi che fungono da lemmi per ricerche future.

A. Apprendimento della Policy Condizionato all'Obiettivo

L'agente apprende una policy $\pi_\theta(A|S, g)$ per predire l'azione successiva dato lo stack corrente $S$ e un obiettivo $g$.

• Hindsight Learning: Durante un episodio di ricerca, qualsiasi stato in cui lo stack contiene una singola formula $f_t$ è trattato come un "teorema raggiunto", indipendentemente dal fatto che fosse l'obiettivo originale.
• Segnale di Addestramento: Il prefisso di azioni che conduce a $f_t$ è trattato come una dimostrazione di $f_t$. Questi prefissi vengono aggiunti a un set di addestramento $D_{train}$ per aggiornare la policy tramite perdita di cross-entropia.
• Buffer degli Obiettivi ($G$): Un buffer mantiene i teoremi scoperti. L'agente campiona obiettivi uniformemente da $G$ per gli episodi di ricerca successivi, implementando efficacemente un proprio curriculum di bootstrapping.

B. Estrazione di Teoremi Utili

Per evitare che la libreria si gonfi di teoremi triviali o ridondanti, l'algoritmo filtra i teoremi scoperti basandosi su due criteri:

1. Generalità: I teoremi sono filtrati per rimuovere quelli che sono meri specializzazioni di altri candidati. Il sistema mantiene solo gli elementi "minimi" sotto un ordine parziale definito dalla sostituzione di formule (ovvero, mantenendo le forme più generali).
2. Riproducibilità: Il sistema stima la probabilità che la policy corrente possa ri-dimostrare un teorema. Utilizzando una media posteriore Bayesiana (Beta(1,1) prior), esso dà priorità ai teoremi che sono stati scoperti ma che sono difficili da ri-dimostrare in modo affidabile. Questi teoremi "difficili da ri-dimostrare" sono preziosi perché l'aggiunta di essi come lemmi comprime i percorsi di dimostrazione complessi.

C. Espansione della Libreria Multi-Generazionale

Il processo opera in generazioni:

1. Apprendimento della Policy: Addestramento della policy sullo spazio di azione corrente (inizialmente solo assiomi e MP).
2. Estrazione: Identificazione dei teoremi utili dal buffer degli obiettivi $G$ in base a generalità e riproducibilità.
3. Espansione dello Spazio di Azione: Aggiunta dei teoremi estratti come nuovi azioni di libreria (es. $Thm_1, Thm_2$). Quando selezionate, queste azioni inseriscono il corrispondente teorema nello stack, agendo come un lemma pre-verificato.
4. Iterazione: Ripetizione del processo, permettendo all'agente di usare i teoremi precedentemente scoperti per trovare nuovi teoremi più complessi.

Contributi Chiave

1. Formulazione: La dimostrazione di teoremi proposizionali è formulata come un processo decisionale a macchina a stack basato direttamente sugli assiomi di Hilbert e sulle regole di inferenza, evitando il ricorso a corpora di prove esterni.
2. Algoritmo: Viene proposto un algoritmo di scoperta di teoremi auto-supervisionato che espande la libreria di teoremi partendo dalle sole regole primitive. Riutilizza i teoremi estratti come lemmi per la ricerca di prove successiva.
3. Scoperta Autonoma: L'agente scopre decine di migliaia di teoremi e trova dimostrazioni per problemi di benchmark scritti da umani senza utilizzare prior umani per l'addestramento.
4. Trasferibilità: I teoremi estratti fungono da conoscenza esterna efficace, migliorando le prestazioni di ragionamento di LLM esterni quando forniti come lemmi nel prompt.

Risultati Sperimentali

1. Scoperta di Teoremi e Copertura

• Crescita: Il numero di teoremi scoperti aumenta su sei generazioni, dimostrando la capacità dell'agente di espandere autonomamente la propria base di conoscenza.
• Prestazioni sui Benchmark: L'agente trova con successo dimostrazioni nel sistema di Hilbert per il 30% di un set di benchmark scritto da umani (derivato dal testo di Kleene).
• Confronto: Mentre GPT-5-high (il baseline più forte) raggiunge solo circa il 23% di accuratezza su questi benchmark senza assistenza, la capacità dell'agente di trovare dimostrazioni per il 30% suggerisce che scopre dimostrazioni non banali che sono significative dal punto di vista matematico umano.

2. Impatto sul Ragionamento degli LLM

• Prompt Lemmata: Quando i teoremi estratti vengono forniti come lemmi nel prompt a varianti di GPT-4o e GPT-5, i loro tassi di successo nelle dimostrazioni sui problemi di benchmark migliorano significativamente.
• Analisi Qualitativa:
  • Alcuni teoremi scoperti corrispondono a principi ben noti (ad esempio, il principio di esplosione, $\neg A \to (A \to B)$), che sono facilmente interpretabili.
  • Altri (ad esempio, il complesso sollevamento delle implicazioni) non sono immediatamente ovvi per gli umani ma funzionano efficacemente come conoscenza di supporto nelle dimostrazioni degli LLM.
  • Ciò indica che l'agente può far emergere lemmi utili che gli umani non hanno esplicitamente fornito, e che questi lemmi sono trasferibili tra diverse architetture di ragionamento (dall'agente agli LLM).

Significato e Rivendicazioni

Il documento sostiene di fornire la prova che teoremi utili possono emergere dalla ricerca di prove senza fare affidamento su librerie di teoremi fornite dall'uomo.

• IA Auto-Evolutiva: Il lavoro suggerisce una strada verso sistemi di IA auto-evolventi per la matematica che possono espandere autonomamente la propria conoscenza formale attraverso la ricerca di prove, garantendo al contempo che ogni scoperta rimanga formalmente verificabile.
• Verificabilità Formale: A differenza degli LLM che possono allucinare affermazioni plausibili ma errate, le scoperte dell'agente sono strettamente ancorate agli assiomi e alle regole di inferenza del sistema di Hilbert.
• Modestia: Gli autori non pretendono di aver superato gli LLM allo stato dell'arte nel ragionamento generale. Invece, dimostrano che, in un contesto formale e ristretto, un agente può imparare a scoprire e utilizzare la propria conoscenza per risolvere problemi che sono difficili anche per gli LLM avanzati, e che tale conoscenza auto-scoperta può potenziare sistemi esterni.

Lo studio è limitato a un singolo sistema assiomatico (logica proposizionale di Hilbert), ma gli autori pongono che il framework sia generalizzabile a sistemi più ricchi come la logica del primo ordine o la teoria degli insiemi, il che rimane una direzione per il lavoro futuro.