論文の概要: ProsaBuddy: Assisting Mechanized Real-Time Schedulability Analysis with LLM-based Agents

• arxiv url: http://arxiv.org/abs/2610.03796v1
• Date: Thu, 01 Oct 2026 03:29:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-13 05:12:52.811551
• Title: ProsaBuddy: Assisting Mechanized Real-Time Schedulability Analysis with LLM-based Agents
• Title（参考訳）: ProsaBuddy: LLMエージェントを用いたリアルタイムスケジューリング支援
• Abstract要約: Prosaイニシアチブは、Rocq証明アシスタントでマシンチェック可能なスケジュール可能性分析証明を構築するための基盤を提供する。 この研究は、リアルタイムスケジューリング可能性証明を開発するのに必要な労力を減らすためにLLMベースのエージェントシステムであるProsaBuddyを提示する。
• 参考スコア（独自算出の注目度）: 12.793412574900957
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Rigorous schedulability analysis is essential for the design of hard real-time systems, yet errors in pen-and-paper proofs threaten the safety of critical applications. The Prosa initiative addresses this by offering a foundation for building machine-checkable schedulability analysis proofs in the Rocq proof assistant. However, the substantial time and expertise required to construct such proofs remain a major barrier for wider adoption of Prosa. This work presents ProsaBuddy, an LLM?based agent system designed to lower the effort needed to develop mechanized real-time schedulability proofs. ProsaBuddy employs a ReAct loop with retrieval over the Prosa codebase, access to Rocq tools and optional human-written hints. It uses a subgoal?delegation architecture, decomposing a lemma into subgoals and dispatches them to subagents for proof. We evaluate ProsaBuddy on a mini benchmark drawn from real-time scheduling literature. Experiment results show that ProsaBuddy significantly outper?forms state-of-the-art LLM-based Rocq automated proving agent systems and a general coding agent OpenCode
• Abstract（参考訳）: 厳密なスケジューリング可能性分析は、ハードリアルタイムシステムの設計には不可欠であるが、ペンとペーパーの証明における誤りは、クリティカルなアプリケーションの安全性を脅かす。 Prosaイニシアチブは、Rocq証明アシスタントでマシンチェック可能なスケジュール可能性分析証明を構築するための基盤を提供することで、この問題に対処している。 しかし、そのような証明を構築するのに必要なかなりの時間と専門知識は、 Prosa を広く採用する上で大きな障壁となっている。 この作品は、LLMであるProsaBuddyを提示しますか? ベースエージェントシステムは、機械化されたリアルタイムスケジューリング可能性証明を開発するのに必要な労力を減らすように設計されている。 ProsaBuddyはReActループを使用し、Prosaコードベース上での検索、Rocqツールへのアクセス、オプションの人書きヒントを提供している。 サブゴールを使うのか? アーキテクチャを委譲し、レムマをサブゴールに分解し、証明のためにサブエージェントに送る。 ProsaBuddyを,リアルタイムスケジューリングの文献から抽出したミニベンチマークで評価する。 実験の結果、ProsaBuddyは大幅に上回ったか? 最先端のLLMベースのRocq自動証明エージェントシステムと一般的なコーディングエージェントOpenCodeを形成する

関連論文リスト

• AgentR A Stateful and Recovery-Aware Software Architecture for LLM-based Auditable Workflows [14.042464830509864]
  AgentRは、研究意図、生成されたクエリ、候補論文の評価、ギャップ分析を耐久性のあるワークフローアーティファクトとして表現する。 設計には、明示的な処理状態遷移、指数的バックオフによるリトライ、クレジット対応の事前チェック、ACIDトークンコストのログ、価格レコードの徐々に変化するType-2が含まれている。 LLMの段階では、99.2%のジョブ完了を達成し、意図分解、クエリ生成、および紙スコアのための平均遅延は9.0秒、18.9秒25.4秒である。
  論文  参考訳（メタデータ） (2026-08-15T14:51:43Z)
• PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs [2.6015820133532137]
  本稿では, PROSA/ROCQ スクリプトを生成する LLM 支援フレームワーク PROVE-RT を紹介する。 我々は,1,191のリアルタイムシステム論文から機械化指向コーパスを構築し,134の非公式スケッチと依存関係情報を含む。 キュレートされた評価セットでは、最先端のLLMの直接的なプロンプトは有効なPROSA機構を確実に生成することができず、PROVE-RTは44.7%の成功率を達成する。
  論文  参考訳（メタデータ） (2026-08-13T03:12:17Z)
• The Optimizer Is the Agent: Reasoning-Driven Search across Prompts, Programs, and ML Workflows [72.9051182568928]
  推論駆動最適化のための統合フレームワークであるReASearchを提案する。 共有エージェントループとドメイン固有のツールにより、ReASearchは、プロンプト、プログラム、MLを最適化するために、まったく同じスキャフォールドをインスタンス化する。 我々は,複雑な探索行動がエージェントの推論プロセスから自然に現れることを観察する。
  論文  参考訳（メタデータ） (2026-08-07T02:15:39Z)
• Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs [21.65389718022749]
  提案するQuarryは,証明計画と証明実行を分離した,計画に基づく証明合成フレームワークである。 特に、Quarry は LLM に対して、任意のサブレンマを持つ複数の証明分解を積極的に提案するよう求め、Rocq で一時的に承認されたサブレンマの下でそれらをタイプチェックし、証明状態に基づく困難モデルを用いて候補をランク付けする。 可解性を考慮した評価による計画ベース分解は,予測可能なコストを維持しつつ,自動化を大幅に改善することを示す。
  論文  参考訳（メタデータ） (2026-06-16T14:33:15Z)
• Collider-Bench: Benchmarking AI Agents with Particle Physics Analysis Reproduction [0.02446672595462589]
  我々は,LHC(Large Hadron Collider)から,公開論文とオープンサイエンスソフトウェアのみを用いて,言語モデルエージェントが実験分析を再現できるかどうかを評価するベンチマークであるCollind-Benchを紹介する。 したがってエージェントは、これらのギャップを埋めるために、物理的推論、ドメイン知識、試行錯誤に頼らなければならない。 以上の結果から, 平均的なエージェントが, ループ内解法を確実に打ち負かすことは不可能であることが示唆された。
  論文  参考訳（メタデータ） (2026-05-13T18:00:00Z)
• When Should a Robot Think? Resource-Aware Reasoning via Reinforcement Learning for Embodied Robotic Decision-Making [68.12864562049957]
  身体ロボットシステムは、高レベルの推論をサポートするために、大規模言語モデル(LLM)ベースのエージェントにますます依存している。 エージェントはいつ、いつ、いつ行動すべきか? 本稿では,エンボディエージェントのリソース・アウェア・オーケストレーションのための階層的なフレームワークであるRARRL(Resource-Aware Reasoning via Reinforcement Learning)を提案する。
  論文  参考訳（メタデータ） (2026-03-17T15:38:50Z)
• Understanding by Reconstruction: Reversing the Software Development Process for LLM Pretraining [66.89012795621349]
  大規模言語モデル(LLM)は、複雑なソフトウェア工学に必要な、深く、長期にわたる推論に苦しむことが多い。 本稿では,再構築による理解という,新しいパラダイムを提案する。 マルチエージェントシミュレーションを用いて潜在エージェント軌道を合成するフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-03-11T09:23:20Z)
• AI-for-Science Low-code Platform with Bayesian Adversarial Multi-Agent Framework [4.782965804438204]
  大規模言語モデル(LLM)は、科学的コード生成を自動化する可能性を示しているが、信頼性、エラーの伝播、評価において課題に直面している。 我々は,AI for Science(AI4S)タスクを低符号プラットフォーム(LCP)の形で特別に設計したベイズ対向型マルチエージェントフレームワークを提案する。 ユーザ入力を実行可能な計画と適応テストケースに構造化するタスクマネージャ、候補ソリューションを生成するコードジェネレータ、包括的なフィードバックを提供する評価器である。
  論文  参考訳（メタデータ） (2026-03-03T18:25:00Z)
• NL2Repo-Bench: Towards Long-Horizon Repository Generation Evaluation of Coding Agents [79.29376673236142]
  既存のベンチマークは、完全なソフトウェアシステムを構築するのに必要な長期的能力の厳格な評価に失敗する。 符号化エージェントの長期リポジトリ生成能力を評価するために設計されたベンチマークであるNL2Repo Benchを提案する。
  論文  参考訳（メタデータ） (2025-12-14T15:12:13Z)

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

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