論文の概要: LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning
- arxiv url: http://arxiv.org/abs/2603.21065v1
- Date: Sun, 22 Mar 2026 05:16:09 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-24 19:11:39.221478
- Title: LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning
- Title（参考訳）: LongCat-Flash-Prover:エージェントツールによる強化学習によるネイティブ形式推論の強化
- Abstract要約: LongCat-Flash-Proverはエージェントツール統合推論のためのオープンソースのMoEモデルである。
これは、自己形式化と定理証明の両方において、オープンウェイトモデルのための新しい最先端状態を設定する。
MiniF2F-Testのパスレートは97.1%で、72の推論予算しか使用していない。
- 参考スコア（独自算出の注目度）: 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.
- Abstract（参考訳）: このモデルでは,エージェントツール統合推論(TIR)を通じて,Lean4のNative Formal Reasoning(Native Formal Reasoning)を進化させる。
我々は、ネイティブな形式推論タスクを、3つの独立した形式的能力、すなわち自動形式化、スケッチ、証明に分解する。
これらの機能を実現するために,与えられた非公式な問題に基づいて形式文を生成すること,ステートメントから直接全文を生成すること,あるいはレムマスタイルのスケッチを含む,高品質なタスクトラジェクトリを拡張するハイブリット・エキスパート・イテレーション・フレームワークを提案する。
エージェントRLでは,階層的重要度サンプリングポリシー最適化(HisPO)アルゴリズムが提案される。
それは、ポリシーの不安定さと、シーケンスレベルとトークンレベルの両方で固有の列車推論エンジンの相違を考慮に入れた勾配マスキング戦略を採用している。
さらに、報酬ハッキング問題を排除するために、定理整合性と合法性検出機構も組み込んだ。
我々のLongCat-Flash-Proverは、自己形式化と定理証明の両方において、オープンウェイトモデルのための新しい最先端を設定できることを示す。
顕著なサンプル効率を示すため、MiniF2F-Testでは72の推論予算で97.1%のパスレートを達成した。
より困難なベンチマークでは、ProverBenchの70.8%とPutnamBenchの41.5%を解決し、既存のオープンウェイトベースラインを大幅に上回っている。
関連論文リスト
- VibeThinker-3B: Exploring the Frontier of Verifiable Reasoning in Small Language Models [10.513021831152363]
本稿では、3Bパラメータを持つコンパクトな密度モデルVibeThinker-3Bについて紹介する。
VibeThinker-3Bは高要求の検証タスクにおいてフロンティアレベルの性能を実現する。
論文 参考訳（メタデータ） (2026-06-15T02:57:19Z) - Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation [27.324913853284404]
Pythagoras-Prover(ピタゴラス・プロバー)は、実用的な計算予算のために開発された、リーンの定理プローバーの計算効率のよいファミリーである。
学習効率を向上させるために、カリキュラムSFTの簡単で中堅な問題に階層化されたリーン検証コーパスを構築します。
Augmented Lean Formalisation (ALF)も導入しています。
論文 参考訳（メタデータ） (2026-06-10T18:43:11Z) - LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - Training LLMs for Divide-and-Conquer Reasoning Elevates Test-Time Scalability [129.1296673737603]
大規模言語モデル(LLM)は、ステップ・バイ・ステップ・チェーン・オブ・シークレット(CoT)推論を通じて強力な推論能力を示している。
潜在的には、解のより効率的な探索を容易にするために複雑な問題をサブプロブレムに分解するDAC推論がある。
本稿では,DAC型推論能力を高めるために,エンドツーエンド強化学習(RL)フレームワークを提案する。
論文 参考訳（メタデータ） (2026-02-02T18:54:54Z) - Structured Uncertainty guided Clarification for LLM Agents [126.26213027785813]
LLMエージェントは、ツールコール機能を備えた大きな言語モデルを拡張するが、曖昧なユーザ命令は、しばしば誤った呼び出しやタスクの失敗につながる。
本稿では,ツールコールパラメータに対する構造的不確かさの定式化,完全情報の期待値(EVPI)を目標としたPOMDPのモデル化,冗長性防止のためのアスペクトベースコストモデルを提案する。
我々のSAGE-Agentは、この構造化された不確実性を活用し、より優れた効率を達成するために、曖昧なタスクのカバレッジを7～39%増加させ、明確な質問を1.5～2.7$times$に減らした。
論文 参考訳（メタデータ） (2025-11-11T21:50:44Z) - Introducing LongCat-Flash-Thinking: A Technical Report [116.75498493511026]
LongCat-Flash-ThinkingはオープンソースのMixture-of-Experts (MoE)推論モデルである。
高度な能力は、巧妙に製作された訓練プロセスを通じて育成される。
LongCat-Flash-Thinkingは、複雑な推論タスクのスイート上で、オープンソースモデル間の最先端のパフォーマンスを達成する。
論文 参考訳（メタデータ） (2025-09-23T10:25:48Z) - Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving [48.22540519786074]
最近の研究では、非公式な精度は80%を超え、公式な成功はPutnamBenchのようなベンチマークで8%以下である。
低レベルの証明生成から高レベルの推論を分離する新しいフレームワークを提案する。
提案手法は,2000年以降のIMO問題に対して,従来のオープンソース証明者が未報告の課題として評価した。
論文 参考訳（メタデータ） (2025-07-07T22:38:49Z) - Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs [11.87831709160905]
本稿では,自動定理証明のためのAIエージェントであるProver Agentを紹介する。
大規模な言語モデル(LLM)と公式な証明アシスタントであるLeanを統合している。
MiniF2Fベンチマークで88.1%の成功率を達成した。
論文 参考訳（メタデータ） (2025-06-24T18:01:52Z) - Theorem Prover as a Judge for Synthetic Data Generation [22.124954482278536]
RLHF(Reinforcement Learning from Human Feedback)において、人間のアノテーションを定理証明に置き換える枠組みを提案する。
複数の大規模言語モデル(LLM)でTP-as-a-JudgeとRFを適用し、ベンチマークをわずか3,508サンプルで改善し、MultiArithmのMistral-7Bで5.56%の精度を達成した。
論文 参考訳（メタデータ） (2025-02-18T18:57:09Z) - Chain of Evidences and Evidence to Generate: Prompting for Context Grounded and Retrieval Augmented Reasoning [3.117335706912261]
チェイン・オブ・エビデンス(CoE)とエビデンス・トゥ・ジェネレーション(E2G)は2つのユニークな戦略に基づいて構築されている。
根拠のない推論の主張の代わりに、我々の革新的なアプローチは「意思決定の証拠」の力を利用する。
我々のフレームワークは、様々な知識集約的推論および生成タスクにおいて、常に顕著な結果を達成する。
論文 参考訳（メタデータ） (2024-01-11T09:49:15Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。