Formally Solving Answer-Construction Problems in Lean

Sintesi Tecnica: Risolvere Formalmente Problemi di Costruzione di Risposte in Lean

Definizione del Problema
I problemi delle competizioni matematiche generalmente rientrano in due categorie: la dimostrazione di teoremi (verificare un'affermazione data) e la costruzione di risposte (costruire un oggetto specifico che soddisfi una proprietà). Mentre i recenti progressi nei Modelli di Linguaggio di Grandi Dimensioni (LLM) hanno migliorato significativamente la dimostrazione formale di teoremi, la costruzione formale di risposte rimane scarsamente esplorata. Esiste un divario critico tra i sistemi di ragionamento informale, che sono forti nelle congetture ma deboli nella verifica formale, e i modelli LLM per la dimostrazione formale, che sono ottimizzati per le dimostrazioni ma faticano a scoprire i testimoni necessari per eliminare i quantificatori esistenziali.

Una sfida specifica nella formalizzazione della costruzione di risposte è l'ammissibilità. I normali controllori di prove Lean verificano che un termine di prova abbia il tipo corretto, ma non impongono intrinsecamente che il testimone costruito sia una risposta canonica e in forma chiusa. Per esempio, una prova potrebbe soddisfare un'affermazione esistenziale $\exists x, P(x)$ restituendo un termine non canonico come sInf PropertySet (l'infimo dell'insieme definito) invece di un numero naturale esplicito (ad esempio, 245). Tali testimoni "circolari" o non in forma chiusa sono matematicamente validi all'interno della logica, ma inadmissibili come risposte per un concorso.

Metodologia: Enumerate-Conjecture-Prove (ECP)
Per affrontare queste sfide, gli autori introducono Enumerate-Conjecture-Prove (ECP), un framework neuro-simbolico progettato per la costruzione di risposte end-to-end con prove formali in Lean 4. ECP separa il processo in fasi distinte mantenendo al contempo un ciclo di verifica formale:

1. Formalizzazione del Problema e Controllo di Ammissibilità:

   • I problemi sono formalizzati come compiti di sintesi funzionale: trovare una funzione $\Psi$ tale che $\forall X, P(X) \to Q(X, \Psi(X))$.
   • Viene implementato un controllore di ammissibilità per garantire che il testimone sintetizzato utilizzi solo un "vocabolario ammissibile" predefinito (ad esempio, costanti specifiche, operatori aritmetici e costruttori standard). Esso estrae strutturalmente le costanti semantiche dal termine Lean e filtra le costanti amministrative (come le istanze di typeclass o gli artefatti generati dal compilatore) e le definizioni non canoniche (come sInf).

2. Fase di Enumerazione (Esplorazione Assistita da Strumenti):

   • Un LLM general-purpose (ad esempio, GPT-5.4) è dotato di capacità di esecuzione di strumenti Python.
   • L'LLM scrive ed esegue codice Python per eseguire un'enumerazione limitata su piccoli domini al fine di trovare tuple che soddisfino i vincoli del problema.
   • Questi trace di esecuzione servono come evidenza empirica per identificare pattern, invarianti e forme funzionali.

3. Fase di Congettura (Sintesi della Risposta):

   • Utilizzando l'evidenza della fase di Enumerazione, lo stesso LLM general-purpose sintetizza una funzione risposta candidata $\Psi'$.
   • Il candidato è sottoposto a due filtri prima di procedere:
     • Verifica Sintattica: Il termine deve compilare in Lean con il tipo corretto.
     • Verifica di Ammissibilità: Il termine deve utilizzare solo costanti dal vocabolario consentito.
   • Se un candidato fallisce, il sistema itera includendo il messaggio di errore nel prompt.

4. Fase di Dimostrazione (Verifica Formale):

   • Una volta costruito un candidato valido $\Psi'$, il sistema tenta di dimostrare il teorema istanziato $Stmt(T)|_{\Psi=\Psi'}$.
   • Ciclo di Confutazione: Prima di tentare una dimostrazione, il sistema tenta di confutare il candidato dimostrando la sua negazione. Se la confutazione ha successo, il candidato viene scartato e il sistema torna alla fase di Congettura.
   • Generazione della Dimostrazione: Se la confutazione fallisce, il sistema tenta di dimostrare l'affermazione positiva utilizzando una combinazione dell'automazione integrata in Lean (tattiche come simp, aesop, ring, norm_num) e un prover LLM specializzato (ad esempio, Goedel-Prover-V2). Se l'automazione fallisce, il prover LLM viene invocato con un ciclo di riparazione per generare o correggere la dimostrazione.

Contributi Chiave

• Framework per la Costruzione di Risposte: ECP è il primo framework che separa esplicitamente la costruzione della risposta dalla generazione della dimostrazione, imponendo vincoli di ammissibilità all'interno di un ciclo di verifica formale.
• Imposizione dell'Ammissibilità: Il documento introduce un metodo strutturale per filtrare testimoni non canonici (es. definizioni circolari) che i normali controllori Lean accetterebbero, garantendo che l'output corrisponda ai requisiti del concorso.
• Integrazione Neuro-Simbolica: Il framework combina efficacemente il ragionamento esplorativo degli LLM general-purpose con gli strumenti Python e le rigorose capacità di dimostrazione degli LLM specializzati per la prova.
• Benchmark e Autoformalizzazione: Gli autori hanno autoformalizzato 75 problemi dalle finali MathArena 2026 (AIME, HMMT, APEX) e 346 problemi di costruzione di risposte da PutnamBench, creando un nuovo standard di valutazione per questo tipo di problema.

Risultati Sperimentali
Il sistema è stato valutato su MathArena 2026 (75 problemi) e PutnamBench (346 problemi) rispetto a baseline che includono LLM di generazione diretta di prove (GPT-5.4, Goedel-Prover-V2).

• Prestazioni End-to-End: ECP ha superato le baseline di generazione diretta di prove (GPT-5.4, Goedel-Prover-V2).
  • MathArena: ECP ha risolto 18/75 problemi (Pass@32), rispetto a 13/75 della migliore baseline basata solo su LLM (GPT-5.4).
  • PutnamBench: ECP ha risolto 17/346 problemi (Pass@32), rispetto a 8/346 per GPT-5.4 e 7/346 per Goedel-Prover-V2-32B.
• Accuratezza della Sola Risposta: La costruzione della risposta assistita da strumenti ha migliorato significativamente l'accuratezza degli LLM general-purpose nella generazione di candidati corretti. Per GPT-5.4, l'uso di strumenti ha aumentato la costruzione di risposte corrette su PutnamBench da 290/346 a 303/346.
• Impatto dell'Amissibilità: L'analisi ha rivelato che molte prove generate dalle baseline erano compilabili in Lean ma contenevano risposte inadmissibili (es. testimoni circolari). Il controllo di ammissibilità esplicito di ECP è stato cruciale per filtrarle.
• Studi di Ablazione:
  • Rimuovere il passaggio di correzione del prover LLM ha ridotto le prestazioni su MathArena (18 $\to$ 16) e PutnamBench (17 $\to$ 16).
  • Rimuovere l'automazione di Lean ha avuto un impatto severo su MathArena (18 $\to$ 11) ma meno su PutnamBench in questa specifica esecuzione, suggerendo che i problemi di MathArena dipendano maggiormente dalle tattiche di automazione, mentre PutnamBench dipenda maggiormente dalla capacità del prover.
  • L'uso di un prover più piccolo (8B) ha mantenuto le prestazioni su MathArena ma ha ridotto significativamente i risultati di PutnamBench (17 $\to$ 7), indicando che i problemi di Putnam sono più limitati dalla ricerca della dimostrazione.

Significato e Rivendicazioni
Il documento sostiene che ECP riesce a colmare il divario tra la generazione di risposte informali e la dimostrazione formale di teoremi. Gestendo esplicitamente la fase di "costruzione della risposta" e imponendo l'ammissibilità, ECP risolve istanze che sono attualmente intrattabili per gli approcci di generazione diretta di prove. Gli autori sottolineano che il loro approccio è particolarmente efficace per problemi che richiedono la costruzione di un testimone specifico (quantificazione esistenziale) piuttosto che la semplice verifica di una conclusione fissata.

Il lavoro evidenzia come gli attuali benchmark formali spesso omettano la difficoltà della costruzione della risposta, concentrandosi invece sulle versioni dei problemi "con risposta". ECP dimostra che combinare LLM general-purpose con l'esecuzione di strumenti per l'enumerazione, seguiti da prover LLM specializzati per la verifica, è una via percorribile per risolvere problemi matematici complessi e aperti nei sistemi formali. Gli autori notano limitazioni riguardanti la natura euristica dell'etichettatura del vocabolario ammissibile e il potenziale di esplosione combinatoria nella fase di enumerazione per problemi combinatori altamente complessi.