mlsanityData to 14 Oct 2026

MASA: LLM-Driven Multi-Agent Systems for Autoformalization

arXiv 2510.08988 ↗First posted 10 Oct 2025cs.CL cs.FLcited by 6

On the map: LLM agents and tool use → General LLM agent frameworks and benchmarks

Abstract (arXiv)

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.

Key facts. Cited by 6 papers in the map (data through 14 Oct 2026). Placed in General LLM agent frameworks and benchmarks, one of 16 directions in LLM agents and tool use. Builds on 23 of its 45 references that are in the map. First posted on arXiv 10 Oct 2025.

Builds on

23 of 45 references.

References · 23

  1. 2020Language Models are Few-Shot Learnerscited by 32,419
  2. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 9,379
  3. 2023Judging LLM-as-a-Judge with MT-Bench and Chatbot Arenacited by 8,626
  4. 2022Self-Consistency Improves Chain of Thought Reasoning in Language Modelscited by 5,708
  5. 2024Qwen2.5 Technical Reportcited by 4,942
  6. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  7. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  8. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  9. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 192
  10. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  11. 2022NumGLUE: A Suite of Fundamental yet Challenging Mathematical Reasoning Taskscited by 112
  12. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 81
11 more
  1. 2019Does BLEU Score Work for Code Migration?cited by 49
  2. 2024Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistencycited by 41
  3. 2024Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Provingcited by 35
  4. 2024MEDCO: Medical Education Copilots Based on A Multi-Agent Frameworkcited by 33
  5. 2025ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Datacited by 23
  6. 2025Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitionscited by 22
  7. 2024Consistent Autoformalization for Constructing Mathematical Librariescited by 21
  8. 2024Enhancing Ethical Explanations of Large Language Models through Iterative Symbolic Refinementcited by 16
  9. 2025CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalizationcited by 16
  10. 2023A Symbolic Framework for Evaluating Mathematical Reasoning and Generalisation with Transformerscited by 15
  11. 2023Neural Machine Translation for Mathematical Formulaecited by 7

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2026: 6.

6 papers.

  1. 2026Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisationcited by 4
  2. 2026Monotonic Reference-Free Refinement for Autoformalizationcited by 1
  3. 2026Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theorycited by 1
  4. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  5. 2026LogicTrack: Auditing Reasoning Trajectories of Large Language Models with Formal Logic Solverscited by 1
  6. 2026ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimizationcited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025Autoformalization in the Era of Large Language Models: A Survey
  2. 2026Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
  3. 2025StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion
  4. 2024Towards Logically Sound Natural Language Reasoning with Logic-Enhanced Language Model Agents
  5. 2024A Survey on LLM-based Multi-Agent System: Recent Advances and New Frontiers in Application
  6. 2024Large Language Model based Multi-Agents: A Survey of Progress and Challenges
  7. 2025FMC: Formalization of Natural Language Mathematical Competition Problems
  8. 2025Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning