Riepilogo Tecnico: CAM-Bench

Enunciato del Problema

I benchmark esistenti per la dimostrazione di teoremi formali destinati ai Large Language Models (LLM) si concentrano prevalentemente su problemi in stile olimpico e su domini algebrici (ad esempio, MiniF2F, PutnamBench, ProofNet). Sebbene questi benchmark abbiano guidato i progressi nel ragionamento formale, lasciano la matematica computazionale e applicata significativamente sottorappresentata.

I problemi di matematica applicata (ad esempio, ottimizzazione, algebra lineare numerica, analisi numerica) differiscono fondamentalmente dalle enunciazioni di teoremi isolate. Sono spesso dipendenti dal contesto, basandosi su:

• Definizioni, notazioni e algoritmi introdotti localmente.
• Convenzioni e risultati elementari specifici del capitolo.
• Assunzioni ereditate che non sono esplicitamente dichiarate nell'esercizio ma sono necessarie per una formalizzazione fedele.

I benchmark attuali faticano a valutare se i modelli possano tracciare queste assunzioni locali, decomporre le dimostrazioni in base ai contesti dei manuali e applicare risultati elementari che non sono ancora disponibili come lemmi standard in librerie formali come Mathlib4. C'è la necessità di un benchmark che miri a problemi di matematica applicata in cui il "contesto locale" è critico quanto l'enunciazione del teorema stesso.

Metodologia

Gli autori introducono CAM-Bench, un benchmark per la dimostrazione di teoremi in Lean 4 composto da 1.000 obiettivi di dimostrazione derivati da 778 esercizi tratti da manuali di ottimizzazione, algebra lineare numerica e analisi numerica. La costruzione di questo benchmark si basa su una nuova pipeline di recupero delle dipendenze e formalizzazione progettata per trasformare esercizi dipendenti dal contesto in obiettivi autonomi e verificabili da macchine.

1. Pipeline di Recupero e Arricchimento delle Dipendenze

Per affrontare la natura non autonoma degli esercizi tratti dai manuali, gli autori hanno sviluppato una procedura ricorsiva di espansione delle dipendenze (Algoritmo 1):

• Espansione Ricorsiva: Partendo da un esercizio grezzo, il sistema estrae i riferimenti (teoremi, equazioni, algoritmi) e recupera ricorsivamente le loro definizioni e dipendenze fino a una profondità limitata.
• Naturalizzazione dal Basso verso l'Alto: L'albero delle dipendenze viene elaborato dal basso verso l'alto. Un naturalizzatore LLM unisce le rappresentazioni arricchite, risolvendo i riferimenti locali, standardizzando la notazione e fluidificando le transizioni per garantire che le definizioni di livello inferiore siano incorporate prima che le dipendenze di livello superiore le utilizzino.
• Recupero delle Condizioni Implicite: Il sistema rende esplicite le assunzioni richieste (ad esempio, restrizioni di dominio, positività, convessità) solo quando supportate dal problema originale o dal contesto recuperato. Questo arricchimento è radicato nella fonte; non congetturare dipendenze mancanti, ma le esclude se non possono essere recuperate.
• Revisione Multi-Round: Le enunciazioni arricchite subiscono un ciclo di validazione per verificare la presenza di assunzioni mancanti, deviazioni dal compito e idoneità a Lean. Le riparazioni sono vincolate a correggere difetti locali senza alterare l'obiettivo matematico o inventare dipendenze non supportate.

2. Formalizzazione in Lean Guidata dalla Modularizzazione

Una volta stabilito un obiettivo informale, il sistema lo converte in codice Lean 4 utilizzando una strategia di costruzione a blocchi con contesto congelato:

• Decomposizione Semantica a Blocchi: Gli esercizi eterogenei sono decomposti in blocchi semantici tipizzati (definizioni, problemi di ottimizzazione, algoritmi, obiettivi di teorema). Questo separa il contesto di supporto dall'obiettivo finale del teorema.
• Traduzione Incrementale: Il sistema traduce i blocchi in sequenza. Le dichiarazioni precedentemente accettate vengono mantenute come contesto congelato e in sola lettura. Questo previene errori a cascata e localizza i fallimenti al blocco corrente.
• Riparazione Guidata dal Compilatore e Semantica:
  • Riparazione della Compilazione: Se un blocco non riesce a compilare, un correttore utilizza i diagnostici del compilatore per generare patch locali (sintassi, annotazioni di tipo, risoluzione degli spazi dei nomi).
  • Revisione Semantica: Un revisore confronta il candidato compilabile con il blocco informale per garantire la fedeltà semantica (preservando variabili, assunzioni e conclusioni). Le discrepanze attivano una riscrittura semantica.
• Controllo Consapevole della Cronologia: Il sistema mantiene una cronologia dei tentativi falliti e delle ragioni di rifiuto per prevenire l'oscillazione e guidare le riparazioni successive lontano dalle direzioni precedentemente fallite.

3. Costruzione e Validazione del Benchmark

Il dataset finale include l'esercizio grezzo, il contesto recuperato, il teorema informale normalizzato e l'obiettivo Lean finale. La validazione avviene a due livelli:

• Livello Sorgente: Garantisce che l'obiettivo informale sia fedele all'esercizio del manuale e autonomo.
• Livello Lean: Garantisce che la dichiarazione formale preservi l'obiettivo informale revisionato. Solo il 92,5% delle dichiarazioni candidate è stato giudicato utilizzabile dopo la validazione semantica, evidenziando la difficoltà della autoformalizzazione fedele.

Contributi Chiave

1. Dataset CAM-Bench: Un benchmark curato di 1.000 obiettivi di dimostrazione in Lean che coprono ottimizzazione, algebra lineare numerica e analisi numerica. Fornisce artefatti tracciabili dagli esercizi grezzi agli obiettivi Lean verificati da macchine, colmando il vuoto nella valutazione della matematica applicata.
2. Pipeline di Recupero delle Dipendenze: Un metodo innovativo per costruire obiettivi Lean fedeli da esercizi dipendenti dal contesto. Combina espansione ricorsiva delle dipendenze, arricchimento radicato nella fonte e riparazione vincolata per gestire definizioni e assunzioni locali che non sono lemmi standard di Mathlib4.
3. Valutazione Completa e Analisi degli Errori: Il documento valuta i LLM all'avanguardia e gli agenti di formalizzazione su CAM-Bench. Identifica specifici modi di fallimento:
   • Grounding Libreria/API: I modelli non riescono a fondare le dimostrazioni nell'infrastruttura Mathlib disponibile, allucinando API o mancando risultati ponte.
   • Rappresentazione Formale: Errori nella disciplina dei tipi, mismatch di dimensioni/indici e fallimenti di coercizione.
   • Decomposizione della Dimostrazione: Incapacità di decomporre dimostrazioni a lungo orizzonte in lemmi ausiliari o di mantenere il controllo su argomenti complessi di ottimizzazione/numerici.

Risultati

Prestazioni di Base

• Modelli Non-Agentici: Anche le basi non-agentiche più forti (ad esempio, Deepseek-v4-pro, Claude-sonnet-4-6) hanno raggiunto una bassa accuratezza verificata in Lean, con la migliore che ha raggiunto il 19,67% (Pass@32).
• Divario Informale vs Formale: Esiste una significativa discrepanza tra la correttezza informale (accuratezza Pass@1 informale ~70–84%) e la correttezza Lean verificata (<20%). I modelli catturano argomenti di alto livello ma falliscono nel soddisfare la sintassi rigorosa di Lean, la disciplina dei tipi e i vincoli della libreria.
• Miglioramento Agentico: I sistemi di ricerca di dimostrazioni agentici (ad esempio, GPT-5.4 con riparazione iterativa e uso di strumenti) hanno migliorato significativamente le prestazioni, raggiungendo un'accuratezza verificata del 44,00%. Tuttavia, ciò è avvenuto a un costo elevato di token (~1,96M token contro ~0,26–0,70M per le basi).

Valutazione di Agenti Esterni

Due sistemi agentici esterni, M2F e Aristotle, sono stati valutati su 200 istanze campionate con un budget di tempo di 8 ore:

• M2F: Ha risolto 143/200 istanze (71,5%).
• Aristotle: Ha risolto 125/200 istanze (62,5%).
• Nonostante questi miglioramenti, il benchmark rimane non saturato. Molti fallimenti sono stati attribuiti a infrastrutture matematiche mancanti, catene lunghe di lemmi ausiliari e ragionamento specifico per l'ottimizzazione.

Significato e Affermazioni

Il documento afferma che CAM-Bench funge da complemento critico ai benchmark formali esistenti mirando a problemi di matematica applicata che si basano su concetti dei manuali e teoremi elementari. Il suo significato risiede in:

1. Valutazione del Ragionamento Dipendente dal Contesto: Testa la capacità di un modello di tracciare assunzioni locali e ricostruire il contesto, una capacità essenziale per la formalizzazione nel mondo reale ma spesso bypassata dai benchmark di teoremi isolati.
2. Diagnosi dei Colli di Bottiglia Sistemici: I risultati evidenziano che i provatori basati su LLM attuali faticano non solo con la sintassi, ma con il grounding in Mathlib, la disciplina dei tipi e la decomposizione di dimostrazioni a lungo orizzonte.
3. Guida allo Sviluppo dell'Infrastruttura: Il benchmark suggerisce che i progressi nella matematica applicata formale richiedono un'infrastruttura Mathlib più robusta (ad esempio, per matrici, spettri, convessità) e agenti più capaci in grado di gestire traiettorie di dimostrazione a lungo orizzonte.

Gli autori mantengono una posizione modesta, notando che, sebbene i sistemi agentici migliorino le prestazioni, il benchmark rimane impegnativo e i risultati dovrebbero essere considerati stime delle capacità attuali piuttosto che un problema risolto. Il benchmark è destinato a essere un componente di una suite di valutazione più ampia per i sistemi di ragionamento matematico.