# MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?

arXiv: https://arxiv.org/abs/2506.06034 · HTML: https://mlsanity.com/paper/2506.06034/

## Key facts

- Cited by 13 papers in the map (data through 14 Oct 2026).
- Placed in VLM benchmarks and visual reasoning, one of 16 directions in Multimodal LLMs / vision-language models.
- Builds on 42 of its 59 references that are in the map.
- First posted on arXiv 6 Jun 2025.

## Placed in

- Multimodal LLMs / vision-language models / [VLM benchmarks and visual reasoning](https://mlsanity.com/mllm/vlm-benchmarks-and-visual-reasoning/)

## Builds on (most cited first, 30 of 42)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Measuring Massive Multitask Language Understanding](https://mlsanity.com/paper/2009.03300/) (2020)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Improved Baselines with Visual Instruction Tuning](https://mlsanity.com/paper/2310.03744/) (2023)
- [MMMU: A Massive Multi-discipline Multimodal Understanding and Reasoning Benchmark for Expert AGI](https://mlsanity.com/paper/2311.16502/) (2023)
- [MathVista: Evaluating Mathematical Reasoning of Foundation Models in Visual Contexts](https://mlsanity.com/paper/2310.02255/) (2023)
- [ChartQA: A Benchmark for Question Answering about Charts with Visual and Logical Reasoning](https://mlsanity.com/paper/2203.10244/) (2022)
- [MathQA: Towards Interpretable Math Word Problem Solving with Operation-Based Formalisms](https://mlsanity.com/paper/1905.13319/) (2019)
- [Program Induction by Rationale Generation : Learning to Solve and Explain Algebraic Word Problems](https://mlsanity.com/paper/1705.04146/) (2017)
- [MathVerse: Does Your Multi-modal LLM Truly See the Diagrams in Visual Math Problems?](https://mlsanity.com/paper/2403.14624/) (2024)
- [Measuring Multimodal Mathematical Reasoning with MATH-Vision Dataset](https://mlsanity.com/paper/2402.14804/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [Towards Reasoning Era: A Survey of Long Chain-of-Thought for Reasoning Large Language Models](https://mlsanity.com/paper/2503.09567/) (2025)
- [Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning](https://mlsanity.com/paper/2105.04165/) (2021)
- [Set-of-Mark Prompting Unleashes Extraordinary Visual Grounding in GPT-4V](https://mlsanity.com/paper/2310.11441/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Mathematical Capabilities of ChatGPT](https://mlsanity.com/paper/2301.13867/) (2023)
- [Visual Sketchpad: Sketching as a Visual Chain of Thought for Multimodal Language Models](https://mlsanity.com/paper/2406.09403/) (2024)
- [What does CLIP know about a red circle? Visual prompt engineering for VLMs](https://mlsanity.com/paper/2304.06712/) (2023)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression](https://mlsanity.com/paper/2212.02746/) (2022)

## Built on by (most cited first, 13 of 13)

- [Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models](https://mlsanity.com/paper/2506.17114/) (2025)
- [LeanGeo: Formalizing Competitional Geometry problems in Lean](https://mlsanity.com/paper/2508.14644/) (2025)
- [GeoSketch: A Neural-Symbolic Approach to Geometric Multimodal Reasoning with Auxiliary Line Construction and Affine Transformation](https://mlsanity.com/paper/2509.22460/) (2025)
- [GGBench: A Geometric Generative Reasoning Benchmark for Unified Multimodal Models](https://mlsanity.com/paper/2511.11134/) (2025)
- [RebuttalAgent: Strategic Persuasion in Academic Rebuttal via Theory of Mind](https://mlsanity.com/paper/2601.15715/) (2026)
- [Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4](https://mlsanity.com/paper/2510.26094/) (2025)
- [FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?](https://mlsanity.com/paper/2603.26996/) (2026)
- [PAGER: Bridging the Semantic-Execution Gap in Point-Precise Geometric GUI Control](https://mlsanity.com/paper/2605.15963/) (2026)
- [Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean](https://mlsanity.com/paper/2607.19374/) (2026)
- [PyFi: Toward Pyramid-like Financial Image Understanding for VLMs via Adversarial Agents](https://mlsanity.com/paper/2512.14735/) (2025)
- [Verifiable Geometry Problem Solving: Solver-Driven Autoformalization and Theorem Proposing](https://mlsanity.com/paper/2606.27926/) (2026)
- [An Analysis of Training-Free Self-Reported Confidence in Language Models](https://mlsanity.com/paper/2609.20541/) (2026)
- [Mind or Message? Auditing Theory of Mind in Multi-Agent Social Simulation](https://mlsanity.com/paper/2609.24146/) (2026)

## Abstract (arXiv)

Numerous theorems, such as those in geometry, are often presented in multimodal forms (e.g., diagrams). Humans benefit from visual reasoning in such settings, using diagrams to gain intuition and guide the proof process. Modern Multimodal Large Language Models (MLLMs) have demonstrated remarkable capabilities in solving a wide range of mathematical problems. However, the potential of MLLMs as Automated Theorem Provers (ATPs), specifically in the multimodal domain, remains underexplored. In this paper, we introduce the Multimodal Automated Theorem Proving benchmark (MATP-BENCH), a new Multimodal, Multi-level, and Multi-language benchmark designed to evaluate MLLMs in this role as multimodal automated theorem provers. MATP-BENCH consists of 1056 multimodal theorems drawn from high school, university, and competition-level mathematics. All these multimodal problems are accompanied by formalizations in Lean 4, Coq and Isabelle, thus making the benchmark compatible with a wide range of theorem-proving frameworks. MATP-BENCH requires models to integrate sophisticated visual understanding with mastery of a broad spectrum of mathematical knowledge and rigorous symbolic reasoning to generate formal proofs. We use MATP-BENCH to evaluate a variety of advanced multimodal language models. Existing methods can only solve a limited number of the MATP-BENCH problems, indicating that this benchmark poses an open challenge for research on automated theorem proving.