論文の概要: Numina Fuse: Interactive Autoformalization in Lean 4

• arxiv url: http://arxiv.org/abs/2610.33860v1
• Date: Sat, 24 Oct 2026 19:05:32 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-27 22:27:13.465775
• Title: Numina Fuse: Interactive Autoformalization in Lean 4
• Title（参考訳）: Numina Fuse: リーン4におけるインタラクティブな自動形式化
• Abstract要約: Numina Fuseは、Lean 4で数学を形式化するエージェントネイティブアプリケーションである。 ユーザは、リーンプロジェクトでAIオーケストレータと作業し、青写真、依存性グラフ、リーンコードのビューを通じてそれを監視します。 バックエンドはプロジェクトの派生状態を保持し、ユーザがいない状態で何時間もエージェントを実行します。
• 参考スコア（独自算出の注目度）: 5.541135564754761
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Numina Fuse is an agent-native application for formalizing mathematics in Lean 4. Since Lean can compile while not representing its intended informal meaning, and agents now write Lean faster than people can read it, we built Fuse around human supervision of agent work. A user works with an AI orchestrator on a Lean project and supervises it through views of the blueprint, the dependency graph, and the Lean code, while the backend keeps the project's derived state and runs agents for hours without the user present. We describe the development of Fuse throughout 2026, as it moved from a prescribed pipeline of agents paced by human review to an orchestrator that dispatches specialists, provers, and parallel children on its own. We designed for this shift, keeping project state, tooling, and interface design separate from orchestration so that agents could take over more of the work as models improved. We report Fuse's use in a formalization of the three-dimensional Kakeya conjecture and a study of prover models. We close with lessons for the next generation of autoformalization systems. Fuse Desktop, an open-source local version, is available at https://github.com/project-numina/fuse-desktop.
• Abstract（参考訳）: Numina Fuseは、Lean 4で数学を形式化するエージェントネイティブアプリケーションである。 リーンは意図した非公式な意味を表わさずにコンパイルできるため、エージェントはより早くリーンを書けるようになった。 ユーザは、リーンプロジェクトでAIオーケストレータと作業し、ブループリント、依存性グラフ、リーンコードのビューを通じてそれを監視します。 我々は2026年を通して、Fuseの開発について述べる。それは、人間のレビューによってペーストされた所定のエージェントのパイプラインから、専門家、プローバー、並列した子供たちを単独で派遣するオーケストレータへと移行した。 私たちはこのシフトのために設計し、プロジェクト状態、ツーリング、インターフェース設計をオーケストレーションから切り離して、モデルの改善に伴ってエージェントがより多くの作業を引き継ぐようにしました。 フーズが3次元カキーア予想の形式化や証明モデルの研究に用いていることを報告する。 われわれは次世代のオートフォーマル化システムについて学ぶ。 Fuse Desktopはオープンソースのローカルバージョンで、https://github.com/project-numina/fuse-desktop.comから入手できる。

関連論文リスト

• Librarian Agents: Training LLMs to Curate Long-Context Workspaces that Anticipate Future Queries [61.486885079210055]
  構築者エージェントが生文書を階層的な合成ファイルと参照リンクに変換するフレームワークであるLibrarian Agentsを導入し、下流の応答エージェントに適したワークスペースを形成する。 経験的に、ライブラリアンエージェントはBrowseComp-Plusで最強の検索と事前計算のベースラインを33ポイント上回り、繰り返しクエリで事前構築コストを償却し、31ポイント平均精度の改善でBRIGHT上の未確認領域にゼロショットを一般化する。
  論文  参考訳（メタデータ） (2026-10-15T17:35:17Z)
• L3M: A Verifiable Harness and Runtime for Self-Extending and Self-Improving Agents [4.31785433770184]
  L3Mは、ある言語がハーネスを実装し、不変性を記述するという前提で構築されたランタイムであり、言語エージェントがそれを拡張している。 1つの計算は人間、エージェント、モデル、コードにまたがる。 ターミナルベンチでは、未調整のL3Mが安全ツールのみを使用してシェル装備のパスレートの約3分の2に達する。
  論文  参考訳（メタデータ） (2026-10-14T05:03:06Z)
• Driving Epidemic Models with AI Agents: the Epydemix Agent Framework [43.590506976483795]
  我々はEpydemix Agent Frameworkを紹介した。Epydemixはオープンソースのコンパートメンタル流行モデリング用Pythonライブラリである。 呼吸器感染症に対するワクチン接種戦略の比較を事例として,エンド・ツー・エンドのワークフローについて紹介する。 フレームワークのエージェント使用とPythonインターフェースの直接使用を比較して,50のエージェントセッションと5つのモデリングタスクでフレームワークを評価した。
  論文  参考訳（メタデータ） (2026-09-23T18:31:43Z)
• SciForge: An AI-Native, Multimodal Workbench for Scientific Discovery [48.99744520105086]
  SciForgeはマルチモーダルな研究ネイティブAIワークベンチである。 検索、解析、モデルルーティング、ワークフローの実行、プロット、書き込み、プレゼンテーション生成がモジュラーエージェントアクセス可能なサービスとして実行される間、人間の判断のためにグラフィカルインターフェースを予約する。
  論文  参考訳（メタデータ） (2026-07-17T15:13:03Z)
• Multi-agent Autoformalization of Tensor Network Theory [0.21847754147782886]
  我々は、専門的な大規模言語モデルエージェントのチームを構築し、理論物理学における研究レベルの形式化のためのエージェント駆動ワークフローを提示する。 エージェントは、構造化された数学的青写真と定期的な人間のレビューを通して調整し、完全な形式化を自律的にオーケストレーションし実行した。 いくつかの声明では、エージェントは標準的な文献には含まれない新しい証明ルートを探索することができた。
  論文  参考訳（メタデータ） (2026-07-08T18:43:33Z)
• The Evolution of Tool Use in LLM Agents: From Single-Tool Call to Multi-Tool Orchestration [58.61149924275458]
  ツールの使用により、大きな言語モデルが外部情報にアクセスし、ソフトウェアシステムを実行し、モデルパラメータだけで解決できるもの以外のデジタル環境で動作することができる。 エージェントシステムが進化するにつれて、中央の問題は、中途半端な状態、実行フィードバック、環境の変化、安全性、コスト、検証可能性といった実践的な制約によって、孤立呼び出しからマルチツールオーケストレーションへと移行した。 推論時の計画と実行、トレーニングと軌道構築、安全と制御、リソース制約下での効率性、オープン環境における能力の完全性、およびベンチマーク設計と評価の6つの分野に関する文献を整理する。
  論文  参考訳（メタデータ） (2026-03-24T07:05:05Z)
• Agents: An Open-source Framework for Autonomous Language Agents [98.91085725608917]
  我々は、言語エージェントを人工知能への有望な方向と見なしている。 Agentsはオープンソースライブラリで、これらの進歩を広く非専門的な聴衆に開放することを目的としています。
  論文  参考訳（メタデータ） (2023-09-14T17:18:25Z)

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

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