Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects

• URL: http://arxiv.org/abs/2409.09223v1
• Date: Fri, 13 Sep 2024 22:25:58 GMT
• Title: Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects
• Authors: Nick Feng, Lina Marsso, Marsha Chechik,
• Abstract summary: Satisfiability-based automated reasoning is successfully used in software engineering to validate complex software. We tackle the challenge of validating the correctness of FOL* unsatisfiability results. We develop a proof-based diagnosis to explain the cause of unsatisfiability.
• Score: 1.6727186769396274
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Satisfiability-based automated reasoning is an approach that is being successfully used in software engineering to validate complex software, including for safety-critical systems. Such reasoning underlies many validation activities, from requirements analysis to design consistency to test coverage. While generally effective, the back-end constraint solvers are often complex and inevitably error-prone, which threatens the soundness of their application. Thus, such solvers need to be validated, which includes checking correctness and explaining (un)satisfiability results returned by them. In this work, we consider satisfiability analysis based on First-Order Logic with relational objects (FOL*) which has been shown to be effective for reasoning about time- and data-sensitive early system designs. We tackle the challenge of validating the correctness of FOL* unsatisfiability results and deriving diagnoses to explain the causes of the unsatisfiability. Inspired by the concept of proofs of UNSAT from SAT/SMT solvers, we define a proof format and proof rules to track the solvers' reasoning steps as sequences of derivations towards UNSAT. We also propose an algorithm to verify the correctness of FOL* proofs while filtering unnecessary derivations and develop a proof-based diagnosis to explain the cause of unsatisfiability. We implemented the proposed proof support on top of the state-of-the-art FOL* satisfiability checker to generate proofs of UNSAT and validated our approach by applying the proof-based diagnoses to explain the causes of well-formedness issues of normative requirements of software systems.

Related papers

• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  Large language models (LLMs) struggle with consistent and accurate reasoning. LLMs are trained primarily on correct solutions, reducing their ability to detect and learn from errors. We propose a novel collaborative method integrating Chain-of-Thought (CoT) and Program-of-Thought (PoT) solutions for verification.
  arXiv  Detail & Related papers  (2024-10-05T05:21:48Z)
• SHACL2FOL: An FOL Toolkit for SHACL Decision Problems [0.4895118383237099]
  We introduce SHACL2FOL, the first automatic tool that translates SHACL documents into FOL sentences. The tool computes the answer to the two static analysis problems of satisfiability and containment. It also allow to test the validity of a graph with respect to a set of constraints.
  arXiv  Detail & Related papers  (2024-06-12T09:20:25Z)
• Efficient and Universal Merkle Tree Inclusion Proofs via OR Aggregation [27.541105686358378]
  We propose a novel proof aggregation approach based on OR logic for Merkle tree inclusion proofs. We achieve a proof size independent of the number of leaves in the tree, and verification can be performed using any single valid leaf hash. The proposed techniques have the potential to significantly enhance the scalability, efficiency, and flexibility of zero-knowledge proof systems.
  arXiv  Detail & Related papers  (2024-05-13T17:15:38Z)
• Certified MaxSAT Preprocessing [9.717669529984349]
  MaxSAT has become a viable approach for solving NP-hard optimization problems. ensuring correctness of MaxSAT solvers has remained an important concern. We show how pseudo-Boolean proof logging can be used to certify the correctness of a range of modern MaxSAT preprocessing techniques.
  arXiv  Detail & Related papers  (2024-04-26T10:55:06Z)
• A Closer Look at the Self-Verification Abilities of Large Language Models in Logical Reasoning [73.77088902676306]
  We take a closer look at the self-verification abilities of large language models (LLMs) in the context of logical reasoning. Our main findings suggest that existing LLMs could struggle to identify fallacious reasoning steps accurately and may fall short of guaranteeing the validity of self-verification methods.
  arXiv  Detail & Related papers  (2023-11-14T07:13:10Z)
• 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)
• Comprehensible Counterfactual Explanation on Kolmogorov-Smirnov Test [56.5373227424117]
  We tackle the problem of producing counterfactual explanations for test data failing the Kolmogorov-Smirnov (KS) test. We develop an efficient algorithm MOCHE that avoids enumerating and checking an exponential number of subsets of the test set failing the KS test.
  arXiv  Detail & Related papers  (2020-11-01T06:46:01Z)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  Neural networks can learn complex, non- adversarial functions, and it is challenging to guarantee their correct behavior in safety-critical contexts. Many approaches exist to find failures in networks (e.g., adversarial examples), but these cannot guarantee the absence of failures. We propose an approach that integrates the optimization process into the verification procedure, achieving better performance than the naive approach.
  arXiv  Detail & Related papers  (2020-10-07T08:19:48Z)
• Verification of ML Systems via Reparameterization [6.482926592121413]
  We show how a probabilistic program can be automatically represented in a theorem prover. We also prove that the null model used in a Bayesian hypothesis test satisfies a fairness criterion called demographic parity.
  arXiv  Detail & Related papers  (2020-07-14T02:19:25Z)

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.