Benchmarking Testing in Automated Theorem Proving

1. Enunciato del Problema

Il rapido avanzamento dei Large Language Models (LLM) ha migliorato la loro capacità di generare dimostrazioni formali in sistemi come Lean. Tuttavia, i metodi di valutazione attuali soffrono di un difetto critico: confondono la validità sintattica con la correttezza semantica.

• Il Limite della Compilazione: I benchmark esistenti (ad esempio MiniF2F, ProofNet) valutano principalmente i modelli verificando se un teorema generato viene compilato. Sebbene la compilazione verifichi che il codice sia sintatticamente valido e logicamente coerente in isolamento, non garantisce che il teorema catturi il significato matematico inteso.
• Il Problema della "Tautologia": Un modello può generare una tautologia banale (ad esempio, $a + b = a + b$) che viene compilata con successo ma fallisce nel dimostrare l'affermazione non banale intesa (ad esempio, la commutatività $a + b = b + a$).
• Inadeguatezza dei Proxy: I tentativi esistenti di misurare la correttezza semantica si basano su proxy inaffidabili come la sovrapposizione lessicale (punteggi BLEU) rispetto a riferimenti annotati manualmente o ispezione manuale. Questi metodi sono o rumorosi, richiedono costosa manodopera umana, o non riescono a distinguere tra significati semantici corretti e scorretti.

2. Metodologia

Gli autori propongono un cambio di paradigma ispirato al testing di integrazione nell'ingegneria del software. Invece di valutare un teorema in isolamento, lo valutano in base a come interagisce con il resto della base di codice.

Concetto Chiave: Theorem Testing (T2)

Attingendo alla corrispondenza di Curry-Howard (dove le dimostrazioni corrispondono ai programmi), gli autori trattano un teorema generato come una funzione e i teoremi che dipendono da esso come "casi di test".

• Grafo delle Dipendenze: Costruiscono un grafo delle dipendenze in cui un teorema target ($t_{GT}$) ha predecessori (definizioni/lemmi che utilizza) e successori (teoremi che lo invocano o si basano su di esso).
• Logica del Testing di Integrazione: Se un teorema generato ($t_{fl}$) è semanticamente scorretto (ad esempio, definisce una tautologia invece della proprietà intesa), qualsiasi teorema successore che si basa su di esso fallirà nella compilazione.
• Analogia con l'Eliminazione del Taglio: Il processo è formalmente fondato sul principio logico dell'Eliminazione del Taglio. Se una catena di dimostrazioni ($X \to Y \to Z \to W$) fallisce quando il lemma intermedio ($Y$) viene sostituito da un candidato generato, il candidato è semanticamente scorretto.

Il Benchmark T2

Gli autori hanno costruito un benchmark su larga scala, T2, per facilitare questa valutazione:

• Fonte: Estratto da 5 repository reali di Lean 4 (che coprono algebra, topologia, teoria dei numeri, ecc.).
• Scala: 2.206 problemi, ciascuno accoppiato con una media di 41 teoremi successori.
• Sottoinsieme Hard: Un sottoinsieme di 389 problemi "Hard" in cui il modello deve generare sia la proposizione (affermazione) che la dimostrazione, anziché semplicemente completare una dimostrazione per un'affermazione data.
• Automazione: La pipeline di estrazione è completamente automatizzata, non richiedendo annotazione umana per la struttura delle dipendenze. Le descrizioni in linguaggio naturale (NL) sono state generate da un LLM potente (Claude Sonnet 4.5) e verificate manualmente su un campione.

La Metrica: Testing Accuracy (TA)

Il paper introduce l'Testing Accuracy (TA) come metrica di valutazione primaria:
$$TA = E_{P \sim D} \left[ \prod_{i=1}^{k} \text{compiles}(t^{(i)}_{succ} \mid t_{fl}) \right]$$
Un teorema generato supera la prova solo se tutti i suoi teoremi successori dipendenti vengono compilati con successo quando il teorema originale viene sostituito con quello generato.

3. Contributi Chiave

1. Benchmark T2: Il primo benchmark su larga scala, ricco di dipendenze, per la dimostrazione di teoremi formali che va oltre i problemi isolati per abbracciare contesti di repository reali.
2. Testing Accuracy (TA): Una metrica nuova, automatica e priva di riferimenti che verifica direttamente la correttezza semantica attraverso la compilazione dei moduli dipendenti.
3. Analisi del Divario Empirico: Valutazione completa di 18 modelli all'avanguardia (sia open che closed-source) che rivela un enorme disallineamento tra il successo della compilazione e la correttezza semantica.
4. Insight Contestuali: Ha dimostrato che fornire i teoremi successori come contesto migliora significativamente la correttezza semantica, mentre fornire solo dimostrazioni in linguaggio naturale non lo fa.

4. Risultati Sperimentali

Gli autori hanno valutato 18 modelli (inclusi GPT-5, Claude-Sonnet-4.5, Llama-3.1 e modelli matematici specializzati come DeepSeek-Prover) sul benchmark T2.

• Il Divario Semantico:

  • Accuratezza di Compilazione: I modelli hanno ottenuto tassi di compilazione elevati (ad esempio, Claude-Sonnet-4.5: 80,3% sull'insieme completo).
  • Testing Accuracy (TA): Gli stessi modelli hanno ottenuto punteggi TA drasticamente più bassi (ad esempio, Claude-Sonnet-4.5: 38,9% sull'insieme completo; 4,5% sull'insieme Hard).
  • Falsi Positivi: Fino al 93,1% dei teoremi compilabili si è rivelato semanticamente scorretto quando testato contro i successori.

• Fallimento delle Metriche Esistenti:

  • BLEU: Un'alta similarità lessicale (punteggi BLEU) ha mostrato quasi nessuna correlazione con la correttezza semantica (Correlazione: 0,123). I modelli potevano generare dimostrazioni testualmente simili ma logicamente errate.
  • Modelli Specializzati: I modelli fine-tunati specificamente per la dimostrazione di teoremi hanno spesso ottenuto tassi di compilazione più alti, ma hanno performato peggio o allo stesso modo dei modelli generici sulla TA, suggerendo che si sovrappongono alla sintassi piuttosto che alla semantica.

• Impatto del Contesto:

  • Fornire i Teoremi Successori come contesto di input ha migliorato costantemente la TA (ad esempio, +4,9% per Claude-Sonnet-4.5).
  • Fornire solo Dimostrazioni NL senza successori non ha migliorato le prestazioni e talvolta le ha degradate.
  • Il few-shot prompting e la rifinitura iterativa (utilizzando feedback del compilatore) hanno prodotto miglioramenti trascurabili sull'insieme Hard, indicando che la difficoltà risiede nel ragionamento semantico profondo, non solo nel formato del compito.

5. Significato e Conclusione

Questo paper sfida fondamentalmente lo stato attuale della valutazione dell'Automated Theorem Proving (ATP).

• Ridefinire il Successo: Dimostra che la "compilazione" è una condizione necessaria ma non sufficiente per la generazione di teoremi. Un modello può essere sintatticamente perfetto ma semanticamente inutile.
• Affidabilità: Il benchmark T2 e la metrica TA forniscono un modo rigoroso e automatico per valutare se un LLM comprende davvero i concetti matematici o sta semplicemente allucinando codice sintatticamente valido.
• Direzione Futura: Il lavoro suggerisce che i futuri sistemi ATP devono essere valutati sulla loro capacità di integrarsi in basi di codice esistenti (generazione consapevole delle dipendenze) piuttosto che risolvere enigmi isolati. Sottolinea inoltre che fornire la "suite di test" (teoremi successori) al modello durante la generazione è una strategia cruciale per migliorare l'allineamento semantico.

In sintesi, il paper sostiene che il testing di integrazione è l'anello mancante nella valutazione degli LLM per la matematica formale, rivelando che i modelli attuali all'avanguardia sono lontani dal raggiungere una correttezza semantica affidabile nella dimostrazione di teoremi.