論文の概要: Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
- arxiv url: http://arxiv.org/abs/2601.14027v1
- Date: Tue, 20 Jan 2026 14:51:45 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-01-21 22:47:23.359249
- Title: Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
- Title（参考訳）: Numina-Lean-Agent:形式数学のためのオープンで汎用的なエージェント推論システム
- Authors: Junqi Liu, Zihao Zhou, Zekai Zhu, Marco Dos Santos, Weikun He, Jiawei Liu, Ran Wang, Yunzhou Xie, Junqiao Zhao, Qiufeng Wang, Lihong Zhi, Jia Li, Wenda Li,
- Abstract要約: 我々はClude CodeとNumina-Lean-MCPを組み合わせたNumina-Lean-Agentを導入し、リーンとの自律的なインタラクションを可能にします。
Claude Opus 4.5 をベースモデルとして、Numina-Lean-Agent はPutnam 2025 (12 / 12) の全ての問題を解決する。
- 参考スコア（独自算出の注目度）: 25.762535169301984
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Agentic systems have recently become the dominant paradigm for formal theorem proving, achieving strong performance by coordinating multiple models and tools. However, existing approaches often rely on task-specific pipelines and trained formal provers, limiting their flexibility and reproducibility. In this paper, we propose the paradigm that directly uses a general coding agent as a formal math reasoner. This paradigm is motivated by (1) A general coding agent provides a natural interface for diverse reasoning tasks beyond proving, (2) Performance can be improved by simply replacing the underlying base model, without training, and (3) MCP enables flexible extension and autonomous calling of specialized tools, avoiding complex design. Based on this paradigm, we introduce Numina-Lean-Agent, which combines Claude Code with Numina-Lean-MCP to enable autonomous interaction with Lean, retrieval of relevant theorems, informal proving and auxiliary reasoning tools. Using Claude Opus 4.5 as the base model, Numina-Lean-Agent solves all problems in Putnam 2025 (12 / 12), matching the best closed-source system. Beyond benchmark evaluation, we further demonstrate its generality by interacting with mathematicians to successfully formalize the Brascamp-Lieb theorem. We release Numina-Lean-Agent and all solutions at https://github.com/project-numina/numina-lean-agent.
- Abstract（参考訳）: エージェントシステムは、最近、複数のモデルやツールをコーディネートすることで、強力な性能を達成するフォーマルな定理証明の主要なパラダイムとなっている。
しかし、既存のアプローチは、しばしばタスク固有のパイプラインと訓練されたフォーマルなプロバーに依存し、柔軟性と再現性を制限する。
本稿では,一般の符号化エージェントを公式な数学的推論器として直接使用するパラダイムを提案する。
このパラダイムは,(1)証明を超えた多様な推論タスクのための自然なインタフェースを提供する一般コーディングエージェント,(2)基礎となるベースモデルを置き換えることによるパフォーマンスの向上,(3)MPPは複雑な設計を避けることで,柔軟な拡張と自律的呼び出しを可能にする。
このパラダイムに基づいて、Clude CodeとNumina-Lean-MCPを組み合わせたNumina-Lean-Agentを導入し、リーンとの自律的なインタラクション、関連する定理の検索、非公式な証明、補助的な推論ツールを実現します。
Claude Opus 4.5 をベースモデルとして、Numina-Lean-Agent はPutnam 2025 (12 / 12) の全ての問題を解決する。
ベンチマーク評価以外にも、数学者と対話してBrascamp-Lieb定理の形式化を成功させることにより、その一般化をさらに実証する。
Numina-Lean-Agentと、https://github.com/project-numina/numina-lean-agent.comのすべてのソリューションをリリースします。
関連論文リスト
- Multimodal Reinforcement Learning with Agentic Verifier for AI Agents [131.46008226323423]
Argosは、エージェントタスクの推論モデルをトレーニングするための、原則化されたマルチモーダル報酬エージェントである。
エージェント検証をSFTデータとRLトレーニングの両方で活用することにより、我々のモデルは最先端の結果を得ることができる。
論文 参考訳（メタデータ） (2025-12-03T04:42:47Z) - Agent0: Unleashing Self-Evolving Agents from Zero Data via Tool-Integrated Reasoning [84.70211451226835]
大規模言語モデル(LLM)エージェントは、人間の計算データへの依存によって制約される。
我々は,外部データを持たない高性能エージェントを進化させる完全自律型フレームワークであるAgent0を紹介する。
Agent0は推論能力を大幅に向上させ、Qwen3-8B-Baseモデルを数学的推論で18%改善し、一般的な推論ベンチマークで24%改善した。
論文 参考訳（メタデータ） (2025-11-20T05:01:57Z) - Reducing Cognitive Overhead in Tool Use via Multi-Small-Agent Reinforcement Learning [1.974921946982281]
ツールの使用から推論を明示的に分離するフレームワークであるMSARLを提案する。
MSARLでは、Reasoning Agentが問題とツール呼び出しを分解し、複数のツールエージェントが特定の外部ツールを専門にしている。
コード実行による数学的問題解決において、MSARLは単一エージェントベースラインに対する推論安定性と最終回答精度を大幅に改善する。
論文 参考訳（メタデータ） (2025-08-12T12:10:53Z) - Chain-of-Agents: End-to-End Agent Foundation Models via Multi-Agent Distillation and Agentic RL [41.847359443133776]
CoA(Chain-of-Agents)は、大規模言語モデル(LLM)推論の新しいパラダイムであり、ネイティブなエンドツーエンドの複雑な問題解決を可能にする。
我々は, エージェント制御微調整のための多エージェント蒸留フレームワークを導入し, 最先端のマルチエージェントシステムをチェーン・オブ・エージェント・トラジェクトリに蒸留する。
次に、検証可能なエージェントタスクに対するエージェント強化学習を用いて、チェーン・オブ・エージェントの問題解決におけるモデルの能力をさらに向上する。
論文 参考訳（メタデータ） (2025-08-06T17:01:02Z) - Solving Formal Math Problems by Decomposition and Iterative Reflection [30.54275542622631]
textbfDelta Proverは汎用LLMとLean 4の実証環境とのインタラクションを編成します。
bftextDelta Proverは、miniF2F-testベンチマークで、最先端の95.9%の成功率を達成した。
論文 参考訳（メタデータ） (2025-07-21T03:56:35Z) - 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) - Distilling LLM Agent into Small Models with Retrieval and Code Tools [65.73762766854192]
Agent Distillationは、推論能力とタスク解決の振る舞いを大きな言語モデルから小さな言語モデルに移行するためのフレームワークである。
その結果,SLMは0.5B,1.5B,3Bのパラメータで,次世代の1.5B,3B,7Bモデルと競合する性能が得られることがわかった。
論文 参考訳（メタデータ） (2025-05-23T08:20:15Z) - LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。
LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。
これは23のリーンリポジトリにわたる155の定理の正式な証明を生成する。
論文 参考訳（メタデータ） (2024-10-08T17:11:24Z) - Pangu-Agent: A Fine-Tunable Generalist Agent with Structured Reasoning [50.47568731994238]
人工知能(AI)エージェント作成の鍵となる方法は強化学習(RL)である
本稿では,構造化推論をAIエージェントのポリシーに統合し,学習するための一般的なフレームワークモデルを提案する。
論文 参考訳（メタデータ） (2023-12-22T17:57:57Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。