2025-11-13T01:07:10.778375

MASA: LLM-Driven Multi-Agent Systems for Autoformalization

Zhang, Valentino, Freitas
Autoformalization serves a crucial role in connecting natural language and formal reasoning. This paper presents MASA, a novel framework for building multi-agent systems for autoformalization driven by Large Language Models (LLMs). MASA leverages collaborative agents to convert natural language statements into their formal representations. The architecture of MASA is designed with a strong emphasis on modularity, flexibility, and extensibility, allowing seamless integration of new agents and tools to adapt to a fast-evolving field. We showcase the effectiveness of MASA through use cases on real-world mathematical definitions and experiments on formal mathematics datasets. This work highlights the potential of multi-agent systems powered by the interaction of LLMs and theorem provers in enhancing the efficiency and reliability of autoformalization, providing valuable insights and support for researchers and practitioners in the field.
academic

MASA: LLM-gesteuerte Multi-Agent-Systeme zur Autoformaliserung

Grundinformationen

  • Papier-ID: 2510.08988
  • Titel: MASA: LLM-Driven Multi-Agent Systems for Autoformalization
  • Autoren: Lan Zhang (University of Manchester), Marco Valentino (University of Sheffield), André Freitas (University of Manchester, Idiap Research Institute, National Biomarker Centre)
  • Klassifizierung: cs.CL (Computerlinguistik), cs.FL (Formale Sprachen)
  • Veröffentlichungsdatum: 10. Oktober 2025 (arXiv-Preprint)
  • Papierlink: https://arxiv.org/abs/2510.08988

Zusammenfassung

Die Autoformaliserung spielt eine Schlüsselrolle bei der Verbindung von natürlicher Sprache und formaler Inferenz. Dieses Papier präsentiert MASA, ein Framework für Multi-Agent-Systeme, das von großen Sprachmodellen (LLMs) angetrieben wird und für Autoformaliserungsaufgaben konzipiert ist. MASA nutzt kollaborative Agenten, um natürlichsprachliche Aussagen in ihre formalen Darstellungen zu konvertieren. Die Architektur von MASA betont Modularität, Flexibilität und Skalierbarkeit und ermöglicht die nahtlose Integration neuer Agenten und Werkzeuge, um sich an die sich schnell entwickelnde Domäne anzupassen. Die Autoren demonstrieren die Wirksamkeit von MASA durch Anwendungsfälle mit realen mathematischen Definitionen und Experimente auf formalen mathematischen Datensätzen. Diese Arbeit hebt das Potenzial von Multi-Agent-Systemen, die durch die Interaktion von LLMs und Theorembeweisern angetrieben werden, zur Verbesserung der Effizienz und Zuverlässigkeit der Autoformaliserung hervor.

Forschungshintergrund und Motivation

Problemdefinition

Autoformaliserung ist die Aufgabe, mathematische Aussagen in natürlicher Sprache automatisch in maschinenverifizierbare Formeln der formalen Logik umzuwandeln. Die Kernherausforderungen dieses Problems sind:

  1. Semantische Kluft: Großer Unterschied zwischen der Mehrdeutigkeit der natürlichen Sprache und der Strenge der formalen Sprache
  2. Komplexität: Mathematische Aussagen aus der Praxis beinhalten häufig komplexe Konzepte und Inferenzketten
  3. Genauigkeitsanforderungen: Formalisierungsergebnisse müssen sowohl syntaktisch als auch semantisch korrekt sein

Bedeutung des Problems

Autoformaliserung ist von großer Bedeutung:

  • Mathematische Verifikation: Bietet Grundlagen für Theorembeweise und mathematische Verifikation
  • Transparenz der Inferenz: Formale Inferenz ist systematischer, transparenter und strenger als Inferenz in natürlicher Sprache
  • Automatisierungsbedarf: Manuelle Formalisierung erfordert umfangreiches Fachwissen und zeitliche Ressourcen

Einschränkungen bestehender Methoden

Bestehende LLM-basierte Autoformaliserungssysteme weisen folgende Probleme auf:

  1. Monolithische Architektur-Einschränkungen: Ein einzelnes LLM kann komplexe reale Autoformaliserungsprobleme schwer bewältigen
  2. Mangel an Modularität: Bestehende Implementierungen fehlt Modularität, Flexibilität und Skalierbarkeit
  3. Unzureichende Komponenteninteraktion: Kann mehrere interaktive Komponenten nicht effektiv integrieren

Forschungsmotivation

Die Motivation der Autoren für die Vorstellung des MASA-Frameworks ist:

  • Konstruktion eines modularen Multi-Agent-Systems zur Bewältigung der Komplexität der Autoformaliserung
  • Bereitstellung eines flexiblen und erweiterbaren Frameworks zur Unterstützung von Forschern bei der schnellen Entwicklung und Erweiterung von Systemen
  • Verbesserung der Effizienz und Zuverlässigkeit der Autoformaliserung durch Agentenzusammenarbeit

Kernbeiträge

  1. Vorstellung eines modularen Multi-Agent-Frameworks: MASA bietet ein modulares Framework zur Konstruktion von Multi-Agent-Systemen für Autoformaliserung mit guter Flexibilität und Skalierbarkeit
  2. Demonstration realer Anwendungen: Durch die Formalisierung realer mathematischer Definitionen durch Agenten wird das praktische Potenzial des Frameworks hervorgehoben
  3. Systematische Bewertung: Bewertung des Frameworks unter drei Multi-Agent-Einstellungen, Nachweis seiner Wirksamkeit und Bereitstellung wertvoller Erkenntnisse. Das endgültige iterative Selbstverbesserungssystem erreicht Formalisierungsraten von 35,25% auf Qwen2.5-7B und 61,89% auf GPT-4.1-mini, die syntaktisch korrekt und semantisch ausgerichtet sind
  4. Open-Source-Implementierung: Bereitstellung vollständiger Code und Daten zur Senkung der Forschungshürden

Methodische Details

Aufgabendefinition

Autoformaliserung kann als eine Transformationsfunktion A definiert werden, die eine natürlichsprachliche Aussage s auf ihre formale Darstellung φ = A(s) abbildet. Traditionelle Methoden werden durch LLM-Prompting implementiert: A = LLM(prompt). MASA erweitert diese Definition durch die Implementierung eines komplexeren Transformationsprozesses über ein Multi-Agent-System.

Modellarchitektur

Das MASA-Framework enthält fünf Kernkomponenten:

1. Agent (Agent)

Agenten sind grundlegende Elemente, die spezifische Funktionen ausführen, einschließlich:

  • AutoformalizationAgent: Führt Few-Shot-Autoformaliserung durch
  • HardCritiqueAgent: Bietet Kritik auf syntaktischer Ebene basierend auf Theorembeweisern
  • SoftCritiqueAgent: Bietet Kritik auf semantischer Ebene basierend auf LLM
  • FormalRefinementAgent: Verbessert Formalisierungscode basierend auf harter Kritik
  • InformalRefinementAgent: Verbessert Formalisierungscode basierend auf weicher Kritik
  • DenoisingAgent: Werkzeug-Agent zur Rauschunterdrückung
  • ImportRetrievalAgent: Werkzeug-Agent zur Import-Abrufung

2. Large Language Model (Großes Sprachmodell)

LLM bietet Agenten Inferenz- und Sprachfähigkeiten und unterstützt:

  • OpenAI-Modelle (wie GPT-4.1-mini)
  • Lokale HuggingFace-Modelle (wie Qwen2.5-7B, DeepSeek-Math)

3. Knowledge Base (Wissensbasis)

Speichert Informationen über formale Sprachbibliotheken und unterstützt den Abruf relevanter Kenntnisse. Die aktuelle Implementierung umfasst eine Wissensbasis mit Isabelle/HOL-Formalaussagen und -beweisen.

4. Retriever (Abrufer)

Ordnet Datenpunkte in mathematischen Bibliotheken nach Relevanz. Die aktuelle Implementierung basiert auf der BM25-Methode.

5. Theorem Prover (Theorembeweiser)

Verifiziert die syntaktische Korrektheit und Logik der Formalisierung und bietet Fehlermeldungen. Unterstützt:

  • Isabelle (über dedizierten Server)
  • Lean4 (über REPL)

Technische Innovationen

  1. Modulares Design: Verwendung von abstrakten Basisklassen-Designs zur einfachen Erweiterung neuer Agenten und Werkzeuge
  2. Mehrstufiger Kritik-Mechanismus: Kombination von harter Kritik (Syntax) und weicher Kritik (Semantik)
  3. Iterativer Verbesserungsprozess: Unterstützung für mehrere Runden der Selbstverbesserung durch Agentenzusammenarbeit
  4. Integration von Werkzeug-Agenten: Integration praktischer Werkzeuge wie Rauschunterdrückung und Import-Abrufung

Experimentelle Einrichtung

Datensätze

  1. miniF2F: Bietet echte Formalisierungen in Isabelle/HOL und Lean4 für Benchmark-Tests
  2. ProofNet: Bietet echte Formalisierungen von Lean4-Code

Bewertungsmetriken

Syntaktische Korrektheit

  • Pass Rate: Prozentsatz syntaktisch korrekter Formalisierungen

Semantische Bewertung

  • BLEU-4: N-Gramm-Überlappung mit echten Formalisierungen
  • ChrF: Zeichenebenen-F-Score
  • RUBY: Code-Migrations-Bewertungsmetrik

Agent-Bewertung

  • Alignment Faithfulness (AF): Ob der Formalisierungscode die natürlichsprachliche Semantik genau ausrichtet
  • Formalization Correctness (FC): Ob der Formalisierungscode selbst gültig, natürlich und gut formatiert ist

Vergleichsmethoden

  • Zero-Shot-Prompting (ZS): Direktes LLM-Prompting für Formalisierung
  • Few-Shot-Prompting (FS): Formalisierung mit 3 Beispielen
  • Verschiedene LLM-Kombinationen: GPT-4.1-mini, DeepSeek-Math-7B, Qwen2.5-7B

Implementierungsdetails

  • Verwendung von GPT-4.1-mini als Backend-LLM für den Soft-Critique-Agent
  • Unterstützung für zwei formale Sprachen: Isabelle/HOL und Lean4
  • Bereitstellung vollständiger Python-Implementierung und Jupyter-Notebook-Beispiele

Experimentelle Ergebnisse

Hauptergebnisse

Hard-Critique-Formalisierungsverbesserungssystem (Tabelle 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%)

Soft-Critique-Informale-Verbesserungssystem (Tabelle 2)

miniF2F (Lean4):

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

Iterative Selbstverbesserungsexperimente

Abbildung 2 zeigt Ergebnisse:

  • Qwen2.5-7B: Nach 4 Iterationen erreicht der Anteil syntaktisch korrekter und semantisch ausgerichteter Formalisierungen 35,25%
  • GPT-4.1-mini: Nach 4 Iterationen erreicht der Anteil syntaktisch korrekter und semantisch ausgerichteter Formalisierungen 61,89%

Experimentelle Erkenntnisse

  1. Few-Shot übertrifft Zero-Shot: Few-Shot-Lernen verbessert die Leistung in allen Einstellungen erheblich
  2. Modellkapazität hat Auswirkungen: Starke Modelle (GPT-4.1-mini) zeigen bessere Leistung bei der Formalisierungsverbesserung
  3. Iterative Verbesserung ist wirksam: Mehrere Iterationen können die Formalisierungsqualität kontinuierlich verbessern
  4. Modellübergreifende Verbesserung: Starke Modelle können die Ausgaben schwacher Modelle verbessern

Verwandte Arbeiten

Autoformaliserungsforschung

  • Prompting-Methoden: Wu et al. (2022) und andere verwenden LLM-Prompting für Autoformaliserung
  • Datengenerierung: Jiang et al. (2024) und Liu et al. (2025b) entwickeln großflächige parallele Korpora
  • Systemimplementierung: Bestehende Systeme fehlt Modularität und Skalierbarkeit

Multi-Agent-Systeme

  • Anwendungsbereiche: Betriebssysteme, medizinische Ausbildung, Antwortverifikation usw.
  • Inferenzaufgaben: Arithmetische Inferenz und allgemeine Inferenz
  • Autoformaliserungsanwendung: Forschung zu Multi-Agent-Systemen im Autoformaliserungsbereich ist begrenzt

Schlussfolgerung und Diskussion

Hauptschlussfolgerungen

  1. Framework-Wirksamkeit: MASA konstruiert erfolgreich ein modulares Multi-Agent-Autoformaliserungssystem
  2. Leistungsverbesserung: Multi-Agent-Zusammenarbeit verbessert die Genauigkeit der Autoformaliserung erheblich
  3. Praktischer Wert: Das Framework bietet Forschern eine flexible Entwicklungsplattform

Einschränkungen

  1. Mangel an zentraler Kontrolle: Das System verfügt über keinen zentralen Agenten zur Zuweisung und Kontrolle verschiedener Agenten
  2. Einschränkungen der semantischen Bewertung: Die semantische Bewertung ist auf hochrangige Urteile beschränkt und erfordert feinkörnigere Bewertungsstandards
  3. Modellabhängigkeit: Die Systemleistung hängt stark von den Fähigkeiten des zugrunde liegenden LLM ab

Zukünftige Richtungen

  1. Verbesserung der zentralen Kontrolle: Entwicklung fortgeschrittenerer Multi-Agent-System-Kontrollmechanismen
  2. Verfeinerung der Bewertung: Etablierung feinkörnigerer semantischer Bewertungsstandards
  3. Erweiterung der Anwendung: Anwendung des Frameworks auf breitere Formalisierungsaufgaben

Tiefgreifende Bewertung

Stärken

  1. Starke Innovativität: Erstes systematisches Multi-Agent-Autoformaliserungsframework
  2. Vernünftiges Design: Elegantes modulares Architektur-Design, leicht zu erweitern
  3. Umfangreiche Experimente: Umfasst mehrere Einstellungen und Bewertungsmetriken
  4. Hoher praktischer Wert: Open-Source-Implementierung senkt Forschungshürden
  5. Überzeugende Ergebnisse: Validierung der Methodenwirksamkeit auf mehreren Datensätzen

Mängel

  1. Unzureichende theoretische Analyse: Mangel an theoretischer Analyse der Multi-Agent-Kooperationsmechanismen
  2. Rechenkostenanalyse: Analyse der Rechenkostenbelastung von Multi-Agent-Systemen ist unzureichend
  3. Fehlerausbreitung: Unzureichende Analyse der Fehlerausbreitungsprobleme zwischen Agenten
  4. Bewertungseinschränkungen: Semantische Bewertung basiert immer noch auf LLM-Urteilen, die möglicherweise verzerrt sind

Einfluss

  1. Akademischer Beitrag: Bietet ein neues Paradigma für die Autoformaliserungsforschung
  2. Praktischer Wert: Framework kann direkt für praktische Anwendungsentwicklung verwendet werden
  3. Reproduzierbarkeit: Vollständige Open-Source-Implementierung gewährleistet Reproduzierbarkeit
  4. Förderung der Entwicklung: Wird wahrscheinlich die Anwendung von Multi-Agent-Systemen im Formalisierungsbereich fördern

Anwendungsszenarien

  1. Mathematische Formalisierung: Geeignet für Autoformaliserung komplexer mathematischer Theoreme und Definitionen
  2. Bildungsanwendungen: Kann für Formalisierungstraining im mathematischen Unterricht verwendet werden
  3. Forschungswerkzeug: Bietet eine Grundplattform für Autoformaliserungsforschung
  4. Industrielle Anwendung: Kann in Softwaresystemen integriert werden, die formale Verifikation erfordern

Referenzen

Wichtige Referenzen umfassen:

  • 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

Zusammenfassung: MASA ist ein innovatives Multi-Agent-Autoformaliserungsframework, das durch modulares Design und Agentenzusammenarbeit die Wirksamkeit der Autoformaliserung erheblich verbessert. Diese Arbeit zeigt hervorragende Leistungen in technischer Innovation, experimenteller Validierung und praktischem Wert und eröffnet neue Richtungen für die Autoformaliserungsforschung. Trotz einiger Einschränkungen macht seine Open-Source-Implementierung und gute Erweiterbarkeit es zu einem wichtigen Beitrag auf diesem Gebiet.