論文の概要: Awakening the Sleeping Agent: Lean-Specific Agentic Data Reactivates General Tool Use in Goedel Prover

• arxiv url: http://arxiv.org/abs/2604.08388v1
• Date: Thu, 09 Apr 2026 15:47:29 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-10 18:34:06.007023
• Title: Awakening the Sleeping Agent: Lean-Specific Agentic Data Reactivates General Tool Use in Goedel Prover
• Title（参考訳）: 睡眠エージェントの覚醒: リーン特有なエージェントデータによってGoedel Proverで一般的なツールが利用できるようになる
• Authors: Jui-Hui Chung, Hongzhou Lin, Lai Jiang, Shange Tang, Chi Jin,
• Abstract要約: Goedel-Prover-V2 を用いて形式数学の現象を研究する。 ドメインの特殊化の後、モデルは有効なツールコールを生成する能力がほとんど完全に失われます。 少数のリーン固有のツール使用データに基づいて、専門的なモデルを微調整します。
• 参考スコア（独自算出の注目度）: 22.224622637829096
• License: http://creativecommons.org/publicdomain/zero/1.0/
• Abstract: Heavy supervised fine-tuning on a target domain can strongly suppress capabilities that were present in the base model. We study this phenomenon in formal mathematics using Goedel-Prover-V2, an open-source model heavily trained on 1.8 million formal-math examples. After domain specialization, the model almost completely loses its ability to produce valid tool calls, even when explicitly instructed to use tools, dropping from 89.4% function-calling accuracy in the base model to nearly 0%. We ask whether this agentic collapse is permanent or instead reversible. To answer this question, we fine-tune the specialized model on a small amount of Lean-specific tool-use data. Remarkably, as few as 100 agentic traces are sufficient to restore strong tool-calling behavior. Importantly, this recovery is not the result of reward hacking or benchmark-specific optimization: the recovery data is entirely drawn from the Lean setting, where the model uses natural-language queries to search the Mathlib library for relevant theorems and lemmas, yet the regained capability transfers well beyond that domain. In particular, these same 100 Lean-specific traces improve performance on the Berkeley Function Calling Leaderboard from near zero to 83.8%, approaching the base model's 89.4% despite the mismatch in task distribution and protocol. The recovered capability is also practically useful in-domain. On ProofNet, pass@32 improves from 21.51% to 25.81%. Together, these results show that heavy domain supervised fine-tuning can suppress general tool-use ability without permanently erasing it, and that a small amount of domain-specific agentic data can awaken dormant tool-use capabilities.
• Abstract（参考訳）: ターゲット領域における重教師付き微調整は、ベースモデルに存在する能力を強く抑制することができる。 Goedel-Prover-V2というオープンソースモデルを用いて、この現象を形式数学において研究する。 ドメインの特殊化後、このモデルはツールの使用を明示的に指示されたとしても、有効なツールコールを生成する能力がほぼ完全に失われ、ベースモデルの89.4%の関数呼び出し精度は0%に低下した。 このエージェント的崩壊は恒久的なのか、それとも可逆なのかを問う。 この質問に答えるために、少数のリーン固有のツール使用データに基づいて、専門的なモデルを微調整します。 注目すべきは、強力なツール呼び出し動作を回復するのには、エージェントトレースが100にも満たないことだ。 このリカバリデータは、モデルが自然言語クエリを使用して、関連する定理や補題をMathlibライブラリで検索するLean設定から完全に引き出されたものです。 特に、これらの100のリーン固有のトレースは、タスクの配布とプロトコルのミスマッチにもかかわらず、ベースモデルの89.4%に近づき、バークレー関数呼び出しリーダーボードのパフォーマンスをほぼゼロから83.8%に改善した。 回復した能力はドメイン内で実用的に有用である。 ProofNetでは、pass@32は21.51%から25.81%に改善されている。 これらの結果から,重ドメインを監督する微調整は,恒常的に消去することなく汎用ツールの使用能力を抑えることができ,少数のドメイン固有のエージェントデータが休息用ツール使用能力を覚醒させる可能性が示唆された。

関連論文リスト

• A Rubric-Supervised Critic from Sparse Real-World Outcomes [87.11204512676193]
  現実のコーディングエージェントは、成功信号がノイズが多く、遅延し、スパースであるループで人間と動作します。 本稿では,RLに基づくトレーニングや推論時間スケーリングの報奨モデルとして,スパースとノイズの相互作用データから"批判的"モデルを学習するプロセスを提案する。
  論文  参考訳（メタデータ） (2026-03-04T07:23:54Z)
• Behavioral Analytics for Continuous Insider Threat Detection in Zero-Trust Architectures [0.0]
  このフレームワークでは、CERT Insider Threatデータセットをデータクリーニング、正規化、クラスバランスに使用しています。 また、次元減少のために主成分分析(PCA)も採用している。 SVM(90.1%)、ANN(94.7%)、ベイズネット(94.9)と比較して、AdaBoostは98.0%のACC、98.3%のPre、98.0%のREC、F1スコア(F1)で高いパフォーマンスを達成した。
  論文  参考訳（メタデータ） (2026-01-10T22:30:19Z)
• HarnessAgent: Scaling Automatic Fuzzing Harness Construction with Tool-Augmented LLM Pipelines [22.70950665226898]
  HarnessAgentはツール拡張されたエージェントフレームワークで、何百ものOSS-Fuzzターゲットに対して完全に自動化され、スケーラブルなハーネス構築を実現する。 OSS-Fuzzプロジェクトと178のC++プロジェクトから243のターゲット関数に対してHarnessAgentを評価する。
  論文  参考訳（メタデータ） (2025-12-03T03:55:09Z)
• GRETEL: A Goal-driven Retrieval and Execution-based Trial Framework for LLM Tool Selection Enhancing [6.790345342526922]
  GRETELは、サンドボックス化された計画実行評価サイクルを通じてセマンティックに検索された候補を処理するエージェントワークフローを実装している。 ToolBenchベンチマークに関する包括的な評価は、すべてのメトリクスで大幅に改善されていることを示しています。
  論文  参考訳（メタデータ） (2025-10-10T00:12:51Z)
• PALADIN: Self-Correcting Language Model Agents to Cure Tool-Failure Cases [2.3181214107210235]
  PALADINは、系統的な障害注入によって構築された5万以上のリカバリアノテーション付き軌道を走行する。 トレーニングでは、LoRAベースの微調整を使用して、回復能力を注入しながらベース能力を維持する。 このアプローチは、トレーニング分布を超えた新しい失敗に一般化する。
  論文  参考訳（メタデータ） (2025-09-25T10:37:30Z)
• How Can Input Reformulation Improve Tool Usage Accuracy in a Complex Dynamic Environment? A Study on $τ$-bench [58.114899897566964]
  マルチターンの会話環境では、大きな言語モデル(LLM)は、一貫性のある推論とドメイン固有のポリシーへの固執にしばしば苦労する。 本稿では,関連するドメインルールを付加したユーザクエリを自動的に再構成するIRMA(Input-Reformulation Multi-Agent)フレームワークを提案する。 IRMAはReAct、Function Calling、Self-Reflectionをそれぞれ16.1%、12.7%、19.1%で大きく上回っている。
  論文  参考訳（メタデータ） (2025-08-28T15:57:33Z)
• SMaRt: Improving GANs with Score Matching Regularity [114.43433222721025]
  生成的敵ネットワーク(GAN)は通常、基礎となる多様体が複雑である非常に多様なデータから学ぶのに苦労する。 スコアマッチングは、生成したデータポイントを実データ多様体へ持続的にプッシュする能力のおかげで、この問題に対する有望な解決策であることがわかった。 提案手法は, 実世界のデータセットにおいて, 近似スコア関数として機能する事前学習拡散モデルを用いて, 最先端のGANの性能を継続的に向上させることができることを示す。
  論文  参考訳（メタデータ） (2023-11-30T03:05:14Z)
• Tool-Augmented Reward Modeling [58.381678612409]
  本稿では,外部環境へのアクセスによるRMの強化により,制約に対処するツール拡張された嗜好モデリング手法であるThemisを提案する。 我々の研究は、外部ツールをRMに統合し、様々な外部ソースとの相互作用を可能にすることを目的としている。 人間の評価では、テミスで訓練されたRLHFはベースラインと比較して平均32%の勝利率を得る。
  論文  参考訳（メタデータ） (2023-10-02T09:47:40Z)

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

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