論文の概要: On the Verification of Belief Programs
- arxiv url: http://arxiv.org/abs/2204.12562v1
- Date: Tue, 26 Apr 2022 19:52:02 GMT
- ステータス: 処理完了
- システム内更新日: 2022-04-28 13:30:41.310266
- Title: On the Verification of Belief Programs
- Title（参考訳）: 信仰プログラムの検証について
- Authors: Daxin Liu and Gerhard Lakemeyer
- Abstract要約: 本稿では,行動・信念のモーダル論理に基づく信仰プログラムの形式化を提案する。
さらに,信念プログラムの検証問題に対する決定可能性や不決定性についても検討する。
- 参考スコア（独自算出の注目度）: 17.716702533701092
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In a recent paper, Belle and Levesque proposed a framework for a type of
program called belief programs, a probabilistic extension of GOLOG programs
where every action and sensing result could be noisy and every test condition
refers to the agent's subjective beliefs. Inherited from GOLOG programs, the
action-centered feature makes belief programs fairly suitable for high-level
robot control under uncertainty. An important step before deploying such a
program is to verify whether it satisfies properties as desired. At least two
problems exist in doing verification: how to formally specify properties of a
program and what is the complexity of verification. In a recent paper, Belle
and Levesque proposed a framework for a type of program called belief programs,
a probabilistic extension of GOLOG programs where every action and sensing
result could be noisy and every test condition refers to the agent's subjective
beliefs. Inherited from GOLOG programs, the action-centered feature makes
belief programs fairly suitable for high-level robot control under uncertainty.
An important step before deploying such a program is to verify whether it
satisfies properties as desired. At least two problems exist in doing
verification: how to formally specify properties of a program and what is the
complexity of verification. In this paper, we propose a formalism for belief
programs based on a modal logic of actions and beliefs. Among other things,
this allows us to express PCTL-like temporal properties smoothly. Besides, we
investigate the decidability and undecidability for the verification problem of
belief programs.
- Abstract（参考訳）: これはgologプログラムの確率的拡張であり、あらゆるアクションやセンシングの結果がうるさく、テスト条件がエージェントの主観的な信念を参照している。
GOLOGプログラムを継承したこの行動中心の機能は、不確実性の下で高いレベルのロボット制御に適した信念プログラムを実現する。
このようなプログラムをデプロイする前に重要なステップは、必要に応じてプロパティを満たすかどうかを検証することだ。
検証を行う際に少なくとも2つの問題が存在している:プログラムのプロパティを正式に指定する方法と、検証の複雑さである。
これはgologプログラムの確率的拡張であり、あらゆるアクションやセンシングの結果がうるさく、テスト条件がエージェントの主観的な信念を参照している。
GOLOGプログラムを継承したこの行動中心の機能は、不確実性の下で高いレベルのロボット制御に適した信念プログラムを実現する。
このようなプログラムをデプロイする前に重要なステップは、必要に応じてプロパティを満たすかどうかを検証することだ。
検証を行う際に少なくとも2つの問題が存在している:プログラムのプロパティを正式に指定する方法と、検証の複雑さである。
本稿では,行動と信念の様相論理に基づく信念プログラムの形式化を提案する。
中でもPCTLのような時間特性をスムーズに表現することができる。
さらに,信念プログラムの検証問題に対する決定可能性や不決定性についても検討する。
関連論文リスト
- miniCodeProps: a Minimal Benchmark for Proving Code Properties [22.548472305010005]
私たちはLeanの証明アシスタントで201のプログラム仕様のベンチマークであるminiCodePropsを紹介します。
その単純さにもかかわらず、MiniCodePropsは現在のLLMベースのプローバーを壊すのに十分である。
論文 参考訳（メタデータ） (2024-06-16T21:11:23Z) - Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
本稿では,検証対応言語における仕様の質を評価するための指標を提案する。
MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。
また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
論文 参考訳（メタデータ） (2024-06-14T06:52:08Z) - NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
大規模言語モデル(LLM)のコードは通常、プログラムの表面テキスト形式に基づいて訓練される。
NExTは,プログラムの実行トレースを検査し,実行時の動作を判断する手法である。
論文 参考訳（メタデータ） (2024-04-23T01:46:32Z) - Automatic Program Instrumentation for Automatic Verification (Extended
Technical Report) [0.0]
帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。
本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。
我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
論文 参考訳（メタデータ） (2023-05-26T14:55:35Z) - Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
Program-Guided Fact-Checking (ProgramFC)は、複雑なクレームを単純なサブタスクに分解する新しいファクトチェックモデルである。
まず,大規模言語モデルの文脈内学習能力を活用して推論プログラムを生成する。
我々は,各サブタスクを対応するサブタスクハンドラに委譲することでプログラムを実行する。
論文 参考訳（メタデータ） (2023-05-22T06:11:15Z) - Verification of Nondeterministic Quantum Programs [1.9302781323430196]
非決定論的選択は、実装の詳細を指定せずにプログラムの振る舞いを記述する方法を提供する有用なプログラム構成である。
非決定性は量子プログラミングにも導入され、非決定性量子プログラムの終了は広く分析されてきた。
論文 参考訳（メタデータ） (2023-02-15T22:37:23Z) - Generation Probabilities Are Not Enough: Uncertainty Highlighting in AI Code Completions [54.55334589363247]
本研究では,不確実性に関する情報を伝達することで,プログラマがより迅速かつ正確にコードを生成することができるかどうかを検討する。
トークンのハイライトは、編集される可能性が最も高いので、タスクの完了が早くなり、よりターゲットを絞った編集が可能になることがわかりました。
論文 参考訳（メタデータ） (2023-02-14T18:43:34Z) - Fault-Aware Neural Code Rankers [64.41888054066861]
サンプルプログラムの正しさを予測できる故障認識型ニューラルネットワークローダを提案する。
我々のフォールト・アウェア・ローダは、様々なコード生成モデルのpass@1精度を大幅に向上させることができる。
論文 参考訳（メタデータ） (2022-06-04T22:01:05Z) - Non-ground Abductive Logic Programming with Probabilistic Integrity
Constraints [2.624902795082451]
本稿では,変数の確率的推論に対処する,よりリッチな論理言語について考察する。
まず, 分配セマンティックスに基づいて, 全体としての帰納的言語とその意味を提示する。
次に,前述したものを拡張して得られた証明手順を導入し,その健全性と完全性を証明する。
論文 参考訳（メタデータ） (2021-08-06T10:22:12Z) - Enforcing Consistency in Weakly Supervised Semantic Parsing [68.2211621631765]
本稿では,関連する入力に対する出力プログラム間の整合性を利用して,スプリアスプログラムの影響を低減することを提案する。
より一貫性のあるフォーマリズムは、一貫性に基づくトレーニングを必要とせずに、モデルパフォーマンスを改善することにつながります。
論文 参考訳（メタデータ） (2021-07-13T03:48:04Z) - Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。
ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。
本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
論文 参考訳（メタデータ） (2020-10-07T08:19:48Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。