LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning

• URL: http://arxiv.org/abs/2603.21065v1
• Date: Sun, 22 Mar 2026 05:16:09 GMT
• Title: LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning
• Abstract summary: LongCat-Flash-Prover is an open-source MoE model for agentic tool-integrated reasoning.<n>It sets a new state-of-the-art for open-weights models in both auto-formalization and theorem proving.<n>It achieves a 97.1% pass rate on MiniF2F-Test using only 72 inference budget per problem.
• Score: 46.294745464571456
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce LongCat-Flash-Prover, a flagship 560-billion-parameter open-source Mixture-of- Experts (MoE) model that advances Native Formal Reasoning in Lean4 through agentic tool-integrated reasoning (TIR). We decompose the native formal reasoning task into three independent formal capabilities, i.e., auto-formalization, sketching, and proving. To facilitate these capabilities, we propose a Hybrid-Experts Iteration Framework to expand high-quality task trajectories, including generating a formal statement based on a given informal problem, producing a whole-proof directly from the statement, or a lemma-style sketch. During agentic RL, we present a Hierarchical Importance Sampling Policy Optimization (HisPO) algorithm, which aims to stabilize the MoE model training on such long-horizon tasks. It employs a gradient masking strategy that accounts for the policy staleness and the inherent train-inference engine discrepancies at both sequence and token levels. Additionally, we also incorporate theorem consistency and legality detection mechanisms to eliminate reward hacking issues. Extensive evaluations show that our LongCat-Flash-Prover sets a new state-of-the-art for open-weights models in both auto-formalization and theorem proving. Demonstrating remarkable sample efficiency, it achieves a 97.1% pass rate on MiniF2F-Test using only 72 inference budget per problem. On more challenging benchmarks, it solves 70.8% of ProverBench and 41.5% of PutnamBench with no more than 220 attempts per problem, significantly outperforming existing open-weights baselines.

Related papers

• VibeThinker-3B: Exploring the Frontier of Verifiable Reasoning in Small Language Models [10.513021831152363]
  This report introduces VibeThinker-3B, a compact dense model with 3B parameters developed to investigate how far verifiable reasoning can be pushed within a strictly small-model regime.<n> Experimental evaluations demonstrate that VibeThinker-3B achieves frontier-level performance on highly demanding verifiable tasks.
  arXiv  Detail & Related papers  (2026-06-15T02:57:19Z)
• Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation [27.324913853284404]
  Pythagoras-Prover is a compute-efficient family of Lean theorem provers built for practical compute budgets.<n>For training efficiency, we build a Lean-verified corpus stratified into easy, medium, and hard problems for curriculum SFT.<n>We also introduce Augmented Lean Formalisation (ALF), which expands scarce verified corpora into variants of formal statements.
  arXiv  Detail & Related papers  (2026-06-10T18:43:11Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate verifiable proofs in formal languages like Lean.<n>We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving.
  arXiv  Detail & Related papers  (2026-06-02T08:16:42Z)
• Training LLMs for Divide-and-Conquer Reasoning Elevates Test-Time Scalability [129.1296673737603]
  Large language models (LLMs) have demonstrated strong reasoning capabilities through step-by-step chain-of-thought (CoT) reasoning.<n>A potential alternative is divide-and-conquer (DAC) reasoning, which decomposes a complex problem into subproblems to facilitate more effective exploration of the solution.<n>We propose an end-to-end reinforcement learning (RL) framework to enhance their DAC-style reasoning capacity.
  arXiv  Detail & Related papers  (2026-02-02T18:54:54Z)
• Structured Uncertainty guided Clarification for LLM Agents [126.26213027785813]
  LLM agents extend large language models with tool-calling capabilities, but ambiguous user instructions often lead to incorrect invocations and task failures.<n>We introduce a principled formulation of structured uncertainty over tool-call parameters, modeling joint tool-argument clarification as a POMDP with Expected Value of Perfect Information (EVPI) objective for optimal question selection and aspect-based cost modeling to prevent redundancy.<n>Our SAGE-Agent leverages this structured uncertainty to achieve superior efficiency: increasing coverage on ambiguous tasks by 7-39% while reducing clarification questions by 1.5-2.7$times$ compared to strong prompting and uncertainty-based baselines.
  arXiv  Detail & Related papers  (2025-11-11T21:50:44Z)
• Introducing LongCat-Flash-Thinking: A Technical Report [116.75498493511026]
  LongCat-Flash-Thinking is an efficient open-source Mixture-of-Experts (MoE) reasoning model.<n>Its advanced capabilities are cultivated through a meticulously crafted training process.<n>LongCat-Flash-Thinking achieves state-of-the-art performance among open-source models on a suite of complex reasoning tasks.
  arXiv  Detail & Related papers  (2025-09-23T10:25:48Z)
• Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving [48.22540519786074]
  Recent studies show that the informal accuracy exceeds 80% while formal success remains below 8% on benchmarks like PutnamBench.<n>We propose a novel framework that decouples high-level reasoning from low-level proof generation.<n>We evaluate our method on a challenging set of post-2000 IMO problems, a problem set on which no prior open-source prover has reported success.
  arXiv  Detail & Related papers  (2025-07-07T22:38:49Z)
• Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs [11.87831709160905]
  We present Prover Agent, a novel AI agent for automated theorem proving.<n>It integrates large language models (LLMs) with a formal proof assistant, Lean.<n>It achieves an 88.1% success rate on the MiniF2F benchmark.
  arXiv  Detail & Related papers  (2025-06-24T18:01:52Z)
• Theorem Prover as a Judge for Synthetic Data Generation [22.124954482278536]
  We present a framework that replaces human annotation with theorem prover in Reinforcement Learning from Human Feedback (RLHF)<n>Across multiple large language models (LLMs), applying TP-as-a-Judge and RF improves benchmarks with only 3,508 samples, achieving 5.56% accuracy on Mistral-7B for MultiArithm.
  arXiv  Detail & Related papers  (2025-02-18T18:57:09Z)
• Chain of Evidences and Evidence to Generate: Prompting for Context Grounded and Retrieval Augmented Reasoning [3.117335706912261]
  Chain of Evidences (CoE) and Evidence to Generate (E2G) are built upon two unique strategies.<n>Instead of unverified reasoning claims, our innovative approaches leverage the power of "evidence for decision making"<n>Our framework consistently achieves remarkable results across various knowledge-intensive reasoning and generation tasks.
  arXiv  Detail & Related papers  (2024-01-11T09:49:15Z)

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.