Fugu-MT 論文翻訳(概要): Can Proof Assistants Verify Multi-Agent Systems?

論文の概要: Can Proof Assistants Verify Multi-Agent Systems?

arxiv url: http://arxiv.org/abs/2503.06812v1
Date: Mon, 10 Mar 2025 00:24:29 GMT
ステータス: 翻訳完了
システム内更新日: 2025-03-11 15:45:39.984059
Title: Can Proof Assistants Verify Multi-Agent Systems?
Title（参考訳）: 証明アシスタントはマルチエージェントシステムを検証することができるか?
Authors: Julian Alfredo Mendez, Timotheus Kampik,
Abstract要約: Sodaは高レベルの関数型およびオブジェクト指向言語である。強く静的に型付けされた高レベルのプログラミング言語であるScalaだけでなく、リーンにも、コードのコンパイルをサポートする。
参考スコア（独自算出の注目度）: 0.0
License:
Abstract: This paper presents the Soda language for verifying multi-agent systems. Soda is a high-level functional and object-oriented language that supports the compilation of its code not only to Scala, a strongly statically typed high-level programming language, but also to Lean, a proof assistant and programming language. Given these capabilities, Soda can implement multi-agent systems, or parts thereof, that can then be integrated into a mainstream software ecosystem on the one hand and formally verified with state-of-the-art tools on the other hand. We provide a brief and informal introduction to Soda and the aforementioned interoperability capabilities, as well as a simple demonstration of how interaction protocols can be designed and verified with Soda. In the course of the demonstration, we highlight challenges with respect to real-world applicability.
Abstract（参考訳）: 本稿では,マルチエージェントシステムを検証するためのSoda言語について述べる。 Sodaは高レベルの関数型とオブジェクト指向の言語で、コードをScalaにコンパイルするだけでなく、静的に型付けされた高レベルの言語であるだけでなく、証明アシスタントでプログラミング言語のLeanにもサポートしています。これらの機能を考えると、Sodaはマルチエージェントシステム(あるいはその一部)を実装し、一方はメインストリームのソフトウェアエコシステムに統合し、他方では最先端のツールで正式に検証することができる。我々は、Sodaの簡潔かつ非公式な紹介と、前述の相互運用性機能、およびSodaによるインタラクションプロトコルの設計と検証の簡単なデモを提供する。デモでは,実世界の適用性に関する課題を強調した。

関連論文リスト

Bidirectional Emergent Language in Situated Environments [4.950411915351642]
マルチエージェントポンとコレクターの2つの新しい協調環境を紹介した。最適なパフォーマンスには通信プロトコルの出現が必要ですが、適度な成功はそれなしで達成できます。エージェントは意味のあるメッセージのみを生成し、調整なしでは成功できない状態の受信メッセージに作用する。
論文参考訳（メタデータ） (2024-08-26T21:25:44Z)
ClawMachine: Learning to Fetch Visual Tokens for Referential Comprehension [71.03445074045092]
我々はClawMachineを提案し、視覚トークンのグループのトークン集合を用いて各エンティティに明示的に通知する新しい方法論を提案する。追加構文を用いることなく視覚的参照タスクのプロンプトと応答を統一する手法を提案する。 ClawMachineは、高い効率でシーンレベルおよび参照理解タスクにおいて優れたパフォーマンスを達成する。
論文参考訳（メタデータ） (2024-06-17T08:39:16Z)
Code-Switched Language Identification is Harder Than You Think [69.63439391717691]
コードスイッチングは、文字と音声の通信において一般的な現象である。 CSコーパスの構築の応用について検討する。タスクをもっと多くの言語に拡張することで、タスクをより現実的にします。文レベルのマルチラベルタグ付け問題としてタスクを再構築し、より難易度の高いものにする。
論文参考訳（メタデータ） (2024-02-02T15:38:47Z)
A Systematic Study of Performance Disparities in Multilingual Task-Oriented Dialogue Systems [68.76102493999134]
マルチリンガルなタスク指向対話システム間に存在するタスクパフォーマンスの相違を,実証的に分析し,分析する。我々は現在のToDシステムにおける適応と本質的バイアスの存在を証明した。本稿では,新しい言語に対するToDデータ収集とシステム開発へのアプローチについて,実践的なヒントを提供する。
論文参考訳（メタデータ） (2023-10-19T16:41:44Z)
Document-Level Language Models for Machine Translation [37.106125892770315]
文書レベルのモノリンガルデータを利用した文脈対応翻訳システムを構築した。モデル組み合わせの最近の進歩を活用することで、既存のアプローチを改善します。ほとんどのシナリオでは、バックトランスレーションは、翻訳システムを再トレーニングするコストを犠牲にして、よりよい結果をもたらす。
論文参考訳（メタデータ） (2023-10-18T20:10:07Z)
LARCH: Large Language Model-based Automatic Readme Creation with Heuristics [9.820370420194948]
大規模言語モデル(LLM)は,リポジトリを表すコードフラグメントを識別できれば,一貫性のある,事実上正しい読み出しを生成することができることを示す。 LARCH (LLM-based Automatic Readme Creation with Heuristics) を開発した。 LARCHは、ほとんどのケースにおいて整合的で事実的に正しい読み出しを生成できることを示し、代表的なコード識別に依存しないベースラインよりも優れていることを示す。
論文参考訳（メタデータ） (2023-08-06T12:28:24Z)
ChatDev: Communicative Agents for Software Development [84.90400377131962]
ChatDevはチャットを利用したソフトウェア開発フレームワークで、特別なエージェントがコミュニケーション方法についてガイドされる。これらのエージェントは、統一された言語ベースのコミュニケーションを通じて、設計、コーディング、テストフェーズに積極的に貢献する。
論文参考訳（メタデータ） (2023-07-16T02:11:34Z)
Language Models as Zero-Shot Planners: Extracting Actionable Knowledge for Embodied Agents [111.33545170562337]
自然言語で表現された高レベルなタスクを、選択された実行可能なステップのセットに基底付ける可能性について検討する。事前学習したLMが十分に大きく、適切に誘導された場合、ハイレベルなタスクを効果的に低レベルな計画に分解できることがわかった。本稿では,既存の実演の条件を規定し,計画が許容可能な行動に意味的に変換される手順を提案する。
論文参考訳（メタデータ） (2022-01-18T18:59:45Z)
Call Larisa Ivanovna: Code-Switching Fools Multilingual NLU Models [1.827510863075184]
NLU(Multilingual natural Language understanding)の新たなベンチマークには、意図とスロットを付加した複数の言語での単言語文が含まれる。既存のベンチマークでは、文法構造が複雑であるため、収集やラベル付けが困難であるコードスイッチ付き発話が欠如している。我々の研究は、可塑性で自然な発声音声を生成するための認識された手法を採用し、それらを用いて合成コード発声テストセットを作成する。
論文参考訳（メタデータ） (2021-09-29T11:15:00Z)
Unsupervised Machine Translation On Dravidian Languages [13.404286929634614]
Unsupervised neural Machine Translation (UNMT) は、ドラヴィディア族のような低リソース言語にとって有益である。近年,補助並列データの利用が提案され,最先端の成果が得られた。
論文参考訳（メタデータ） (2021-03-29T18:33:53Z)
Learning Adaptive Language Interfaces through Decomposition [89.21937539950966]
本稿では,分解による新しいハイレベルな抽象化を学習するニューラルセマンティック解析システムを提案する。ユーザは、新しい振る舞いを記述する高レベルな発話を低レベルなステップに分解することで、対話的にシステムを教える。
論文参考訳（メタデータ） (2020-10-11T08:27:07Z)

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