論文の概要: Modular Answer Set Programming as a Formal Specification Language
- arxiv url: http://arxiv.org/abs/2008.02015v2
- Date: Fri, 7 Aug 2020 09:40:40 GMT
- ステータス: 処理完了
- システム内更新日: 2022-11-02 18:29:32.884149
- Title: Modular Answer Set Programming as a Formal Specification Language
- Title（参考訳）: 形式仕様言語としてのモジュラアンサーセットプログラミング
- Authors: Pedro Cabalar, Jorge Fandinno and Yuliya Lierler
- Abstract要約: ASP(Answer Set Programming)の形式検証問題について検討する。
与えられた(非基底)論理プログラムPの解集合が、問題インスタンスに関係なく、Pによって符号化された問題の解に正しく対応していることを示す公式な証明を得る。
- 参考スコア（独自算出の注目度）: 8.823761706435814
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In this paper, we study the problem of formal verification for Answer Set
Programming (ASP), namely, obtaining a formal proof showing that the answer
sets of a given (non-ground) logic program P correctly correspond to the
solutions to the problem encoded by P, regardless of the problem instance. To
this aim, we use a formal specification language based on ASP modules, so that
each module can be proved to capture some informal aspect of the problem in an
isolated way. This specification language relies on a novel definition of
(possibly nested, first order) program modules that may incorporate local
hidden atoms at different levels. Then, verifying the logic program P amounts
to prove some kind of equivalence between P and its modular specification.
Under consideration for acceptance in TPLP.
- Abstract（参考訳）: 本稿では,与えられた(非基底)論理プログラムPの解集合が,問題事例に関わらず,Pによって符号化された問題に対する解に正しく対応していることを示す形式的証明を得るために,解答集合プログラミング(ASP)の形式的検証の問題について検討する。
この目的のために、ASPモジュールに基づいた正式な仕様言語を使用し、各モジュールが独立した方法で問題の非公式な側面をキャプチャできることを証明できる。
この仕様言語は、異なるレベルに局所隠れ原子を組み込むことができる(おそらく入れ子、一階)プログラムモジュールの新しい定義に依存している。
すると、論理プログラム P の検証は、P とモジュラー仕様の間の何らかの同値性を証明する。
TPLPの受容についての検討
関連論文リスト
- Combining Logic with Large Language Models for Automatic Debugging and Repair of ASP Programs [1.0650780147044159]
FormHeは、ロジックベースのテクニックと大規模言語モデルを組み合わせて、Answer Set Programmingの課題を特定し、修正するツールである。
以上の結果から,FormHeは94%の症例の欠陥を正確に検出し,誤りの58%を修復することに成功した。
論文 参考訳（メタデータ） (2024-10-28T12:30:48Z) - Inductive Predicate Synthesis Modulo Programs (Extended) [1.7372615815088566]
プログラム解析のトレンドは、入力プログラムの言語内で検証条件を符号化することである。
Inductive Predicate Synthesis Modulo Programs (IPS-MP) を提案する。
論文 参考訳（メタデータ） (2024-07-11T12:51:08Z) - Is Modularity Transferable? A Case Study through the Lens of Knowledge Distillation [59.37775534633868]
同族PLM間で事前訓練されたタスク固有のPEFTモジュールを転送するための極めて簡単なアプローチを提案する。
また,不整合性PLM間のモジュールの移動を,推論複雑性の変化を伴わずに行う方法を提案する。
論文 参考訳（メタデータ） (2024-03-27T17:50:00Z) - How Proficient Are Large Language Models in Formal Languages? An In-Depth Insight for Knowledge Base Question Answering [52.86931192259096]
知識ベース質問回答(KBQA)は,知識ベースにおける事実に基づいた自然言語質問への回答を目的としている。
最近の研究は、論理形式生成のための大規模言語モデル(LLM)の機能を活用して性能を向上させる。
論文 参考訳（メタデータ） (2024-01-11T09:27:50Z) - SCREWS: A Modular Framework for Reasoning with Revisions [58.698199183147935]
我々は、リビジョンを伴う推論のためのモジュラーフレームワークであるSCREWSを紹介する。
我々は、SCREWSが、共通のフレームワークの下で、いくつかの以前のアプローチを統合することを示す。
我々は,多種多様な推論タスクに基づいて,最先端のLCMを用いてフレームワークの評価を行った。
論文 参考訳（メタデータ） (2023-09-20T15:59:54Z) - Coupling Large Language Models with Logic Programming for Robust and
General Reasoning from Text [5.532477732693001]
大規模言語モデルは, 意味論的に非常に効果的な数ショットとして機能することを示す。
自然言語文を論理形式に変換し、応答集合プログラムの入力として機能する。
本手法は,bAbI, StepGame, CLUTRR, gSCAN など,いくつかのベンチマークにおいて最先端性能を実現する。
論文 参考訳（メタデータ） (2023-07-15T03:29:59Z) - Resolution for Constrained Pseudo-Propositional Logic [0.0]
この研究は、制約付き擬似命題論理の解法証明システムを得るために、命題分解を一般化する方法を示す。
有限個の節に制限された CNF の公式の構成とは異なり、拡張された CPPL は対応する集合を有限とする必要はない。
論文 参考訳（メタデータ） (2023-06-11T09:17:24Z) - Faithful Question Answering with Monte-Carlo Planning [78.02429369951363]
本稿では,FAME(Fithful Questioning with Monte-carlo planning)を提案する。
我々は,タスクを離散的な意思決定問題として定式化し,推論環境とコントローラの相互作用によって解決する。
FAMEは標準ベンチマークで最先端のパフォーマンスを達成する。
論文 参考訳（メタデータ） (2023-05-04T05:21:36Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳（メタデータ） (2022-04-28T17:57:33Z) - Planning with Incomplete Information in Quantified Answer Set
Programming [1.3501640559999886]
ASP(Answer Set Programming)における不完全な情報を用いた計画手法を提案する。
論理プログラムが状態間の遷移関数を記述する単純な形式主義を用いて計画問題を表現している。
本稿では、量子化された論理プログラムをQBFに変換し、QBFソルバを実行する翻訳ベースのQASPソルバを提案する。
論文 参考訳（メタデータ） (2021-08-13T21:24:47Z) - Text Modular Networks: Learning to Decompose Tasks in the Language of
Existing Models [61.480085460269514]
本稿では,既存のモデルで解けるより単純なモデルに分解することで,複雑なタスクを解くための解釈可能なシステムを構築するためのフレームワークを提案する。
我々はこのフレームワークを用いて、ニューラルネットワークのファクトイド単一スパンQAモデルとシンボリック電卓で答えられるサブクエストに分解することで、マルチホップ推論問題に答えられるシステムであるModularQAを構築する。
論文 参考訳（メタデータ） (2020-09-01T23:45:42Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。