論文の概要: SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems
- arxiv url: http://arxiv.org/abs/2509.23130v2
- Date: Tue, 30 Sep 2025 07:31:57 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-10-01 12:20:10.389814
- Title: SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems
- Title（参考訳）: SysMoBench: 複雑な実世界のシステムを形式的にモデル化するAIの評価
- Authors: Qian Cheng, Ruize Tang, Emilie Ma, Finn Hackett, Peiyang He, Yiming Su, Ivan Beschastnikh, Yu Huang, Xiaoxing Ma, Tianyin Xu,
- Abstract要約: 我々は、AIが大規模で複雑なシステムを正式にモデル化する能力を評価するベンチマークであるSysMoBenchを紹介する。
私たちは、今日の重要なコンピューティングインフラストラクチャのキーストーンである、並列および分散システムに重点を置いています。
- 参考スコア（独自算出の注目度）: 12.181911851729614
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formal models are essential to specifying large, complex computer systems and verifying their correctness, but are notoriously expensive to write and maintain. Recent advances in generative AI show promise in generating certain forms of specifications. However, existing work mostly targets small code, not complete systems. It is unclear whether AI can deal with realistic system artifacts, as this requires abstracting their complex behavioral properties into formal models. We present SysMoBench, a benchmark that evaluates AI's ability to formally model large, complex systems. We focus on concurrent and distributed systems, which are keystones of today's critical computing infrastructures, encompassing operating systems and cloud infrastructure. We use TLA+, the de facto specification language for concurrent and distributed systems, though the benchmark can be extended to other specification languages. We address the primary challenge of evaluating AI-generated models by automating metrics like syntactic and runtime correctness, conformance to system code, and invariant correctness. SysMoBench currently includes nine diverse system artifacts: the Raft implementation of Etcd and Redis, the Spinlock and Mutex in Asterinas OS, etc.; more artifacts are being actively added. SysMoBench enables us to understand the capabilities and limitations of today's LLMs and agents, putting tools in this area on a firm footing and opening up promising new research directions.
- Abstract（参考訳）: 形式モデルは、大規模で複雑なコンピュータシステムを特定し、その正しさを検証するのに不可欠であるが、書き込みやメンテナンスに費用がかかることで有名である。
生成AIの最近の進歩は、特定の形態の仕様を生成することを約束している。
しかし、既存の作業は主に、完全なシステムではなく、小さなコードをターゲットにしています。
複雑な振る舞い特性を形式モデルに抽象化する必要があるため、AIが現実的なシステムアーティファクトに対処できるかどうかは不明だ。
我々は、AIが大規模で複雑なシステムを正式にモデル化する能力を評価するベンチマークであるSysMoBenchを紹介する。
私たちは、オペレーティングシステムやクラウドインフラストラクチャを含む今日の重要なコンピューティングインフラストラクチャのキーストーンである、並列および分散システムに重点を置いています。
並列および分散システムのためのデファクト仕様言語であるTLA+を使っていますが、ベンチマークは他の仕様言語にも拡張できます。
シンタクティックとランタイムの正しさ、システムコードへの準拠、不変の正しさといったメトリクスを自動化することで、AI生成モデルを評価する上での最大の課題に対処する。
SysMoBenchは現在、EtcdとRedisのRaft実装、Asterinas OSのSpinlockとMutexなど、9つの多様なシステムアーティファクトを含んでいる。
さらに多くのアーティファクトが追加されている。
SysMoBenchは、今日のLLMとエージェントの能力と限界を理解し、この領域にツールをしっかりと配置し、将来有望な新しい研究方向を開くことができます。
関連論文リスト
- Embodied AI: From LLMs to World Models [65.68972714346909]
人工知能(AI)は、人工知能(AGI)を実現するためのインテリジェントシステムパラダイムである。
近年のLarge Language Models(LLMs)とWorld Models(WMs)のブレークスルーは、AIを具現化する上で大きな注目を集めている。
論文 参考訳（メタデータ） (2025-09-24T11:37:48Z) - Is the `Agent' Paradigm a Limiting Framework for Next-Generation Intelligent Systems? [0.0]
エージェント」の概念は人工知能(AI)の研究を深く形作っている。
本稿では,エージェント中心パラダイムの必要性と最適性を再評価する。
論文 参考訳（メタデータ） (2025-09-13T16:11:27Z) - Reasoning Language Models: A Blueprint [16.04440875855868]
推論言語モデル(RLM)は、AIの問題解決能力を再定義した。
しかし、それらの高コスト、プロプライエタリな性質、複雑なアーキテクチャは、アクセシビリティとスケーラビリティの課題を提示している。
本稿では、RLMコンポーネントをモジュール化フレームワークにまとめる包括的青写真を提案する。
論文 参考訳（メタデータ） (2025-01-20T02:16:19Z) - Fundamental Risks in the Current Deployment of General-Purpose AI Models: What Have We (Not) Learnt From Cybersecurity? [60.629883024152576]
大規模言語モデル(LLM)は、幅広いユースケースで急速にデプロイされている。
OpenAIs Alteraは、自律性の向上、データアクセス、実行機能の一例に過ぎない。
これらの方法には、さまざまなサイバーセキュリティ上の課題が伴う。
論文 参考訳（メタデータ） (2024-12-19T14:44:41Z) - Large Action Models: From Inception to Implementation [51.81485642442344]
大規模アクションモデル(LAM)は動的環境内でのアクション生成と実行のために設計されている。
LAMは、AIを受動的言語理解からアクティブなタスク完了に変換する可能性を秘めている。
創発から展開まで,LAMを体系的に開発するための総合的なフレームワークを提案する。
論文 参考訳（メタデータ） (2024-12-13T11:19:56Z) - Specifications: The missing link to making the development of LLM systems an engineering discipline [65.10077876035417]
我々は、構造化出力、プロセスの監督、テストタイム計算など、これまでの分野の進歩について論じる。
モジュール型かつ信頼性の高いLCMシステムの開発に向けた研究の今後の方向性について概説する。
論文 参考訳（メタデータ） (2024-11-25T07:48:31Z) - Towards Single-System Illusion in Software-Defined Vehicles -- Automated, AI-Powered Workflow [3.2821049498759094]
本稿では,車載ソフトウェアシステムの開発における,新しいモデルと特徴に基づくアプローチを提案する。
提案されたアプローチの重要なポイントの1つは、近代的な生成AI、特にLarge Language Models(LLM)の導入である。
その結果、パイプラインは広範囲に自動化され、各ステップでフィードバックが生成される。
論文 参考訳（メタデータ） (2024-03-21T15:07:57Z) - TaskMatrix.AI: Completing Tasks by Connecting Foundation Models with
Millions of APIs [71.7495056818522]
私たちは、基礎モデルと数百万のAPIを結合してタスク補完を行う、新しいAIエコシステムとしてTaskMatrix.AIを紹介します。
このようなエコシステムを構築するためのビジョンを示し、それぞれの重要なコンポーネントを説明し、このビジョンの実現可能性と次に取り組むべき主な課題の両方を説明するために研究ケースを使用します。
論文 参考訳（メタデータ） (2023-03-29T03:30:38Z) - Machine Learning Systems: A Survey from a Data-Oriented Perspective [6.933671804969495]
データ指向アーキテクチャ(DOA、Data-oriented Architecture)は、MLモデルを統合する上で、システムにより良いものを提供する新しいスタイルである。
本稿では、MLベースのシステムの実装とデプロイに実践者がDOAを採用した理由、方法、そしてその程度について調査する。
論文 参考訳（メタデータ） (2023-02-09T17:57:02Z) - MRKL Systems: A modular, neuro-symbolic architecture that combines large
language models, external knowledge sources and discrete reasoning [50.40151403246205]
巨大な言語モデル(LM)は、自然言語ベースの知識タスクのゲートウェイとして機能する、AIの新しい時代を支えている。
離散的な知識と推論モジュールによって補完される、複数のニューラルモデルによる柔軟なアーキテクチャを定義する。
本稿では,MRKL(Modular Reasoning, Knowledge and Language)システムと呼ばれる,このニューロシンボリックアーキテクチャについて述べる。
論文 参考訳（メタデータ） (2022-05-01T11:01:28Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。