VEL: A Formally Verified Reasoner for OWL2 EL Profile

• URL: http://arxiv.org/abs/2412.08739v1
• Date: Wed, 11 Dec 2024 19:17:28 GMT
• Title: VEL: A Formally Verified Reasoner for OWL2 EL Profile
• Authors: Atalay Mert Ileri, Nalen Rangarajan, Jack Cannell, Hande McGinty,
• Abstract summary: VEL is a formal verified EL++ reasoner equipped with machine-checkable correctness proofs. Our work demonstrates the necessity of mechanization of reasoning algorithms to ensure their correctness at theoretical and implementation levels.
• Score: 0.0
• License:
• Abstract: Over the past two decades, the Web Ontology Language (OWL) has been instrumental in advancing the development of ontologies and knowledge graphs, providing a structured framework that enhances the semantic integration of data. However, the reliability of deductive reasoning within these systems remains challenging, as evidenced by inconsistencies among popular reasoners in recent competitions. This evidence underscores the limitations of current testing-based methodologies, particularly in high-stakes domains such as healthcare. To mitigate these issues, in this paper, we have developed VEL, a formally verified EL++ reasoner equipped with machine-checkable correctness proofs that ensure the validity of outputs across all possible inputs. This formalization, based on the algorithm of Baader et al., has been transformed into executable OCaml code using the Coq proof assistant's extraction capabilities. Our formalization revealed several errors in the original completeness proofs, which led to changes to the algorithm to ensure its completeness. Our work demonstrates the necessity of mechanization of reasoning algorithms to ensure their correctness at theoretical and implementation levels.

Related papers

• From Scientific Texts to Verifiable Code: Automating the Process with Transformers [2.536225150399618]
  transformers can read research papers that propose algorithms with formal proofs and translate these proofs into verifiable code. We argue that this approach can significantly reduce the barrier to formal verification.
  arXiv  Detail & Related papers  (2025-01-09T14:03:35Z)
• 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)
• Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects [1.6727186769396274]
  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.
  arXiv  Detail & Related papers  (2024-09-13T22:25:58Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARD is a framework that masters uniform synthesis of theorem and proof data of high quality and diversity. We present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points. We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data.
  arXiv  Detail & Related papers  (2024-02-14T05:57:58Z)
• Lyra: Orchestrating Dual Correction in Automated Theorem Proving [63.115422781158934]
  Lyra is a new framework that employs two distinct correction mechanisms: Tool Correction and Conjecture Correction. Tool Correction contributes to mitigating hallucinations, thereby improving the overall accuracy of the proof. Conjecture Correction refines generation with instruction but does not collect paired (generation, error & refinement) prompts.
  arXiv  Detail & Related papers  (2023-09-27T17:29:41Z)
• Verify-and-Edit: A Knowledge-Enhanced Chain-of-Thought Framework [26.7264686036634]
  Large language models (LLMs) have become the norm in NLP, demonstrating good performance in generation and reasoning tasks. One of its most fatal disadvantages is the lack of factual correctness. Generating unfactual texts not only leads to lower performances but also degrades the trust and validity of their applications.
  arXiv  Detail & Related papers  (2023-05-05T03:49:14Z)
• Validation Diagnostics for SBI algorithms based on Normalizing Flows [55.41644538483948]
  This work proposes easy to interpret validation diagnostics for multi-dimensional conditional (posterior) density estimators based on NF. It also offers theoretical guarantees based on results of local consistency. This work should help the design of better specified models or drive the development of novel SBI-algorithms.
  arXiv  Detail & Related papers  (2022-11-17T15:48:06Z)
• A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm [9.349616752756024]
  We present the first formally certified end-to-end implementation of Shor's prime factorization algorithm. By leveraging our framework, one can significantly reduce the effects of human errors.
  arXiv  Detail & Related papers  (2022-04-14T17:02:34Z)
• 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)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  We propose a transformer-based model that answers binary questions over rule-bases and generates the corresponding proofs. Our model learns to predict nodes and edges corresponding to proof graphs in an efficient constrained training paradigm. We conduct experiments on synthetic, hand-authored, and human-paraphrased rule-bases to show promising results for QA and proof generation.
  arXiv  Detail & Related papers  (2020-10-06T15:47: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.