Formal Semantics and Formally Verified Validation for Temporal Planning

• URL: http://arxiv.org/abs/2203.13604v1
• Date: Fri, 25 Mar 2022 12:04:03 GMT
• Title: Formal Semantics and Formally Verified Validation for Temporal Planning
• Authors: Mohammad Abdulaziz, Lukas Koller
• Abstract summary: 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.
• Score: 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.

Related papers

• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof. Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
  We propose Math-Minos, a natural language feedback-enhanced verifier. Our experiments reveal that a small set of natural language feedback can significantly boost the performance of the verifier.
  arXiv  Detail & Related papers  (2024-06-20T06:42:27Z)
• Learning Temporal Logic Predicates from Data with Statistical Guarantees [0.0]
  We present a novel method to learn temporal logic predicates from data with finite-sample correctness guarantees. Our approach leverages expression optimization and conformal prediction to learn predicates that correctly describe future trajectories.
  arXiv  Detail & Related papers  (2024-06-15T00:07:36Z)
• Formally Verified Approximate Policy Iteration [11.602089225841633]
  We show how the formalized algorithm can be refined to an executable, verified implementation. The implementation is evaluated on benchmark problems to show its practicability. As part of the refinement, we develop verified software to certify Linear Programming solutions.
  arXiv  Detail & Related papers  (2024-06-11T15:07:08Z)
• Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs [5.045988012508899]
  Autoformalization seeks to address this by translating proofs written in natural language into a formal representation that is computer-verifiable via interactive theorem provers. We introduce a semantic parsing approach, based on the Universal Transformer architecture, that translates elementary mathematical proofs into an equivalent formalization in the language of the Coq interactive theorem prover.
  arXiv  Detail & Related papers  (2023-01-05T17:56:00Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  We introduce the methodology of Faithfulness-through-Counterfactuals. It generates a counterfactual hypothesis based on the logical predicates expressed in the explanation. It then evaluates if the model's prediction on the counterfactual is consistent with that expressed logic.
  arXiv  Detail & Related papers  (2022-05-25T03:40:59Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• Learning Implicitly with Noisy Data in Linear Arithmetic [94.66549436482306]
  We extend implicit learning in PAC-Semantics to handle intervals and threshold uncertainty in the language of linear arithmetic. We show that our implicit approach to learning optimal linear programming objective constraints significantly outperforms an explicit approach in practice.
  arXiv  Detail & Related papers  (2020-10-23T19:08:46Z)
• Counterfactual Detection meets Transfer Learning [48.82717416666232]
  We show that detecting Counterfactuals is a straightforward Binary Classification Task that can be implemented with minimal adaptation on already existing model Architectures. We introduce a new end to end pipeline to process antecedents and consequents as an entity recognition task, thus adapting them into Token Classification.
  arXiv  Detail & Related papers  (2020-05-27T02:02:57Z)
• Adaptive Teaching of Temporal Logic Formulas to Learners with Preferences [44.63937003271641]
  We investigate machine teaching for temporal logic formulas. An exhaustive search even for a myopic solution takes exponential time. We propose an efficient approach for teaching parametric linear temporal logic formulas.
  arXiv  Detail & Related papers  (2020-01-27T18:22:53Z)
• Understanding the QuickXPlain Algorithm: Simple Explanation and Formal Proof [0.0]
  This paper presents a proof of correctness of Ulrich Junker's QuickXPlain algorithm. It can be used as a guidance for proving other algorithms. It also provides the possibility of providing "gapless" correctness of systems that rely on results computed by QuickXPlain.
  arXiv  Detail & Related papers  (2020-01-07T01:37:41Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.