Fugu-MT 論文翻訳(概要): Formally Verified SAT-Based AI Planning

論文の概要: Formally Verified SAT-Based AI Planning

arxiv url: http://arxiv.org/abs/2010.14648v4
Date: Thu, 17 Dec 2020 18:21:00 GMT
ステータス: 処理完了
システム内更新日: 2022-10-02 12:41:53.091902
Title: Formally Verified SAT-Based AI Planning
Title（参考訳）: SATベースのAI計画の形式的検証
Authors: Mohammad Abdulaziz and Friedrich Kurz
Abstract要約: 本稿では,従来のAI計画のSAT符号化について述べる。検証された符号化を実験的に検証し、合理的な大きさの標準計画ベンチマークに使用できることを示す。我々はまた、最先端のSATベースのプランナーをテストするための参照として使用し、時には問題に一定の長さの解がないという誤った主張を示す。
参考スコア（独自算出の注目度）: 7.538482310185133
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: We present an executable formally verified SAT encoding of classical AI planning. We use the theorem prover Isabelle/HOL to perform the verification. We experimentally test the verified encoding and show that it can be used for reasonably sized standard planning benchmarks. We also use it as a reference to test a state-of-the-art SAT-based planner, showing that it sometimes falsely claims that problems have no solutions of certain lengths.
Abstract（参考訳）: 本稿では,従来のAI計画のSAT符号化について述べる。定理証明器 Isabelle/HOL を用いて検証を行う。検証された符号化を実験的に検証し、合理的な大きさの標準計画ベンチマークに使用できることを示す。我々はまた、最先端のSATベースのプランナーをテストするための参照として使用し、時には問題に一定の長さの解がないと主張する。

関連論文リスト

Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
論文参考訳（メタデータ） (2024-10-18T22:25:54Z)
Learning Reliable Logical Rules with SATNet [7.951021955925275]
我々は、入力出力の例から基礎となるルールを学習する差別化可能なMaxSATソルバSATNetの上に構築する。基礎的真理規則に対して有効な検証手法をいくつか導入する。ストリームトランスフォーメーションとスドク問題に関する実験は、デコードされたルールが信頼性が高いことを示している。
論文参考訳（メタデータ） (2023-10-03T15:14:28Z)
Explaining SAT Solving Using Causal Reasoning [30.469229388827443]
本稿では、因果推論を用いて、現代のSATソルバの機能に関する洞察を得るCausalSATを紹介する。われわれはCausalSATを用いて,これまで「親指のルール」や経験的発見と考えられていた仮説を定量的に検証した。
論文参考訳（メタデータ） (2023-06-09T22:53:16Z)
Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
LEC インスタンスの SAT 符号化の硬さは SAT パーティショニングでは textitw.r. と推定できることを示す。そこで本研究では, SAT符号化の難易度を精度良く推定できるパーティショニング法を提案する。
論文参考訳（メタデータ） (2022-10-04T09:19:13Z)
Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文参考訳（メタデータ） (2022-04-28T17:57:33Z)
Probing for the Usage of Grammatical Number [103.8175326220026]
私たちは、モデルが実際に使用しているエンコーディングを見つけようと試み、使用量ベースの探索設定を導入しました。 BERTの文法的数値のエンコード方法と,このエンコーディングを用いて数値合意課題を解決する方法に焦点をあてる。
論文参考訳（メタデータ） (2022-04-19T11:59:52Z)
Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
本論文は, Boolean satisfiability problem (SAT) を機械学習技術で解くことに関する最近の文献をレビューする。 ML-SATソルバを手作り特徴を持つナイーブ分類器からNeuroSATのような新たなエンド・ツー・エンドSATソルバまで,進化するML-SATソルバについて検討する。
論文参考訳（メタデータ） (2022-03-02T05:14:12Z)
Learning Symbolic Rules for Reasoning in Quasi-Natural Language [74.96601852906328]
我々は,ルールを手作業で構築することなく,自然言語入力で推論できるルールベースシステムを構築した。本稿では,形式論理文と自然言語文の両方を表現可能な"Quasi-Natural"言語であるMetaQNLを提案する。提案手法は,複数の推論ベンチマークにおける最先端の精度を実現する。
論文参考訳（メタデータ） (2021-11-23T17:49:00Z)
Planning with Incomplete Information in Quantified Answer Set Programming [1.3501640559999886]
ASP(Answer Set Programming)における不完全な情報を用いた計画手法を提案する。論理プログラムが状態間の遷移関数を記述する単純な形式主義を用いて計画問題を表現している。本稿では、量子化された論理プログラムをQBFに変換し、QBFソルバを実行する翻訳ベースのQASPソルバを提案する。
論文参考訳（メタデータ） (2021-08-13T21:24:47Z)
Comprehensible Counterfactual Explanation on Kolmogorov-Smirnov Test [56.5373227424117]
我々は,KSテストに失敗するテストデータに対して,反実的説明を生成する問題に対処する。我々は、KSテストに失敗したテストセットの指数的なサブセット数を列挙し、チェックするのを避ける効率的なアルゴリズムMOCHEを開発した。
論文参考訳（メタデータ） (2020-11-01T06:46:01Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。