Fugu-MT 論文翻訳(概要): Formal Semantics and Formally Verified Validation for Temporal Planning

論文の概要: Formal Semantics and Formally Verified Validation for Temporal Planning

arxiv url: http://arxiv.org/abs/2203.13604v1
Date: Fri, 25 Mar 2022 12:04:03 GMT
ステータス: 処理完了
システム内更新日: 2022-03-28 18:49:22.250466
Title: Formal Semantics and Formally Verified Validation for Temporal Planning
Title（参考訳）: 形式的意味論と時間計画のための形式的検証
Authors: Mohammad Abdulaziz, Lukas Koller
Abstract要約: 時間計画のための簡潔で簡潔な意味論を提示する。このセマンティクスは対話型定理証明器 Isabelle/HOL の論理で開発・形式化されている。我々はこれらのセマンティクスから時間計画のための検証アルゴリズムを導き、Isabelle/HOLの形式的証明を用いて、この検証アルゴリズムが我々のセマンティクスを実装していることを示す。
参考スコア（独自算出の注目度）: 7.538482310185133
License: http://creativecommons.org/licenses/by/4.0/
Abstract: We present a simple and concise semantics for temporal planning. Our semantics are developed and formalised in the logic of the interactive theorem prover Isabelle/HOL. We derive from those semantics a validation algorithm for temporal planning and show, using a formal proof in Isabelle/HOL, that this validation algorithm implements our semantics. We experimentally evaluate our verified validation algorithm and show that it is practical.
Abstract（参考訳）: 時間計画のための簡潔で簡潔な意味論を提示する。このセマンティクスは対話型定理証明器 Isabelle/HOL の論理で開発・形式化されている。これらのセマンティクスから時間計画のための検証アルゴリズムを導出し、イザベル/ホルの形式的証明を用いて、この検証アルゴリズムが我々のセマンティクスを実装していることを示す。検証アルゴリズムを実験的に評価し,実用的であることを示す。

関連論文リスト

Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文参考訳（メタデータ） (2024-07-14T01:43:07Z)
LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
本研究では,自然言語フィードバック型検証器Math-Minosを提案する。実験の結果,少量の自然言語フィードバックが検証器の性能を大幅に向上させることがわかった。
論文参考訳（メタデータ） (2024-06-20T06:42:27Z)
Learning Temporal Logic Predicates from Data with Statistical Guarantees [0.0]
有限サンプル精度保証データから時間論理の述語を学習する新しい手法を提案する。提案手法は,表現最適化と共形予測を利用して,将来の軌跡を正しく記述した述語を学習する。
論文参考訳（メタデータ） (2024-06-15T00:07:36Z)
Formally Verified Approximate Policy Iteration [11.602089225841633]
形式化されたアルゴリズムが実行可能で検証可能な実装にどのように洗練されるかを示す。実装は、その実行可能性を示すために、ベンチマーク問題で評価される。この改良の一環として,線形プログラミングソリューションを認証する検証ソフトウェアを開発した。
論文参考訳（メタデータ） (2024-06-11T15:07:08Z)
Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs [5.045988012508899]
オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
論文参考訳（メタデータ） (2023-01-05T17:56:00Z)
Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。これは、説明に表される論理述語に基づいて、反実仮説を生成する。そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
論文参考訳（メタデータ） (2022-05-25T03:40:59Z)
Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文参考訳（メタデータ） (2022-04-28T17:57:33Z)
Learning Implicitly with Noisy Data in Linear Arithmetic [94.66549436482306]
PAC-セマンティックスにおける暗黙学習を拡張し、線形算術の言語における間隔としきい値の不確実性を扱う。最適線形プログラミング対象制約の学習に対する我々の暗黙的アプローチは、実際的な明示的アプローチよりも著しく優れていることを示す。
論文参考訳（メタデータ） (2020-10-23T19:08:46Z)
Counterfactual Detection meets Transfer Learning [48.82717416666232]
既存のモデルアーキテクチャに最小限の適応で実装可能な,単純なバイナリ分類タスクであることを示す。本稿では,先行者や後続者をエンティティ認識タスクとして処理するエンド・ツー・エンドパイプラインを導入し,それらをトークン分類に適用する。
論文参考訳（メタデータ） (2020-05-27T02:02:57Z)
Adaptive Teaching of Temporal Logic Formulas to Learners with Preferences [44.63937003271641]
時間論理式に対する機械教育について検討する。ミオピック溶液の徹底的な探索には指数的時間を要する。パラメトリック線形時間論理式を効率よく教える手法を提案する。
論文参考訳（メタデータ） (2020-01-27T18:22:53Z)
Understanding the QuickXPlain Algorithm: Simple Explanation and Formal Proof [0.0]
本稿では,Ulrich Junker の QuickXPlain アルゴリズムの正当性を示す。他のアルゴリズムを証明するためのガイダンスとして使用できる。また、QuickXPlainによって計算された結果に依存するシステムの"ギャップレス"な正しさを提供する可能性も提供する。
論文参考訳（メタデータ） (2020-01-07T01:37:41Z)

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