Fugu-MT 論文翻訳(概要): Choir: An Open Protocol for Distributed Multi-Agent Autoformalization

論文の概要: Choir: An Open Protocol for Distributed Multi-Agent Autoformalization

arxiv url: http://arxiv.org/abs/2609.31903v1
Date: Fri, 25 Sep 2026 18:44:53 GMT
ステータス: 翻訳完了
システム内更新日: 2026-10-08 04:47:37.0608
Title: Choir: An Open Protocol for Distributed Multi-Agent Autoformalization
Title（参考訳）: Choir: 分散マルチエージェント自動フォーマットのためのオープンプロトコル
Abstract要約: Choirは分散形式化のためのオープンプロトコルである。プロジェクトを独立したコントリビュータによって完了可能なタスクに分解する。 ChoirはLean 4、Isabelle、Rocqをサポートし、オープンソースでモジュール化されている。
参考スコア（独自算出の注目度）: 6.345340156849189
License: http://creativecommons.org/licenses/by/4.0/
Abstract: AI agents can now formalize entire textbooks and major theorems in proof assistants such as Lean, but current efforts are typically centralized: a single team runs all agents and bears the full computational cost. We introduce Choir, an open protocol for distributed formalization. Choir decomposes a project into tasks that can be completed by independent contributors, each running their own agent with their own LLM subscription, while coordinating entirely through the project's GitHub repository. To support open participation, every contribution is checked by a deterministic gate before merge. Choir supports Lean 4, Isabelle, and Rocq, and is open source and modular, allowing projects to replace individual components or extend the protocol.
Abstract（参考訳）: AIエージェントは、Leanのような証明アシスタントで、教科書全体と主要な定理をフォーマルにすることができるが、現在の取り組みは通常、中央集権化されている。分散形式化のためのオープンプロトコルであるChoirを紹介する。 Choirはプロジェクトを独立したコントリビュータによって完了可能なタスクに分解し、それぞれが独自のLLMサブスクリプションで独自のエージェントを実行し、プロジェクトのGitHubリポジトリを通じて完全にコーディネートする。オープンな参加をサポートするために、すべてのコントリビューションはマージ前に決定論的ゲートによってチェックされる。 ChoirはLean 4、Isabelle、Rocqをサポートし、オープンソースでモジュール化されており、プロジェクトは個々のコンポーネントを置き換えるか、プロトコルを拡張することができる。

関連論文リスト

MARC v1: An Open-Source Multi-Agent Framework for Clinical AI Reasoning and Coordination [2.3475925378848124]
MARCは、抽出、推論、回答生成、評価のための役割特定エージェントをコーディネートする。 Decomposerモジュールは、プレーン言語記述からタスク固有のエージェントプロンプトを生成する。 MARCは、プログラミングの専門知識なしに、モデルに依存しず、解釈可能で、臨床領域の専門家にアクセスできるように設計されている。
論文参考訳（メタデータ） (2026-08-13T17:00:08Z)
Toward an Organizational Science of Multi-Agent LLM Systems: Decoupling Who, How, and Which Algorithm [14.162774819793759]
IMACSは、チームにいる人、メンバーがどのように整列し、どのアルゴリズムが作業を混乱させるかという、論理的に異なる3つの懸念を分離する。我々は、この分離を利用して、協調プロトコルが固定されている間、組織的な課題が異なる制御された比較を行う。また、プロトコルの選択を学習可能な変数に変換する。
論文参考訳（メタデータ） (2026-07-28T08:35:21Z)
Tencent WorkBuddy Bench: A Multi-Domain Coding-Agent Benchmark with Contamination-Resistant Task Construction [57.138342889101345]
Tencent WorkBuddy Benchは、コーディングエージェントのためのマルチドメイン評価スイートである。本報告では, 設計手法, スコアリングプロトコル, クロスモデルリーダーボードについて述べる。
論文参考訳（メタデータ） (2026-07-23T04:34:06Z)
Securing the AI Agent: A Unified Framework for Multi-Layer Agent Red Teaming [15.069910056925492]
AI-Infra-Guardは、単一の観察を取り巻くAIレッドチームを組織する、オープンソースのフレームワークです。我々はAI-Infra-Guardをオープンソースとしてリリースし、エージェントセキュリティの実践的な基盤として、Emphlayer-paradigmマッチングを実現する。
論文参考訳（メタデータ） (2026-06-30T07:06:56Z)
Orchestra-o1: Omnimodal Agent Orchestration [72.34907006336108]
Orchestra-o1は、複数のモダリティをまたいだ効率的なエージェントコラボレーションをサポートするように設計された、オムニモーダルなエージェントオーケストレーションフレームワークである。本研究は,モダリティを意識したタスクの分解,オンラインサブエージェントの特殊化,並列サブタスク実行を可能にする統一的なオーケストレーション機構を導入する。このスケーラブルな設計により、エージェントシステムは異種情報ソースを含む複雑な現実世界のタスクに効果的に取り組むことができ、OmniGAIAベンチマークの精度は10.3%向上した。
論文参考訳（メタデータ） (2026-06-10T04:50:35Z)
Benchmarking Open-Ended Multi-Agent Coordination in Language Agents [48.1363632826625]
Alemは、手続き的に生成されたコーディネーションタスク、ソフトな特殊化、コミュニケーション、制御可能なコーディネーションの難しさを、長い水平サバイバルの世界に埋め込む。 Craftaxライクなダイナミックス上に構築されたオープンなマルチエージェント協調のためのJAXベースのベンチマークである$alem$を紹介します。
論文参考訳（メタデータ） (2026-06-06T21:13:43Z)
Improving the Efficiency of Language Agent Teams with Adaptive Task Graphs [52.26652574704317]
大規模言語モデル(LLM)はますますチームにデプロイされているが、既存のコーディネーションアプローチは2つの極端な部分を占めることが多い。本稿では,Language Agent Teams for Task Evolution (LATTE)を紹介した。
論文参考訳（メタデータ） (2026-05-07T14:19:17Z)
Effective Strategies for Asynchronous Software Engineering Agents [52.76455094324273]
本稿では,集中型タスクデリゲート,非同期実行,独立したワークスペースという,3つのSWEプリミティブに根ざした構造化マルチエージェント協調パラダイムを導入する。 CAIDは,紙再生タスク(PaperBench)では26.7%,Pythonライブラリ開発タスクでは14.3%,単一エージェントベースラインでは26.7%の精度向上を実現している。
論文参考訳（メタデータ） (2026-03-23T02:26:35Z)
A distributed and parallel $(k, n)$ QSS scheme with verification capability [0.0]
本稿では、$(k, n )$の量子秘密共有方式を導入し、検証能力を付与する。新しいプロトコルの主な特徴は、完全に分散したセットアップで完全に並列に動作する能力にある。
論文参考訳（メタデータ） (2024-10-24T11:12:38Z)
Multi-Agent Collaboration via Cross-Team Orchestration [31.506350304184526]
大規模言語モデル(LLM)は、特に組織化された自律エージェントを通じて、様々なドメインに大きな影響を与えている。これはスケーラブルなマルチチームフレームワークで、オーケストレーションされたチームはさまざまなタスク指向のソリューションを共同で提案できる。実験では、最先端のベースラインと比較して、ソフトウェアの品質が顕著に向上している。
論文参考訳（メタデータ） (2024-06-13T10:18:36Z)
Multi-agent Deep Covering Skill Discovery [50.812414209206054]
本稿では,複数エージェントの結合状態空間の予測被覆時間を最小化し,マルチエージェントオプションを構築するマルチエージェントDeep Covering Option Discoveryを提案する。また、MARLプロセスにマルチエージェントオプションを採用するための新しいフレームワークを提案する。提案アルゴリズムは,アテンション機構とエージェントの相互作用を効果的に把握し,マルチエージェントオプションの同定に成功した。
論文参考訳（メタデータ） (2022-10-07T00:40:59Z)

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