MASA: Sistemi Multi-Agente Guidati da LLM per l'Autoformalizzazione

Informazioni Fondamentali

• ID Articolo: 2510.08988
• Titolo: MASA: LLM-Driven Multi-Agent Systems for Autoformalization
• Autori: Lan Zhang (University of Manchester), Marco Valentino (University of Sheffield), André Freitas (University of Manchester, Idiap Research Institute, National Biomarker Centre)
• Classificazione: cs.CL (Linguistica Computazionale), cs.FL (Linguaggi Formali)
• Data di Pubblicazione: 10 ottobre 2025 (preprint arXiv)
• Link Articolo: https://arxiv.org/abs/2510.08988

Riassunto

L'autoformalizzazione svolge un ruolo cruciale nel collegare il linguaggio naturale e il ragionamento formale. Questo articolo presenta MASA, un framework per sistemi multi-agente guidati da modelli di linguaggio di grandi dimensioni (LLM) per compiti di autoformalizzazione. MASA sfrutta agenti collaborativi per convertire enunciati in linguaggio naturale nelle loro rappresentazioni formali. L'architettura di MASA enfatizza modularità, flessibilità e scalabilità, consentendo l'integrazione senza soluzione di continuità di nuovi agenti e strumenti per adattarsi al rapido sviluppo del campo. Gli autori dimostrano l'efficacia di MASA attraverso casi d'uso di definizioni matematiche nel mondo reale e esperimenti su dataset di matematica formale. Questo lavoro evidenzia il potenziale dei sistemi multi-agente guidati dall'interazione tra LLM e provatori di teoremi nel migliorare l'efficienza e l'affidabilità dell'autoformalizzazione.

Contesto di Ricerca e Motivazione

Definizione del Problema

L'autoformalizzazione è il compito di convertire automaticamente enunciati matematici in linguaggio naturale in formule logiche formali verificabili da macchina. Le sfide fondamentali di questo problema sono:

1. Divario Semantico: Esiste una differenza sostanziale tra l'ambiguità del linguaggio naturale e la rigidità del linguaggio formale
2. Complessità: Gli enunciati matematici nel mondo reale spesso coinvolgono concetti complessi e catene di ragionamento articolate
3. Requisiti di Accuratezza: I risultati della formalizzazione devono essere corretti sia sintatticamente che semanticamente

Importanza del Problema

L'autoformalizzazione ha un'importanza significativa:

• Verifica Matematica: Fornisce le basi per la dimostrazione di teoremi e la verifica matematica
• Trasparenza del Ragionamento: Il ragionamento formale è più sistematico, trasparente e rigoroso rispetto al ragionamento in linguaggio naturale
• Necessità di Automazione: La formalizzazione manuale richiede notevoli competenze specializzate e investimenti di tempo

Limitazioni degli Approcci Esistenti

I sistemi di autoformalizzazione basati su LLM esistenti presentano i seguenti problemi:

1. Limitazioni dell'Architettura Monolitica: Un singolo LLM ha difficoltà nel gestire problemi complessi di autoformalizzazione nel mondo reale
2. Mancanza di Modularità: Le implementazioni esistenti mancano di modularità, flessibilità e scalabilità
3. Interazione Insufficiente tra Componenti: Incapacità di integrare efficacemente più componenti interattivi

Motivazione della Ricerca

La motivazione degli autori nel proporre il framework MASA è:

• Costruire sistemi multi-agente modulari per affrontare la complessità dell'autoformalizzazione
• Fornire un framework flessibile e scalabile che supporti i ricercatori nello sviluppo e nell'estensione rapida del sistema
• Migliorare l'efficienza e l'affidabilità dell'autoformalizzazione attraverso la collaborazione tra agenti

Contributi Fondamentali

1. Propone un Framework Multi-Agente Modulare: MASA fornisce un framework modulare per la costruzione di sistemi multi-agente per l'autoformalizzazione, con eccellente flessibilità e scalabilità
2. Dimostra Applicazioni nel Mondo Reale: Attraverso la formalizzazione di definizioni matematiche nel mondo reale da parte degli agenti, evidenzia il potenziale pratico del framework
3. Valutazione Sistematica: Valuta il framework in tre diverse configurazioni multi-agente, provando la sua efficacia e fornendo intuizioni preziose. Il sistema finale di auto-miglioramento iterativo raggiunge tassi di formalizzazione sintatticamente corretti e semanticamente allineati del 35,25% su Qwen2.5-7B e del 61,89% su GPT-4.1-mini
4. Implementazione Open-Source: Fornisce codice e dati completi, riducendo le barriere di ricerca

Dettagli del Metodo

Definizione del Compito

L'autoformalizzazione può essere definita come una funzione di trasformazione A che mappa un enunciato in linguaggio naturale s alla sua rappresentazione formale φ = A(s). Gli approcci tradizionali implementano questo attraverso prompt LLM: A = LLM(prompt). MASA estende questa definizione implementando un processo di trasformazione più complesso attraverso un sistema multi-agente.

Architettura del Modello

Il framework MASA contiene cinque componenti fondamentali:

1. Agent (Agenti)

Gli agenti sono elementi fondamentali che eseguono funzioni specifiche, includendo:

• AutoformalizationAgent: Esegue l'autoformalizzazione con pochi esempi
• HardCritiqueAgent: Fornisce critiche a livello sintattico basate su provatori di teoremi
• SoftCritiqueAgent: Fornisce critiche a livello semantico basate su LLM
• FormalRefinementAgent: Migliora il codice formalizzato basato su critiche hard
• InformalRefinementAgent: Migliora il codice formalizzato basato su critiche soft
• DenoisingAgent: Agente strumento per la riduzione del rumore
• ImportRetrievalAgent: Agente strumento per il recupero di importazioni

2. Large Language Model (Modello di Linguaggio di Grandi Dimensioni)

L'LLM fornisce capacità di ragionamento e linguaggio agli agenti, supportando:

• Modelli OpenAI (come GPT-4.1-mini)
• Modelli locali HuggingFace (come Qwen2.5-7B, DeepSeek-Math)

3. Knowledge Base (Base di Conoscenza)

Memorizza informazioni sulla libreria di linguaggi formali, supportando il recupero di conoscenze rilevanti. L'implementazione attuale include una base di conoscenza di enunciati e prove formali Isabelle/HOL.

4. Retriever (Recuperatore)

Classifica i punti dati nella libreria matematica per rilevanza, con implementazione attuale basata sul metodo BM25.

5. Theorem Prover (Provatore di Teoremi)

Verifica la correttezza sintattica e logica della formalizzazione, fornendo messaggi di errore. Supporta:

• Isabelle (tramite server dedicato)
• Lean4 (tramite REPL)

Punti di Innovazione Tecnica

1. Progettazione Modulare: Utilizza il design della classe base astratta, facilitando l'estensione di nuovi agenti e strumenti
2. Meccanismo di Critica Multi-Livello: Combina critiche hard (sintassi) e soft (semantica)
3. Processo di Miglioramento Iterativo: Supporta la collaborazione multi-agente con auto-miglioramento iterativo
4. Integrazione di Agenti Strumento: Integra strumenti pratici come riduzione del rumore e recupero di importazioni

Configurazione Sperimentale

Dataset

1. miniF2F: Fornisce formalizzazioni reali in Isabelle/HOL e Lean4, utilizzate per il benchmarking
2. ProofNet: Fornisce formalizzazioni reali di codice Lean4

Metriche di Valutazione

Correttezza Sintattica

• Pass Rate: Percentuale di formalizzazioni sintatticamente corrette

Valutazione Semantica

• BLEU-4: Sovrapposizione n-gram con formalizzazioni reali
• ChrF: F-score a livello di carattere
• RUBY: Metrica di valutazione della migrazione del codice

Valutazione degli Agenti

• Alignment Faithfulness (AF): Se il codice formalizzato si allinea accuratamente alla semantica del linguaggio naturale
• Formalization Correctness (FC): Se il codice formalizzato stesso è valido, naturale e ben formattato

Metodi di Confronto

• Prompt Zero-Shot (ZS): Utilizzo diretto di LLM per la formalizzazione
• Prompt Few-Shot (FS): Formalizzazione utilizzando 3 esempi
• Diverse Combinazioni di LLM: GPT-4.1-mini, DeepSeek-Math-7B, Qwen2.5-7B

Dettagli di Implementazione

• Utilizzo di GPT-4.1-mini come LLM backend per l'agente di critica soft
• Supporto per due linguaggi formali: Isabelle/HOL e Lean4
• Implementazione Python completa e esempi di Jupyter Notebook

Risultati Sperimentali

Risultati Principali

Sistema di Miglioramento Formale con Critica Hard (Tabella 1)

miniF2F-Test (Isabelle/HOL):

• GPT-4.1-mini zero-shot: Pass Rate 65,57% → 77,05% (+11,48%)
• GPT-4.1-mini few-shot: Pass Rate 76,23% → 86,48% (+10,25%)
• DeepSeek-Math few-shot: Pass Rate 29,10% → 36,48% (+7,38%)

ProofNet-Test (Lean4):

• GPT-4.1-mini zero-shot: Pass Rate 3,30% → 3,85% (+0,55%)
• GPT-4.1-mini few-shot: Pass Rate 12,09% → 14,84% (+2,75%)

Sistema di Miglioramento Informale con Critica Soft (Tabella 2)

miniF2F (Lean4):

• DeepSeek-Math + GPT-4.1-mini migliorato: AF 38,52% → 90,57%, FC 47,54% → 79,92%
• Qwen2.5-7B + GPT-4.1-mini migliorato: AF 54,51% → 93,44%, FC 62,70% → 85,25%

Esperimenti di Auto-Miglioramento Iterativo

I risultati della Figura 2 mostrano:

• Qwen2.5-7B: Dopo 4 iterazioni, la proporzione di formalizzazioni sintatticamente corrette e semanticamente allineate raggiunge il 35,25%
• GPT-4.1-mini: Dopo 4 iterazioni, la proporzione di formalizzazioni sintatticamente corrette e semanticamente allineate raggiunge il 61,89%

Scoperte Sperimentali

1. Few-Shot Superiore a Zero-Shot: In tutte le configurazioni, l'apprendimento few-shot migliora significativamente le prestazioni
2. Impatto della Capacità del Modello: I modelli più forti (GPT-4.1-mini) mostrano prestazioni migliori nel miglioramento formale
3. Efficacia del Miglioramento Iterativo: Le iterazioni multiple migliorano continuamente la qualità della formalizzazione
4. Miglioramento Cross-Modello: I modelli più forti possono migliorare gli output dei modelli più deboli

Lavori Correlati

Ricerca sull'Autoformalizzazione

• Metodi di Prompt: Wu et al. (2022) e altri utilizzano prompt LLM per l'autoformalizzazione
• Generazione di Dati: Jiang et al. (2024) e Liu et al. (2025b) sviluppano corpora paralleli su larga scala
• Implementazioni di Sistemi: I sistemi esistenti mancano di modularità e scalabilità

Sistemi Multi-Agente

• Campi di Applicazione: Sistemi operativi, educazione medica, verifica di risposte
• Compiti di Ragionamento: Ragionamento aritmetico e ragionamento generale
• Applicazioni all'Autoformalizzazione: La ricerca su sistemi multi-agente nel campo dell'autoformalizzazione è limitata

Conclusioni e Discussione

Conclusioni Principali

1. Efficacia del Framework: MASA costruisce con successo un sistema multi-agente modulare per l'autoformalizzazione
2. Miglioramento delle Prestazioni: La collaborazione multi-agente migliora significativamente l'accuratezza dell'autoformalizzazione
3. Valore Pratico: Il framework fornisce ai ricercatori una piattaforma di sviluppo flessibile

Limitazioni

1. Mancanza di Controllo Centrale: Il sistema manca di un agente centrale per assegnare e controllare diversi agenti
2. Limitazioni della Valutazione Semantica: La valutazione semantica è limitata a giudizi di alto livello, richiedendo standard di valutazione più granulari
3. Dipendenza dal Modello: Le prestazioni del sistema dipendono in larga misura dalle capacità dell'LLM sottostante

Direzioni Future

1. Controllo Centrale Migliorato: Sviluppare meccanismi di controllo di sistemi multi-agente più avanzati
2. Valutazione Affinata: Stabilire standard di valutazione semantica più precisi
3. Estensione delle Applicazioni: Applicare il framework a compiti di formalizzazione più ampi

Valutazione Approfondita

Punti di Forza

1. Forte Innovatività: Primo framework sistematico multi-agente per l'autoformalizzazione
2. Progettazione Razionale: L'architettura modulare è elegante e facile da estendere
3. Esperimenti Completi: Copre diverse configurazioni e metriche di valutazione
4. Alto Valore Pratico: L'implementazione open-source riduce le barriere di ricerca
5. Risultati Convincenti: Valida l'efficacia del metodo su più dataset

Insufficienze

1. Analisi Teorica Limitata: Manca l'analisi teorica dei meccanismi di collaborazione multi-agente
2. Costi Computazionali: L'analisi dei costi computazionali del sistema multi-agente è insufficiente
3. Propagazione degli Errori: Manca un'analisi approfondita della propagazione degli errori tra agenti
4. Limitazioni della Valutazione: La valutazione semantica dipende ancora dal giudizio dell'LLM, con possibili distorsioni

Impatto

1. Contributo Accademico: Fornisce un nuovo paradigma per la ricerca sull'autoformalizzazione
2. Valore Pratico: Il framework può essere utilizzato direttamente nello sviluppo di applicazioni pratiche
3. Riproducibilità: L'implementazione open-source completa garantisce la riproducibilità
4. Promozione dello Sviluppo: Potrebbe promuovere l'applicazione di sistemi multi-agente nel campo della formalizzazione

Scenari Applicabili

1. Formalizzazione Matematica: Adatto alla formalizzazione automatica di teoremi e definizioni matematiche complesse
2. Applicazioni Educative: Può essere utilizzato per l'addestramento alla formalizzazione nell'insegnamento della matematica
3. Strumento di Ricerca: Fornisce una piattaforma di base per la ricerca sull'autoformalizzazione
4. Applicazioni Industriali: Può essere integrato in sistemi software che richiedono verifica formale

Bibliografia

La bibliografia chiave include:

• Wu et al. (2022): Autoformalization with large language models
• Zheng et al. (2022): miniF2F: a cross-system benchmark for formal olympiad-level mathematics
• Azerbayev et al. (2023): ProofNet: Autoformalizing and formally proving undergraduate-level mathematics
• Jiang et al. (2023): Draft, sketch, and prove: Guiding formal theorem provers with informal proofs

Sintesi: MASA è un framework innovativo multi-agente per l'autoformalizzazione che migliora significativamente gli effetti dell'autoformalizzazione attraverso la progettazione modulare e la collaborazione tra agenti. Questo lavoro dimostra eccellenza in innovazione tecnica, verifica sperimentale e valore pratico, aprendo nuove direzioni per la ricerca sull'autoformalizzazione. Nonostante alcune limitazioni, la sua implementazione open-source e la buona scalabilità lo rendono un contributo importante nel campo.