論文の概要: 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関数の評価を行う。
関連論文リスト
- 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) - LINC: A Neurosymbolic Approach for Logical Reasoning by Combining
Language Models with First-Order Logic Provers [60.009969929857704]
論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。
本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。
我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
論文 参考訳(メタデータ) (2023-10-23T17:58:40Z) - Towards LogiGLUE: A Brief Survey and A Benchmark for Analyzing Logical
Reasoning Capabilities of Language Models [58.76688462256284]
大規模言語モデル(LLM)は、形式的知識表現(KR)システムの様々な制限を克服する能力を示した。
一つのタスクトレーニング,複数タスクトレーニング,および思考知識の蒸留微調整手法の連鎖について検討し,異なる論理的推論カテゴリにおけるモデルの性能を評価する。
論文 参考訳(メタデータ) (2023-10-02T01:00:50Z) - Tableaux for the Logic of Strategically Knowing How [4.007651550424299]
本稿では,戦略的ノウハウの論理のマルチエージェント版のための表計算手順を提案する。
また、論理の満足度問題はPSPACEで決定可能であることも示している。
論文 参考訳(メタデータ) (2023-07-11T07:12: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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。