論文の概要: Proof-Carrying Plans: a Resource Logic for AI Planning
- arxiv url: http://arxiv.org/abs/2008.04165v2
- Date: Wed, 28 Oct 2020 03:49:19 GMT
- ステータス: 処理完了
- システム内更新日: 2022-10-31 23:32:20.067780
- Title: Proof-Carrying Plans: a Resource Logic for AI Planning
- Title(参考訳): Proof-Carrying Plans: AIプランニングのためのリソース論理
- Authors: Alasdair Hill, Ekaterina Komendantskaya, Ronald P. A. Petrick
- Abstract要約: AI検証と説明可能なAIの最近の傾向は、AI計画技術を検証することができるかどうかという疑問を提起している。
本稿では,AIプランナが作成した計画の検証に使用できる新しい資源論理,Proof Carrying Plans (PCP) ロジックを提案する。
- 参考スコア(独自算出の注目度): 1.7403133838762446
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Recent trends in AI verification and Explainable AI have raised the question
of whether AI planning techniques can be verified. In this paper, we present a
novel resource logic, the Proof Carrying Plans (PCP) logic that can be used to
verify plans produced by AI planners. The PCP logic takes inspiration from
existing resource logics (such as Linear logic and Separation logic) as well as
Hoare logic when it comes to modelling states and resource-aware plan
execution. It also capitalises on the Curry-Howard approach to logics, in its
treatment of plans as functions and plan pre- and post-conditions as types.
This paper presents two main results. From the theoretical perspective, we show
that the PCP logic is sound relative to the standard possible world semantics
used in AI planning. From the practical perspective, we present a complete Agda
formalisation of the PCP logic and of its soundness proof. Moreover, we
showcase the Curry-Howard, or functional, value of this implementation by
supplementing it with the library that parses AI plans into Agda's proofs
automatically. We provide evaluation of this library and the resulting Agda
functions.
- Abstract(参考訳): AI検証と説明可能なAIの最近の傾向は、AI計画技術を検証することができるかどうかという疑問を提起している。
本稿では,AIプランナが作成した計画の検証に使用できる新しい資源論理,Proof Carrying Plans (PCP) ロジックを提案する。
PCPロジックは、既存のリソースロジック(線形論理や分離論理など)や、状態のモデリングやリソース対応プランの実行に関して、Hoareロジックからインスピレーションを得ている。
また、機能としての計画、型としての事前およびポストコンディションの扱いにおいて、論理に対するカレーホワードのアプローチにも乗じている。
本稿は2つの主な結果を示す。
理論的な観点からは、PCP論理はAI計画で使用される標準的な世界意味論と比較して健全であることを示す。
実用の観点からは,PCP論理の完全形式化とその健全性証明について述べる。
さらに、aiプランを自動的にagdaの証明に解析するライブラリを補足することで、この実装のカレーホワード(機能的)な価値を提示する。
このライブラリと結果のAgda関数の評価を行う。
関連論文リスト
- Planning with OWL-DL Ontologies (Extended Version) [6.767885381740952]
フルパワー表現型DLをサポートするブラックボックスを提案する。
主要なアルゴリズムは、OWLによるPDDLへの計画仕様の書き直しに依存している。
いくつかのドメインからのベンチマークセットの実装を評価した。
論文 参考訳(メタデータ) (2024-08-14T13:27:02Z) - Learning Logic Specifications for Policy Guidance in POMDPs: an
Inductive Logic Programming Approach [57.788675205519986]
我々は任意の解法によって生成されるPOMDP実行から高品質なトレースを学習する。
我々は、データと時間効率のIndu Logic Programming(ILP)を利用して、解釈可能な信念に基づくポリシー仕様を生成する。
ASP(Answer Set Programming)で表現された学習は、ニューラルネットワークよりも優れた性能を示し、より少ない計算時間で最適な手作りタスクに類似していることを示す。
論文 参考訳(メタデータ) (2024-02-29T15:36:01Z) - LogicAsker: Evaluating and Improving the Logical Reasoning Ability of Large Language Models [63.14196038655506]
大規模言語モデル(LLM)の論理的推論能力を評価・拡張するための新しいアプローチであるLogicAskerを紹介する。
提案手法は, LLMが論理規則を学習する際の大きなギャップを明らかにし, 異なるモデル間で29%から90%の推論失敗を識別する。
GPT-4oのようなモデルにおける論理的推論を最大5%向上させることで、これらの知見を活用して、ターゲットとなる実演例と微調整データを構築した。
論文 参考訳(メタデータ) (2024-01-01T13:53:53Z) - DetermLR: Augmenting LLM-based Logical Reasoning from Indeterminacy to Determinacy [76.58614128865652]
非決定性から決定性への進化として推論過程を再考する新しい視点であるDetermLRを提案する。
まず、既知の条件を次の2つのタイプに分類する: 決定的および不決定的前提 これは、推論プロセスのオール方向を提供し、不決定的データを段階的決定的洞察に変換する際のLCMを導く。
我々は、利用可能な施設の保存と抽出、推論メモリによる推論パスの自動化、そしてその後の推論ステップに関する歴史的推論の詳細を保存する。
論文 参考訳(メタデータ) (2023-10-28T10:05:51Z) - Discourse-Aware Graph Networks for Textual Logical Reasoning [142.0097357999134]
パッセージレベルの論理関係は命題単位間の係り合いまたは矛盾を表す(例、結論文)
論理的推論QAを解くための論理構造制約モデリングを提案し、談話対応グラフネットワーク(DAGN)を導入する。
ネットワークはまず、インラインの談話接続とジェネリック論理理論を利用した論理グラフを構築し、その後、エッジ推論機構を用いて論理関係を進化させ、グラフ機能を更新することで論理表現を学習する。
論文 参考訳(メタデータ) (2022-07-04T14:38:49Z) - Modeling and Automating Public Announcement Logic with Relativized
Common Knowledge as a Fragment of HOL in LogiKEy [0.0]
本稿では,関連する共通知識を用いた発表ロジックのセマンティックな埋め込みについて述べる。
これにより、古典的な高階論理に対するオフ・ザ・シェルフ定理証明を用いて、この論理を初めて自動化することができる。
この研究は、複数派のLogiKEy知識工学方法論に重要な追加となる。
論文 参考訳(メタデータ) (2021-11-02T15:14:52Z) - Knowing How to Plan [0.0]
このようなロジックを使って、モデルチェックによるノウハウベースのプランニングを行います。
特に、ノウハウの公式を目標とする高次てんかん計画の処理が可能である。
論文 参考訳(メタデータ) (2021-06-22T02:47:06Z) - Actions You Can Handle: Dependent Types for AI Plans [2.064612766965483]
本稿では,AIプランナが作成したプランを依存型言語Agdaに組み込む手法を提案する。
ユーザーは、計画のより一般的で抽象的な特性を推論し、検証することができる。
論文 参考訳(メタデータ) (2021-05-24T13:33:56Z) - Online Learning Probabilistic Event Calculus Theories in Answer Set
Programming [70.06301658267125]
イベント認識(CER)システムは、事前に定義されたイベントパターンを使用して、ストリーミングタイムスタンプデータセットで発生を検出する。
本稿では,複雑なイベントパターンによる確率論的推論を,イベント計算で重み付けされたルールの形で行うことができるAnswer Set Programming(ASP)に基づくシステムを提案する。
その結果, 効率と予測の両面で, 新たなアプローチの優位性が示された。
論文 参考訳(メタデータ) (2021-03-31T23:16:29Z) - RNNLogic: Learning Logic Rules for Reasoning on Knowledge Graphs [91.71504177786792]
本稿では知識グラフに基づく推論のための論理規則の学習について研究する。
論理規則は、予測に使用されるときに解釈可能な説明を提供するとともに、他のタスクに一般化することができる。
既存の手法は、検索スペースの検索の問題や、スパース報酬による非効率な最適化に悩まされている。
論文 参考訳(メタデータ) (2020-10-08T14:47:02Z) - Public Announcement Logic in HOL [0.0]
関連する共通知識を持つ公開告知論理のための浅層セマンティック埋め込みについて述べる。
この埋め込みにより、古典的な高階論理に対するオフ・ザ・シェルフ定理証明を用いて、この論理を初めて自動化することができる。
論文 参考訳(メタデータ) (2020-10-02T06:46:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。