論文の概要: Towards Operation Proof Obligation Generation for VDM
- arxiv url: http://arxiv.org/abs/2506.12858v1
- Date: Sun, 15 Jun 2025 14:18:17 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-06-17 17:28:47.006791
- Title: Towards Operation Proof Obligation Generation for VDM
- Title(参考訳): VDMのオペレーティング・オブ・グリーテーション・ジェネレーションに向けて
- Authors: Nick Battle, Peter Gorm Larsen,
- Abstract要約: 義務の生成は、メソッドをサポートするツールの重要な役割である。
この作業では、この問題に対処するための現在の作業状況を説明し、これまでの能力を示し、残りの作業を強調します。
- 参考スコア(独自算出の注目度): 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: All formalisms have the ability to ensure that their models are internally consistent. Potential inconsistencies are generally highlighted by assertions called proof obligations, and the generation of these obligations is an important role of the tools that support the method. This capability has been available for VDM tools for many years. However, support for obligation generation for explicit operation bodies has always been limited. This work describes the current state of work to address this, showing the capabilities so far and highlighting the work remaining.
- Abstract(参考訳): すべての形式主義は、モデルが内部的に一貫したものであることを保証する能力を持っている。
潜在的な矛盾は一般に証明義務と呼ばれる主張によって強調され、これらの義務の生成はメソッドをサポートするツールの重要な役割である。
この機能は長年VDMツールで利用されてきた。
しかし、明示的な運用機関に対する義務生成のサポートは常に制限されている。
この作業では、この問題に対処するための現在の作業状況を説明し、これまでの能力を示し、残りの作業を強調します。
関連論文リスト
- From Passive Metric to Active Signal: The Evolving Role of Uncertainty Quantification in Large Language Models [77.04403907729738]
このサーベイは、受動的診断基準からリアルタイムモデル動作を導くアクティブ制御信号への不確実性の進化をグラフ化する。
3つのフロンティアにまたがるアクティブ制御信号として不確実性がいかに活用されているかを示す。
この調査は、次世代のスケーラブルで信頼性があり、信頼できるAIを構築するためには、新しい不確実性のトレンドを習得することが不可欠である、と論じている。
論文 参考訳(メタデータ) (2026-01-22T06:21:31Z) - PosA-VLA: Enhancing Action Generation via Pose-Conditioned Anchor Attention [92.85371254435074]
PosA-VLAフレームワークは、ポーズ条件付き監視を通じて視覚的注意を保ち、タスク関連領域に対するモデルの認識を一貫して導く。
本手法は,多様なロボット操作ベンチマークにおいて,正確かつ時間効率のよい動作を実施できることを示す。
論文 参考訳(メタデータ) (2025-12-03T12:14:29Z) - Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems [0.5156484100374059]
大規模言語モデル(LLM)は、自然言語を形式的なアーティファクトに翻訳し、データのパターンを認識するのに優れています。
このビジョンペーパーは、RVとLLMの共生的な統合を論じている。
RV は LLM による自律性のためのガードレールとして機能し、一方 LLM は RV を拡張して仕様取得を支援し、予測推論をサポートし、不確実性に対処する。
論文 参考訳(メタデータ) (2025-11-18T12:35:05Z) - Modeling and Managing Temporal Obligations in GUCON Using SPARQL-star and RDF-star [0.17999333451993949]
利用制御の中枢的なメカニズムは義務の扱いであり、これはデータの使用と共有の副作用として生じる。
義務の効果的な監視には、使用トレースのキャプチャと、開始時間や期限などの時間的側面の会計が必要である。
我々は、義務の時間的側面を明示的にモデル化するために、SPAQRLグラフパターンの形式的意味論に基づくポリシーフレームワークであるGUCONを拡張した。
論文 参考訳(メタデータ) (2025-10-06T09:58:05Z) - The Landscape of Agentic Reinforcement Learning for LLMs: A Survey [103.32591749156416]
エージェント強化学習(Agentic RL)の出現は、大規模言語モデル(LLM RL)に適用された従来の強化学習からパラダイムシフトを示している。
本研究では, LLM-RLの縮退した単段階マルコフ決定過程(MDPs)と, エージェントRLを定義する部分可観測マルコフ決定過程(POMDPs)とを対比することにより, この概念シフトを定式化する。
論文 参考訳(メタデータ) (2025-09-02T17:46:26Z) - Agent Identity Evals: Measuring Agentic Identity [0.5524804393257919]
我々は,LMAシステムがエージェントアイデンティティを時間とともに保持する程度を測定するための,厳密で統計的に駆動された実証的なフレームワークであるテクスタイジェント・アイデンティティ・エバルス(AIE)を紹介した。
AIEは、最適なLMAインフラストラクチャの設計を支援するために、他のパフォーマンス、能力、エージェントの指標と統合できる新しいメトリクスのセットで構成されている。
論文 参考訳(メタデータ) (2025-07-23T06:56:15Z) - Graphs Meet AI Agents: Taxonomy, Progress, and Future Opportunities [117.49715661395294]
データ構造化は、複雑で非組織的なデータをよく構造化された形式に変換することで、有望な役割を果たす。
この調査では、グラフがAIエージェントにどのように権限を与えるかを、初めて体系的にレビューする。
論文 参考訳(メタデータ) (2025-06-22T12:59:12Z) - Dispositions and Roles of Generically Dependent Entities [0.0]
BFO 2020は、機能、配置、および一般的な依存的な連続体の役割をサポートしない。
この問題に対処する2つのアプローチが提示される。
論文 参考訳(メタデータ) (2025-06-20T15:40:45Z) - From Generation to Generalization: Emergent Few-Shot Learning in Video Diffusion Models [65.0487600936788]
ビデオ拡散モデル(VDM)は高品質なコンテンツを合成できる強力な生成ツールとして登場した。
我々は、VDMが自然に構造化された表現を探索し、視覚世界を暗黙的に理解することを主張する。
提案手法は,各タスクを視覚遷移に変換し,短い入力シーケンス上でLoRA重みのトレーニングを可能にする。
論文 参考訳(メタデータ) (2025-06-08T20:52:34Z) - Agentic AI Process Observability: Discovering Behavioral Variability [2.273531916003657]
大規模言語モデル(LLM)を利用するAIエージェントは、現代のソフトウェアシステムの中核的な構成要素になりつつある。
フレームワークは自然言語のプロンプトを使ってエージェントの設定を定義することができる。
このような設定では、エージェントの振る舞いは任意の入力に対して非決定論的である。
論文 参考訳(メタデータ) (2025-05-26T15:26:07Z) - On the Robustness of Agentic Function Calling [5.0243930429558885]
大規模言語モデル(LLM)は、タスクのための特定のツールを呼び出すことができる機能呼び出し(FC)機能を備えた、自律的なエージェントとしてますます機能している。
本稿では,2つの重要な領域においてFCのロバスト性を評価するベンチマークを紹介する。
論文 参考訳(メタデータ) (2025-04-01T15:48:26Z) - AgentOps: Enabling Observability of LLM Agents [12.49728300301026]
大規模言語モデル(LLM)エージェントは、自律的で非決定論的行動のため、AI安全性に重大な懸念を提起する。
本稿では,エージェントのライフサイクル全体を通じて追跡されるべきアーティファクトと関連するデータを特定し,効果的な観測可能性を実現するための,AgentOpsの包括的な分類法を提案する。
私たちの分類は、監視、ロギング、分析をサポートするAgentOpsインフラストラクチャを設計、実装するためのリファレンステンプレートとして機能します。
論文 参考訳(メタデータ) (2024-11-08T02:31:03Z) - States Hidden in Hidden States: LLMs Emerge Discrete State Representations Implicitly [72.24742240125369]
本稿では,チェーン・オブ・ステップ・バイ・ステップの解に頼らずに,拡張された計算列を実行する本質的な能力を明らかにする。
注目すべきは、最も先進的なモデルでは、2桁の加算結果を直接出力できることだ。
論文 参考訳(メタデータ) (2024-07-16T06:27:22Z) - WorkArena++: Towards Compositional Planning and Reasoning-based Common Knowledge Work Tasks [85.95607119635102]
大型言語モデル(LLM)は人間のような知性を模倣することができる。
WorkArena++は、Webエージェントの計画、問題解決、論理的/論理的推論、検索、コンテキスト的理解能力を評価するように設計されている。
論文 参考訳(メタデータ) (2024-07-07T07:15:49Z) - Reasoning or Reciting? Exploring the Capabilities and Limitations of Language Models Through Counterfactual Tasks [71.19560970717495]
最近の言語モデルは、幅広いタスクで印象的なパフォーマンスを示している。
これらのスキルは一般的で、移行可能か、あるいは事前トレーニング中に見られる特定のタスクに特化していますか?
本稿では,標準タスクの既定前提から逸脱する「数値的」タスク変種に基づく評価フレームワークを提案する。
論文 参考訳(メタデータ) (2023-07-05T17:50:42Z) - Hierarchical Few-Shot Imitation with Skill Transition Models [66.81252581083199]
FIST(Few-shot Imitation with Skill Transition Models)は、オフラインデータからスキルを抽出し、それらを利用して見えないタスクに一般化するアルゴリズムである。
本稿では,FISTが新たなタスクに一般化し,ナビゲーション実験において従来のベースラインを大幅に上回っていることを示す。
論文 参考訳(メタデータ) (2021-07-19T15:56:01Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。