論文の概要: Realizability Is Not Enough: Encoding, Liveness, and Auditing of Synthesized Robot Supervisors
- arxiv url: http://arxiv.org/abs/2609.30460v1
- Date: Thu, 24 Sep 2026 18:51:13 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-28 18:27:51.107614
- Title: Realizability Is Not Enough: Encoding, Liveness, and Auditing of Synthesized Robot Supervisors
- Title（参考訳）: ロボットスーパーバイザのエンコード、生き、そして監査
- Abstract要約: 高レベルのロボットスーパーバイザーは、報告された結果がロボットの次の動作を決定する能力を調整する。
設計者は、障害を起こしやすい能力をエンコードし、リトライの意図にマッチする生命性の仮定を選択し、戦略を監査し、それらをロボットソフトウェアに変換する必要がある。
本稿では,ロボット・オペレーティング・システム (ROS) 2 フレキシブル・ビヘイビア・エンジン (FlexBE) のためのオープンソースのパイプラインについて述べる。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: High-level robotic supervisors coordinate capabilities whose reported outcomes determine the robot's next action. Reactive synthesis can generate such supervisors with formal guarantees, but deployment requires more than proving a Generalized Reactivity (1) (GR(1)) specification realizable. Designers must encode failure-prone capabilities, choose liveness assumptions that match retry intent, audit strategies, and translate them into robot software. We present an open-source pipeline for Robot Operating System (ROS) 2 Flexible Behavior Engine (FlexBE) supervisors that generates capability-based GR(1) specifications, analyzes assumptions before synthesis, audits strategies, reduces states with a behavior-preservation proof, and emits executable state machines. Across four case studies (six comparisons), including hardware on two quadcopter platforms, we compare enumerated and one-hot encodings and two liveness formulations. Under the tested backend, enumerated encoding usually synthesizes faster, although fewer propositions do not reliably predict smaller controllers or lower symbolic cost. System-Goal without pending memory is the only liveness treatment confirmed to yield executable controllers under both encodings across the reported grid; Fair-Outcome can permit realizable cycles without designer-intended completion. For this backend and model, we recommend enumerated encoding with System-Goal and auditing every realized strategy, since proposition count and realizability do not measure deployability. The auditor is sound and complete for four structural defect classes (protocol violations, deadlocks, bounded-failure violations, goal-unreachable traps) but is not a general liveness verifier, and the reduction preserves capability-level behavior. Together, these stages narrow the gap between formal realizability and controllers that pass protocol and structural-progress checks.
- Abstract（参考訳）: 高レベルのロボットスーパーバイザーは、報告された結果がロボットの次の動作を決定する能力を調整する。
反応合成はそのようなスーパーバイザーを正式な保証で生成することができるが、展開には一般化された反応(1)(GR(1))仕様の実現以上のものが必要である。
設計者は、障害を起こしやすい能力をエンコードし、リトライの意図にマッチする生命性の仮定を選択し、戦略を監査し、それらをロボットソフトウェアに変換する必要がある。
本稿では,ロボット・オペレーティング・システム (ROS) 2 のフレキシブル・ビヘイビア・エンジン (FlexBE) スーパーバイザのためのオープンソースのパイプラインについて述べる。
2つのクアッドコプタープラットフォーム上のハードウェアを含む4つのケーススタディ(6つのケーススタディ)において、列挙エンコーディングと1つのホットエンコーディングと2つのライブネス定式化を比較した。
テストされたバックエンドでは、列挙された符号化は通常より高速に合成されるが、より小さなコントローラやより低いシンボルコストを確実に予測する命題は少ない。
メモリを保留しないシステム目標(System-Goal without pending memory)は、報告されたグリッドの両エンコーディングの下で実行可能なコントローラを生成することが確認された唯一のライブ処理である。
このバックエンドとモデルのために、提案数と実現可能性はデプロイ可能性を測定するものではないため、System-Goalでエンコーディングを列挙し、実現した戦略をすべて監査することを推奨する。
オーディショナーは、4つの構造的欠陥クラス(プロトコール違反、デッドロック、境界欠陥違反、目標到達不能トラップ)に対して健全で完全であるが、一般的な生きた検証装置ではなく、能力レベルの動作を保っている。
これらのステージは、形式的な実現可能性と、プロトコルをパスするコントローラと構造的プログレスチェックの間のギャップを狭める。
関連論文リスト
- CSymPlan: Certified Symbolic Planning and Control for High-DOF Manipulators [4.257148651564725]
CSymPlanは、高DOFマニピュレータのためのシンボリックプランニングおよび制御フレームワークである。
オフライン実装は、既知のワークスペースに対する認証済みのリーチ回避フィードバックポリシーをプリ計算する。
オンライン実装は、タスクや知覚情報の変更から実行時にシンボリックポリシーを合成または更新する。
どちらの実装も、安全違反のないリーチ回避タスクを完了している。
論文 参考訳（メタデータ） (2026-08-24T08:45:37Z) - PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
我々は、スケジューリング、検証、メモリ、ベンチマーク、安全性をシステムレベルのサービスとして提供するPhyAgentOSを紹介します。
セッション中心のセッションは、スケジューリング、互換性、監督された実行、エビデンス収集、受け入れの最小単位として、アクションではなくセッションを扱う。
SessionVerifierは、実行終了とセマンティックタスク完了を、成功、失敗、または再計画のエビデンスに基づいて判断する。
ベンチマークはデプロイメントセッションと検証パスを再利用するので、結果は実際の実行に遡る。
論文 参考訳（メタデータ） (2026-07-18T04:46:53Z) - Heaviside Continuity of Rolling Coefficients for Eliminating Epistemic Entropy in Large Language Models [0.0]
Heaviside Continuity of Rolling Coefficients (HCRC) は検証ファーストな実行フレームワークである。
これは、ヘビサイドゲートが支配する述語による状態遷移として推論を再構成する。
HCRCは、モデルの信頼性と並列ワーカーアーキテクチャからの独立した検証信号を組み合わせることで、正しい予測が満たされた場合にのみ実行を前進させることができる。
論文 参考訳（メタデータ） (2026-07-06T00:29:34Z) - AuditWeave: A Tamper-Evident, Auditor-Navigable Evidence Layer for AI-Assisted and Data-Transformation Workflows [0.0]
AuditWeaveは、AIアシストとデータ変換のステップを1つのハッシュチェーンの台帳に記録する軽量Pythonライブラリである。
本稿では,参照実装におけるオーバヘッド,拡張性,タンパー検出の正確さを設計し,評価する。
論文 参考訳（メタデータ） (2026-06-14T21:46:04Z) - Protocol-Driven Development: Governing Generated Software Through Invariants and Continuous Evidence [2.124730017640531]
ここでは、主要なソフトウェアアーチファクトがコードではなく、機械で強化可能なプロトコルであるプロトコル駆動開発(PDD)を紹介します。
PDDは、自動化されたソフトウェアエンジニアリングのためのガバナンスモデルを定義する。
論文 参考訳（メタデータ） (2026-05-13T04:23:14Z) - PRISM: : Planning and Reasoning with Intent in Simulated Embodied Environments [59.07829883257003]
5つの集合住宅の上に建設され、PRISMは300の人間認証タスクを3つの能力レベルに構成する。
PRISMはエージェントに依存しない実行可能なアクションAPIを公開し、任意のエージェントをエンドツーエンドで評価できるようにする。
論文 参考訳（メタデータ） (2026-05-12T04:59:47Z) - CellScientist: Dual-Space Hierarchical Orchestration for Closed-Loop Refinement of Virtual Cell Models [62.281480231694]
VCM(Virtual Cell Modeling)は、摂動応答を予測できるだけでなく、予測が失敗した場合にターゲットリビジョンをサポートするモデルを必要とする。
現在のLCM支援モデリングでは、予測誤差が実行可能実装を通して観測されるという改善ルーティング問題に直面している。
提案するCellScientistは,高レベル仮説空間と低レベル実行可能実装空間を結合した,二重空間階層型フレームワークである。
論文 参考訳（メタデータ） (2026-05-08T06:40:24Z) - IMPACT-CYCLE: A Contract-Based Multi-Agent System for Claim-Level Supervisory Correction of Long-Video Semantic Memory [73.22944697933603]
既存のパイプラインは不透明でエンドツーエンドの出力を生成し、検査の中間状態は公開しない。
IMPACT-Cycleは,マルチモーダル反復クレームレベルのメンテナンスとして,長時間ビデオ理解を再構築するマルチエージェントシステムである。
論文 参考訳（メタデータ） (2026-04-22T03:03:33Z) - Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
生成のための教師なし共形推論フレームワークを提案する。
我々のゲートは、分断されたUPPよりも厳密で安定した閾値を提供する。
その結果は、ラベルのない、API互換の、テスト時間フィルタリングのゲートになる。
論文 参考訳（メタデータ） (2025-09-26T23:40:47Z) - Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。
実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
論文 参考訳（メタデータ） (2025-05-28T17:57:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。