Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers

Il paper presenta Strat2Rocq, un approccio che estrae le strategie di prova interne dei modelli linguistici (LLM) per trasformarle in lemmi formali, migliorando così l'efficacia dei prover simbolici come CoqHammer e, incidentalmente, anche degli agenti di prova basati su LLM.

L'essenziale

Ecco una spiegazione semplice e creativa del paper, pensata per chiunque, anche senza conoscenze di informatica.

🧠 L'idea di fondo: Insegnare al "Cervello Logico" a pensare come il "Genio Creativo"

Immagina due personaggi molto diversi che lavorano in un'officina di software:

1. Il "Logico Rigido" (i Proverbi Simbolici, come CoqHammer): È un artigiano meticoloso, preciso e sicuro. Segue le regole alla lettera, passo dopo passo. Non sbaglia mai, ma è lento e a volte si blocca se non vede la strada immediatamente. È come un contabile che deve sommare tutto a mano: infallibile, ma faticoso.
2. Il "Genio Creativo" (le Intelligenze Artificiali, come LLM): È un artista visionario. Vede i problemi in modo olistico, salta i passaggi noiosi e trova soluzioni brillanti in un lampo. Tuttavia, a volte è disordinato, può allucinare (inventare cose che non esistono) e, soprattutto, è costoso e lento da far lavorare ogni volta che serve una soluzione.

Il problema: Le aziende vogliono la precisione del Logico, ma vorrebbero anche la velocità e l'intuizione del Genio. Usare solo il Genio è rischioso (potrebbe dire bugie) e costoso. Usare solo il Logico è troppo lento per i problemi complessi.

🛠️ La soluzione: "Strat2Rocq" (Il Traduttore di Strategie)

Gli autori di questo studio hanno pensato: "E se potessimo prendere le intuizioni del Genio Creativo, trasformarle in regole precise e darle al Logico Rigido, così che lui possa usarle senza bisogno del Genio ogni volta?"

Hanno creato un sistema chiamato Strat2Rocq. Ecco come funziona, passo dopo passo, con una metafora:

1. La Fase di "Scuola Notturna" (Offline)

Immagina che il Logico Rigido stia studiando da solo. Gli autori prendono il Genio Creativo e gli chiedono: "Ehi, come risolveresti questo enigma matematico?".
Il Genio risponde con una spiegazione discorsiva, piena di intuizioni: "Beh, è ovvio che se fai A più B, è la stessa cosa che B più A, quindi non serve fare tutti quei calcoli!".

Invece di lasciare che il Genio risolva il problema ogni volta, il sistema Strat2Rocq fa una cosa geniale:

• Prende l'intuizione del Genio ("A più B è come B più A").
• La traduce in una regola formale, una "legge" scritta in un linguaggio che il Logico Rigido capisce perfettamente (chiamata Lemma).
• Immagina di prendere un'idea astratta e trasformarla in un attrezzo fisico (come un martello o una chiave inglese) che il Logico può mettere nella sua cassetta degli attrezzi.

Questa fase avviene una sola volta, offline. Si crea una biblioteca di "attrezzi intelligenti" derivati dalle intuizioni dell'IA.

2. La Fase di "Lavoro sul Campo" (Online)

Ora, quando arriva un nuovo problema da risolvere:

• Il Logico Rigido apre la sua cassetta degli attrezzi.
• Trova gli "attrezzi" creati dalla fase precedente (le regole derivate dal Genio).
• Usa questi attrezzi per risolvere il problema molto più velocemente e con successo, senza aver bisogno di chiamare il Genio Creativo.

È come se avessimo insegnato al contabile a usare una calcolatrice avanzata che ha memorizzato le scorciatoie del genio, così ora può fare i calcoli da solo, velocemente e senza errori.

📊 I Risultati: Quanto è efficace?

Gli autori hanno testato questo sistema su progetti reali di verifica software (come compilatori certificati e librerie matematiche). I risultati sono stati sorprendenti:

• Il Logico Rigido è diventato più forte: La percentuale di problemi risolti con successo è aumentata del 13,41%. È come se un contabile, dopo aver ricevuto nuovi attrezzi, riuscisse a risolvere 13 problemi su 100 che prima lo bloccavano.
• Anche il Genio ne beneficia: Se si danno questi "attrezzi" anche al Genio Creativo, lui risolve meglio i problemi (migliora del 4%), perché ha meno lavoro da fare e può concentrarsi sulle parti difficili.
• Sicurezza e Risparmio: Il grande vantaggio è che, una volta creato il sistema, non serve più pagare l'IA costosa per ogni singolo calcolo. Tutto può essere fatto sul computer di un utente, in modo sicuro e gratuito.

💡 In sintesi

Il paper Strat2Rocq ci insegna che non dobbiamo scegliere tra l'IA potente e i sistemi sicuri. Possiamo estrarre la saggezza dell'IA e trasformarla in regole solide. È come se prendessimo i sogni di un architetto geniale, li trasformassimo in un manuale di istruzioni preciso, e lo dessimo a un muratore esperto: il risultato è una casa costruita velocemente, senza errori e senza dover chiamare l'architetto ogni giorno.

È un passo avanti verso un futuro in cui l'intelligenza artificiale ci aiuta a costruire software più sicuro, senza però doverci fidare ciecamente di essa ogni volta.

Sommario tecnico

Ecco una sintesi tecnica dettagliata del paper "Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers" (Estrazione di Strategie di Dimostrazione dagli LLM per Potenziare i Prover Symbolici), presentata in italiano.

1. Il Problema

L'area della verifica software, in particolare attraverso la dimostrazione di teoremi interattiva (ITP), richiede spesso un notevole sforzo umano per scrivere prove formali. Sebbene i Large Language Models (LLM) abbiano dimostrato capacità eccezionali nell'automazione delle prove, integrandoli direttamente nei flussi di lavoro presenta sfide significative:

• Costo e Risorse: L'uso di LLM in tempo reale (online) richiede risorse computazionali elevate, rendendoli inadatti per ambienti con hardware limitato o budget ridotti.
• Sicurezza: Molte aziende, specialmente quelle che sviluppano software critico, non possono inviare il proprio codice sorgente (spesso confidenziale) a servizi LLM esterni.
• Limiti degli Approcci Ibridi: Gli agenti di prova ibridi (che combinano LLM e prover simbolici) non possono sostituire completamente gli approcci puramente simbolici, che rimangono essenziali per la loro efficienza, sicurezza e costo contenuto.

La domanda di ricerca centrale è: È possibile estrarre le strategie di prova interne degli LLM per potenziare i prover simbolici tradizionali, rendendoli più efficaci senza dover ricorrere agli LLM durante la fase di prova online?

2. Metodologia: Strat2Rocq

Gli autori propongono Strat2Rocq, un framework che opera in due fasi distinte: una fase offline di estrazione e una fase online di utilizzo. L'obiettivo è estrarre le "strategie" implicite degli LLM e formalizzarle come lemmi verificati nel linguaggio Rocq (Coq), che possono poi essere utilizzati dal prover simbolico CoqHammer.

Fase 1: Estrazione Offline (Mining dei Lemmi)

Questa fase avviene una sola volta su un set di addestramento di teoremi esistenti.

1. Generazione di Prove in Linguaggio Naturale (NL): Per ogni teorema del set di addestramento, un LLM (es. Claude 3.7 Sonnet o o3-mini) viene invitato a generare una prova passo-passo in linguaggio naturale. Si preferisce il linguaggio naturale perché gli LLM lo gestiscono meglio e riflette più fedelmente il loro ragionamento interno rispetto alla generazione diretta di codice formale.
2. Generalizzazione e Formalizzazione: I passaggi della prova in NL vengono analizzati. L'LLM viene istruito a:
   • Generalizzare i passaggi specifici in lemmi generali (strategie astratte).
   • Formalizzare questi lemmi nel linguaggio Rocq.
   • Fornire la prova formale per ciascun lemma.
3. Correzione Iterativa (Proof Agent): Poiché gli LLM possono commettere errori nella formalizzazione, viene utilizzato un "agente di prova" che tenta iterativamente di correggere gli errori di compilazione o di logica nei lemmi generati, fino a un limite di tentativi.

Fase 2: Dimostrazione Online

Una volta estratti e formalizzati i lemmi:

• I nuovi lemmi vengono inseriti nel contesto di un nuovo teorema da dimostrare.
• Il prover simbolico CoqHammer viene eseguito sul teorema target, avendo accesso a questo arricchito contesto di lemmi (che codificano le strategie apprese dall'LLM).
• Nota cruciale: Durante questa fase, non viene utilizzato alcun LLM. Il prover simbolico lavora in autonomia, ma "potenziato" dalla conoscenza estratta in precedenza.

3. Contributi Chiave

• Nuovo Problema di Ricerca: Propone l'estrazione offline delle strategie di prova dagli LLM per migliorare i prover simbolici, superando i limiti di costo e sicurezza degli approcci ibridi online.
• Metodologia di Estrazione: Introduce un flusso di lavoro che trasforma le prove in linguaggio naturale (facili da generare per gli LLM) in lemmi formali verificati, aggirando la difficoltà dell'autoformalizzazione diretta.
• Implementazione e Validazione: Ha implementato il sistema come Strat2Rocq e lo ha validato empiricamente su progetti open-source reali.
• Scoperta Collaterale: Ha dimostrato che i lemmi estratti migliorano non solo i prover simbolici, ma anche gli agenti basati su LLM (tramite tecniche RAG - Retrieval-Augmented Generation).

4. Risultati Sperimentali

Gli esperimenti sono stati condotti su un benchmark di 2.394 teoremi provenienti da progetti Rocq reali (CompCert, Ext-Lib, Coq-Art, Vfa).

• Miglioramento dei Prover Simbolici (CoqHammer):

  • L'uso dei lemmi estratti da Strat2Rocq ha aumentato il tasso di successo delle prove di CoqHammer del 13,41% in media.
  • Il miglioramento è stato particolarmente evidente su CompCert (+17,75%), un compilatore C certificato, dimostrando l'efficacia in scenari reali.
  • Le strategie estratte hanno permesso a CoqHammer di evitare l'uso dell'induzione (che non supporta nativamente) riducendo i teoremi a proprietà algebriche note, e di selezionare meglio i lemmi rilevanti.

• Robustezza e Generalità:

  • Il metodo funziona con diversi LLM backend (testato sia con Claude 3.7 Sonnet che con o3-mini).
  • L'uso combinato di lemmi estratti da diversi LLM ha portato a un miglioramento ancora maggiore, suggerendo che le strategie interne dei modelli non si sovrappongono completamente.

• Impatto sugli Agenti LLM:

  • L'integrazione dei lemmi estratti ha migliorato le prestazioni di un agente LLM del 4,00% e ha ridotto il consumo di token del 5,87%, poiché il prover simbolico potenziato risolve più teoremi autonomamente, riducendo la necessità di chiamate all'LLM.

• Ablation Study:

  • È stato dimostrato che il passaggio di generazione della prova in linguaggio naturale è essenziale: saltare questo passaggio e chiedere direttamente i lemmi formali ha portato a una diminuzione del 63,56% nel numero di lemmi estratti e a un calo delle prestazioni.

5. Significato e Implicazioni

Il lavoro di Fang et al. è significativo per diversi motivi:

1. Sostenibilità e Sicurezza: Offre una via per sfruttare l'intelligenza degli LLM nella verifica software senza i costi ricorrenti e i rischi di sicurezza legati all'invio di dati sensibili a servizi esterni durante la fase operativa.
2. Interpretabilità: Il framework offre un modo per "comprendere" come gli LLM risolvono i problemi. Estraendo le loro strategie sotto forma di lemmi simbolici verificabili, gli autori creano un modello simbolico approssimativo del comportamento dell'LLM.
3. Sinergia tra Paradigmi: Dimostra che l'era degli LLM non sostituisce i prover simbolici, ma può essere utilizzata per potenziarli, creando un ecosistema dove l'LLM funge da "insegnante" offline e il prover simbolico da "studente" efficiente e sicuro online.

In sintesi, Strat2Rocq rappresenta un passo avanti fondamentale verso l'automazione della verifica software che è allo stesso tempo potente (grazie all'LLM), economica e sicura (grazie all'approccio puramente simbolico online).