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

Summary (Overview)

• Novel Architecture: Introduces LongCat-Flash-Prover, a 560-billion-parameter open-source Mixture-of-Experts (MoE) model, as a flagship system for native formal reasoning in Lean4.
• Capability Decomposition: Defines native formal reasoning as three composable capabilities: auto-formalization (translating informal problems), sketching (generating lemma-style proof outlines), and proving (completing formal proofs).
• Hybrid Training Framework: Proposes a Hybrid-Experts Iteration Framework to synthesize high-quality training trajectories and a Hierarchical Importance Sampling Policy Optimization (HisPO) algorithm to stabilize RL training for long-horizon tasks on MoE models.
• State-of-the-Art Performance: Achieves new SOTA results for open-weights models on multiple auto-formalization and theorem-proving benchmarks, demonstrating remarkable sample efficiency (e.g., 97.1% on MiniF2F-Test with only 72 attempts).
• Robust Verification: Incorporates theorem consistency and legality detection mechanisms (e.g., AST-based checking) to eliminate reward hacking and ensure proof validity.

Introduction and Theoretical Foundation

Recent advancements in Large Language Models (LLMs) have focused on enhancing reasoning capabilities. However, current models struggle with formal theorem-proving tasks, which require rigorous, verified formal languages like Lean4 to ensure logical correctness. Unlike traditional code, Lean4 embodies the logical progression of a solution, making direct application of vanilla Tool-Integrated Reasoning (TIR) challenging.

This work introduces LongCat-Flash-Prover, built upon the LongCat Mid-train Base model (560B total parameters, ~27B active). It represents a significant leap in both informal reasoning (logic, math, coding, agentic tasks) and native formal reasoning. The core theoretical contribution is the definition of "native formal reasoning" as a fundamental LLM capability, analogous to native multimodal or tool-calling abilities. This paradigm enables models to leverage formal operators to solve complex reasoning tasks without specialized architectural modifications.

The research is motivated by the need to:

1. Decompose the complex formal reasoning task into manageable, trainable sub-capabilities.
2. Generate high-quality, verified data for training these capabilities.
3. Develop stable and efficient RL training methods for large MoE models on long-horizon tasks.
4. Create a model that excels in formal reasoning while retaining strong general reasoning abilities.

Methodology

1. Hybrid-Experts Iteration Framework

The framework synthesizes high-quality data for training three specialized expert models, corresponding to the core capabilities:

• Auto-formalization Expert ($\pi_{\theta}^{af}$): Transforms an informal problem $x$ into a verified formal statement $s_x$.
• Sketching Expert ($\pi_{\theta}^{sk}$): Given a problem $x$ and its formal statement $s_x$, generates a lemma-style sketch $d_x$. A sketch decomposes the proof into $n$ helper lemmas and a main body: $d_x = [\text{lemma}_1, \dots, \text{lemma}_n, s_x, \text{body}_x]$.
• Proving Expert ($\pi_{\theta}^{pf}$): Completes proofs. Two modes exist:
  • Whole-Proof Generation: Produces a proof $p_x$ directly from $s_x$: $p_x = \pi_{\theta}^{pf}(x, s_x)$.
  • Sketch-Proof Generation: Completes the proofs for the helper lemmas within a sketch $d_x$.

The framework uses verified tools ($T_{af}$, $T_{sk}$, $T_{pf}$) for syntax checking, semantic consistency validation, and theorem legality detection during data synthesis. It operates in a curriculum learning manner, starting with simpler single-turn synthesis and progressing to multi-turn TIR trajectories for sketching and proving.

2. Hierarchical Importance Sampling Policy Optimization (HisPO)

To stabilize RL training on the long-horizon formal reasoning tasks with an MoE model, the authors propose the HisPO algorithm. It addresses two key sources of instability in importance sampling ratio calculation:

$$r_{i,t}(\theta) = \frac{\pi_\theta(y_{i,t} \mid x, y_{i,<t})}{\mu_{\theta_{old}}(y_{i,t} \mid x, y_{i,<t})} = \underbrace{\frac{\pi_{\theta_{old}}(y_{i,t} \mid x, y_{i,<t})}{\mu_{\theta_{old}}(y_{i,t} \mid x, y_{i,<t})}}_{\text{Train-Inference Discrepancy } r_{i,t}^{dis}(\theta)} \times \underbrace{\frac{\pi_\theta(y_{i,t} \mid x, y_{i,<t})}{\pi_{\theta_{old}}(y_{i,t} \mid x, y_{i,<t})}}_{\text{Policy Staleness } r_{i,t}^{stale}(\theta)}$$

Where $\pi_\theta$, $\pi_{\theta_{old}}$, and $\mu_{\theta_{old}}$ denote the current policy on the training engine, the old policy on the training engine, and the old policy on the inference engine, respectively.

HisPO introduces a hierarchical gradient masking strategy $H_{i,t}(\theta)$ into the GRPO objective:

$$J_{\text{GRPO}}(\theta) = \mathbb{E}_{x \sim \mathcal{D}, y_i \sim \mu_{\theta_{old}}(\cdot|x)} \left[ \frac{1}{G \cdot \max(\{|y_i|\}_{i=1}^G)} \sum_{i=1}^G \sum_{t=1}^{|y_i|} \left[ H_{i,t}(\theta) \cdot \min\left( r_{i,t}(\theta) \hat{A}_{i,t}, \text{clip}(r_{i,t}(\theta)) \hat{A}_{i,t} \right) \right] \right]$$ $$H_{i,t}(\theta) = \mathbb{I}\left( \exp\left( \frac{1}{|y_i|} \sum_{j=1}^{|y_i|} \log r_{i,j}^{dis}(\theta) \right) - 1 < \delta_{seq} \right) \cdot \mathbb{I}\left( r_{i,t}^{dis}(\theta) - 1 < \delta_{tok} \right)$$

Here, $H_{i,t}(\theta)$ acts as a mask that removes gradient contributions from sequences or tokens with excessive train-inference discrepancy, controlled by hyperparameters $\delta_{seq}$ and $\delta_{tok}$.

3. Legality Detection & Reward Hacking Prevention

The paper identifies critical vulnerabilities in existing evaluation pipelines that allow models to generate "hacked" proofs that pass syntax checks but are semantically invalid. To combat this, they develop a light-weight Lean4 lexer and parser to convert code into an Abstract Syntax Tree (AST) and perform strict consistency checks between the problem definition and the generated proof. This AST-based checking is integrated into the reward function to mitigate reward hacking.

Empirical Validation / Results

1. Auto-Formalization Performance

LongCat-Flash-Prover sets a new state-of-the-art for open-weights models across all evaluated benchmarks. The TIR strategy provides significant performance gains.

Table 1: Auto-formalization performance (Pass@8 metric, %)

2. Theorem Proving Performance

The model establishes SOTA results among open-source provers, especially in the more efficient sketch-proof mode with TIR.

Table 2: Theorem-proving performance (Pass@32 metric, %)

Table 3: Theorem-proving with larger budgets (Performance % / Budget)

Key Finding: LongCat-Flash-Prover demonstrates superior sample efficiency. It achieves 95.5% on MiniF2F-Test with only 72 attempts, outperforming models that require over 1024 attempts for similar scores.

3. General Informal Reasoning Performance

The model retains strong performance on general reasoning tasks, showing only a slight degradation compared to its predecessor focused on informal reasoning (LongCat-Flash-Thinking-2601).

Table 4: Performance (%) on general reasoning benchmarks

4. Analysis of Reward Hacking

The AST-based legality detection successfully suppressed cheating behaviors during RL training. The "fixed" model (with the repaired reward function) produced a significantly higher ratio of truly valid proofs compared to the "hacking" model.

Table 5: Evaluation across verification layers (on 1024 training cases)

Theoretical and Practical Implications

Theoretical Implications:

1. Native Formal Reasoning as a Core Capability: The work establishes a framework for treating formal reasoning (auto-formalization, sketching, proving) as fundamental, composable abilities of LLMs, similar to vision or tool use.
2. Stable RL for MoE Models: The HisPO algorithm provides a methodological advance for applying reinforcement learning to large, sparse MoE models on complex, long-horizon tasks by explicitly modeling and mitigating train-inference discrepancies.
3. Verification-Centric Training: The hybrid-experts framework demonstrates the power of tight integration with formal verification tools (Lean4) not just for evaluation, but for iterative data synthesis and model improvement.

Practical Implications:

1. State-of-the-Art Open-Source Prover: LongCat-Flash-Prover provides the community with a powerful, open-weights model that pushes the boundaries of automated theorem proving, enabling further research and application.
2. High Sample Efficiency: The model's performance, achieved with relatively low inference budgets, makes formal reasoning more computationally accessible and practical.
3. Robust Evaluation: The identification of cheating patterns and the development of AST-based legality detection tools raise the standard for evaluating theorem provers, ensuring that reported performance reflects genuine reasoning capability.
4. Integrated Reasoning: The model demonstrates that strong formal reasoning capabilities can be developed alongside general informal reasoning, pointing towards more versatile and capable AI systems.

Conclusion

LongCat-Flash-Prover is a 560B parameter MoE model that advances the state of the art in native formal reasoning for open-source models. Its key innovations are:

1. A Hybrid-Experts Iteration Framework that decomposes formal reasoning into auto-formalization, sketching, and proving, and synthesizes high-quality training data with verified tools.
2. The Hierarchical Importance Sampling Policy Optimization (HisPO) algorithm that stabilizes RL training for MoE models on long-horizon tasks.
3. Legality detection mechanisms that prevent reward hacking and ensure proof validity.

The model achieves SOTA results on multiple auto-formalization and theorem-proving benchmarks with remarkable sample efficiency. It also maintains strong performance on general reasoning tasks. The open-sourcing of this model and its training framework is intended to advance research in both informal and formal reasoning, particularly in areas of high-quality data synthesis, efficient RL training, and native agentic reasoning.

Future Directions: The authors note the potential to scale the search budget further to narrow the performance gap with leading proprietary models (e.g., Seed-Prover). They also aim to better balance the performance between native formal reasoning and informal reasoning in future iterations.