論文の概要: Do Theorem Provers Need Theorem-Proving Agents? mini-Lean-agent: A Coding-Agent Baseline for Lean

• arxiv url: http://arxiv.org/abs/2610.17331v1
• Date: Mon, 12 Oct 2026 19:40:30 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-15 21:06:15.446834
• Title: Do Theorem Provers Need Theorem-Proving Agents? mini-Lean-agent: A Coding-Agent Baseline for Lean
• Title（参考訳）: Theorem Provers は Theorem-Proving Agents を必要とするか? mini-Lean-Adnt: リーンのためのコーディング-エージェントベースライン
• Abstract要約: 汎用コーディングエージェントは標準シェルとファイルインタラクションを使用する。 形式的定理証明エージェントは、しばしば特殊でアドホックなツールに依存している。 リーンタスクの最小限のエージェントであるmini-Lean-agentを紹介します。
• 参考スコア（独自算出の注目度）: 24.67132297243691
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: General-purpose coding agents use standard shell and file interactions, yet formal theorem-proving agents often rely on specialized, ad-hoc tooling. This makes it difficult to determine which components of theorem-proving agents provide benchmark gains: an improved base model, a specialized harness, a specific tool, or a combination of any of them. We introduce mini-Lean-agent, a deliberately minimal agent for Lean tasks whose only model-visible tool is bash. The model must use bash to inspect and edit the repository, search local libraries, invoke Lean, and manage its own intermediate work, while a separate trusted evaluator verifies the final artifact. We compare mini-Lean-agent against AxProverBase and Numina-Lean-Agent on the Putnam 2025 benchmark. Experiments with Gemini 3.8 Flash as the base model show that mini-Lean-agent solves 7/12 problems at \$2 per problem limit, compared with AxProverBase's 4/12. With Astra as the base model, mini-Lean-agent solves 12/12 problems at an average cost of \$1.28 per problem. This suggests that a generic coding agent with a minimal harness can already achieve strong performance on Lean benchmarks. Our results motivate using mini-Lean-agent as a standard baseline when evaluating theorem-proving infrastructure.
• Abstract（参考訳）: 汎用符号化エージェントは標準シェルとファイルの相互作用を使用するが、形式的な定理証明エージェントは、しばしば特殊なアドホックツールに依存している。 これにより、どの要素がベンチマークゲイン(ベースモデルの改善、特別なハーネス、特定のツール、またはそれらの組み合わせ)を提供するかを決定するのが難しくなる。 モデルで見えるツールだけがbashであるリーンタスクの最小限のエージェントであるmini-Lean-agentを紹介します。 モデルはbashを使用してリポジトリを検査し、編集し、ローカルライブラリを検索し、Leanを呼び出し、独自の中間的な作業を管理する。 パットナム2025ベンチマークでは、AxProverBaseとNumina-Lean-Agentのミニリアンエージェントを比較した。 Gemini 3.8 Flash をベースモデルとして実験した結果,AxProverBase の 4/12 と比較すると,ミニLean-agent は 7/12 の問題を 1 あたり 2 ドルで解決している。 ベースモデルとしてAstraを用いると、ミニリアンエージェントは平均コストが1.28ドルである12/12の問題を解く。 これは、最小限のハーネスを持つ汎用的なコーディングエージェントが、リーンベンチマークですでに強力なパフォーマンスを達成することができることを示唆している。 本研究は,定理提示基盤の評価において,ミニリアンエージェントを標準ベースラインとして活用する動機付けを行った。

関連論文リスト

• AgentLens: Production-Assessed Trajectory Reviews for Coding Agent Evaluation [0.18567307896771823]
  AgentLensはインタラクティブなコードエージェントのための実運用評価ベンチマークである。 LLMで書かれた軌道レビューとサイド・バイ・サイド比較との形式的検証を組み合わせている。 モデル行動の診断、エージェントの連続したバージョンの比較、夜間評価パイプラインでの製品回帰の取得に使用しています。
  論文  参考訳（メタデータ） (2026-07-07T11:27:43Z)
• Terminus-4B: Can a Smaller Model Replace Frontier LLMs at Agentic Execution Tasks? [3.636948650519796]
  スモール言語モデル(SLM)はエージェント端末実行のタスクにおいてフロンティアモデルに匹敵する性能を達成できる。 教師付ファインタニング(SFT)と強化学習(RL)による訓練後Qwen3-4BモデルであるTerminus-4Bを提案する。 Terminus-4Bは、No Subagentベースラインと比較して、メインエージェントのトークン使用量を最大30%削減できることがわかった。
  論文  参考訳（メタデータ） (2026-05-04T22:24:24Z)
• ISO-Bench: Can Coding Agents Optimize Real-World Inference Workloads? [0.8749675983608171]
  実世界の推論タスクでその能力をテストするためのコーディングエージェントのベンチマークであるISO-Benchを紹介する。 統合プルリクエストから54のタスクをキュレートし、測定可能なパフォーマンスを改善しました。
  論文  参考訳（メタデータ） (2026-02-23T08:37:53Z)
• Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics [25.762535169301984]
  我々はClude CodeとNumina-Lean-MCPを組み合わせたNumina-Lean-Agentを導入し、リーンとの自律的なインタラクションを可能にします。 Claude Opus 4.5 をベースモデルとして、Numina-Lean-Agent はPutnam 2025 (12 / 12) の全ての問題を解決する。
  論文  参考訳（メタデータ） (2026-01-20T14:51:45Z)
• The Bitter Lesson of Diffusion Language Models for Agentic Workflows: A Comprehensive Reality Check [54.08619694620588]
  本稿では,2つの異なるエージェントパラダイムであるEmbodied AgentsとTool-Calling AgentsにまたがるdLLMの包括的評価を行う。 Agentboard と BFCL では,現在の dLLM が信頼できるエージェントバックボーンとして機能しないという,"ビットレッスン" が報告されている。
  論文  参考訳（メタデータ） (2026-01-19T11:45:39Z)
• Holistic Agent Leaderboard: The Missing Infrastructure for AI Agent Evaluation [87.47155146067962]
  数百のタスクで並列評価をオーケストレーションする,標準化された評価ハーネスを提供する。 モデル、足場、ベンチマークにまたがる3次元解析を行う。 私たちの分析では、ほとんどのランで精度を低下させる高い推論努力など、驚くべき洞察が示されています。
  論文  参考訳（メタデータ） (2025-10-13T22:22:28Z)
• GSM-Agent: Understanding Agentic Reasoning Using Controllable Environments [56.007498767771075]
  GSM-Agentは複雑な環境でエージェント推論を評価するための新しいベンチマークである。 我々は,環境文書の埋め込みをノードにクラスタ化することでエージェント推論パターンを分析し,各ツールコールを最も近いノードにマッピングする。 本稿では,LLMのエージェント推論性能を向上させるためのツール拡張テストタイムスケーリング手法を提案する。
  論文  参考訳（メタデータ） (2025-09-26T07:24:37Z)
• 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)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。