MA-LoT: Multi-Agent Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving

• URL: http://arxiv.org/abs/2503.03205v2
• Date: Mon, 10 Mar 2025 17:39:42 GMT
• Title: MA-LoT: Multi-Agent Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving
• Authors: Ruida Wang, Rui Pan, Yuxin Li, Jipeng Zhang, Yizhen Jia, Shizhe Diao, Renjie Pi, Junjie Hu, Tong Zhang,
• Abstract summary: State-of-the-art methods utilize single Large Language Models (LLMs) as agents or provers to either generate complete proof or perform tree searches.<n>We propose MA-LoT: Multi-Agent Lean-based Long Chain-of-Prover framework.<n>We show that our framework achieves a 61.07% accuracy rate on the Lean4 version of the MiniF2F-Test dataset.
• Score: 30.112351299773632
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Solving mathematical problems using computer-verifiable languages like Lean has significantly impacted mathematical and computer science communities. State-of-the-art methods utilize single Large Language Models (LLMs) as agents or provers to either generate complete proof or perform tree searches. However, single-agent methods inherently lack a structured way to combine high-level reasoning in Natural Language (NL) with Formal Language (FL) verification feedback. To solve these issues, we propose MA-LoT: Multi-Agent Lean-based Long Chain-of-Thought framework, (to the best of our knowledge), the first multi-agent framework for Lean4 theorem proving that balance high-level NL reasoning and FL verification in Long CoT. Using this structured interaction, our approach enables deeper insights and long-term coherence in proof generation, with which past methods struggle. We do this by leveraging emergent formal reasoning ability in Long CoT using our novel LoT-Transfer Learning training-inference pipeline. Extensive experiments show that our framework achieves a 61.07% accuracy rate on the Lean4 version of the MiniF2F-Test dataset, largely outperforming GPT-4 (22.95%), single-agent tree search (InternLM-Step-Prover, 50.70%), and whole-proof generation (Godel-Prover, 55.33%) baselines. Furthermore, our findings highlight the potential of combining Long CoT with formal verification for a more insightful generation in a broader perspective.

Related papers

• Unlocking General Long Chain-of-Thought Reasoning Capabilities of Large Language Models via Representation Engineering [59.34894142132706]
  Existing work finds that the capability of long CoT reasoning can be efficiently elicited by tuning on only a few examples. This motivates us to investigate whether long CoT reasoning is a general capability for LLMs. We propose GLoRE, a novel representation engineering method to unleash the general long CoT reasoning capabilities of LLMs.
  arXiv  Detail & Related papers  (2025-03-14T11:30:37Z)
• When More is Less: Understanding Chain-of-Thought Length in LLMs [53.77747102201451]
  Chain-of-thought (CoT) reasoning enhances the multi-step reasoning capabilities of large language models (LLMs)<n>However, for most models and tasks, does an increase in CoT length consistently lead to improved reasoning accuracy?<n>In this paper, we observe a nuanced relationship: as the number of reasoning steps increases, performance initially improves but eventually decreases.
  arXiv  Detail & Related papers  (2025-02-11T05:28:59Z)
• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  We propose ProofAug, a novel theorem proving method that enjoys superior sample efficiency. Our method is validated on the miniF2F-test benchmark using the open-source deepseek-math-7b-base model and the Isabelle proof assistant.
  arXiv  Detail & Related papers  (2025-01-30T12:37:06Z)
• From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs [25.69931278771869]
  This paper focuses on formal verification, an immediate application scenario of formal reasoning.<n>We constructed 18k high-quality instruction-response pairs across five formal specification languages.<n>Fine-tuning with formal data also enhances mathematics, reasoning, and coding capabilities.
  arXiv  Detail & Related papers  (2025-01-27T17:00:56Z)
• Insight-V: Exploring Long-Chain Visual Reasoning with Multimodal Large Language Models [64.1799100754406]
  Large Language Models (LLMs) demonstrate enhanced capabilities and reliability by reasoning more. Despite various efforts to improve LLM reasoning, high-quality long-chain reasoning data and optimized training pipelines still remain inadequately explored in vision-language tasks. We present Insight-V, an early effort to 1) scalably produce long and robust reasoning data for complex multi-modal tasks, and 2) an effective training pipeline to enhance the reasoning capabilities of MLLMs.
  arXiv  Detail & Related papers  (2024-11-21T18:59:55Z)
• FLARE: Faithful Logic-Aided Reasoning and Exploration [50.9814063216852]
  We introduce a novel approach for traversing the problem space using task decompositions.<n>We use the Large Language Models to plan a solution, soft-formalise the query into facts and predicates using a logic programming code.<n>Our method allows us to compute the faithfulness of the reasoning process w.r.t. the generated code and analyse the steps of the multi-hop search without relying on external solvers.
  arXiv  Detail & Related papers  (2024-10-14T19:39:11Z)
• Proof Automation with Large Language Models [6.587933406842906]
  Large Language Models (LLMs) have shown promise in automatically generating informal proofs in natural language. We propose PALM, a novel generate-then-repair approach that first prompts an LLM to generate an initial proof and then leverages targeted symbolic methods to iteratively repair low-level problems. Our results show that PALM significantly outperforms other state-of-the-art approaches, successfully proving 76.6% to 180.4% more theorems.
  arXiv  Detail & Related papers  (2024-09-22T00:19:27Z)
• TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts [26.98890165420689]
  TheoremLlama is an end-to-end framework that trains a general-purpose Lean4 expert. Our framework achieves cumulative accuracies of 36.48% and 33.61% on MiniF2F-Valid and Test datasets respectively.
  arXiv  Detail & Related papers  (2024-07-03T15:36:18Z)
• Faithful Explanations of Black-box NLP Models Using LLM-generated Counterfactuals [67.64770842323966]
  Causal explanations of predictions of NLP systems are essential to ensure safety and establish trust. Existing methods often fall short of explaining model predictions effectively or efficiently. We propose two approaches for counterfactual (CF) approximation.
  arXiv  Detail & Related papers  (2023-10-01T07:31:04Z)
• T-SciQ: Teaching Multimodal Chain-of-Thought Reasoning via Mixed Large Language Model Signals for Science Question Answering [59.63860993280275]
  Large Language Models (LLMs) have demonstrated exceptional performance in various Natural Language Processing (NLP) tasks. We propose a novel method termed T-SciQ that aims at teaching science question answering with LLM signals. Our approach achieves a new state-of-the-art performance on the ScienceQA benchmark, with an accuracy of 96.18%.
  arXiv  Detail & Related papers  (2023-05-05T11:56:30Z)
• Multimodal Chain-of-Thought Reasoning in Language Models [94.70184390935661]
  We propose Multimodal-CoT that incorporates language (text) and vision (images) modalities into a two-stage framework. Experimental results on ScienceQA and A-OKVQA benchmark datasets show the effectiveness of our proposed approach.
  arXiv  Detail & Related papers  (2023-02-02T07:51:19Z)
• Proof Artifact Co-training for Theorem Proving with Language Models [4.934817254755007]
  PACT (bf Proof bf Artifact bf Co-bf Training) is a general methodology for extracting self-supervised data from kernel-level proof terms for co-training. We instrument Lean with a neural theorem prover driven by a Transformer language model and show that PACT improves theorem proving success rate on a held-out suite of test theorems from 32% to 48%.
  arXiv  Detail & Related papers  (2021-02-11T18:59:24Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.