Stateless and Rule-Based Verification For Compliance Checking Applications

• URL: http://arxiv.org/abs/2204.07430v1
• Date: Thu, 14 Apr 2022 17:31:33 GMT
• Title: Stateless and Rule-Based Verification For Compliance Checking Applications
• Abstract summary: We present a formal logic-based framework for creating intelligent compliance checking systems. SARV is a verification framework designed to simplify the overall process of verification for stateless and rule-based verification problems. Based on 300 data experiments, the SARV-based compliance solution outperforms machine learning methods on a 3125-records software quality dataset.
• Score: 1.7403133838762452
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Underlying computational model has an important role in any computation. The state and transition (such as in automata) and rule and value (such as in Lisp and logic programming) are two comparable and counterpart computational models. Both of deductive and model checking verification techniques are relying on a notion of state and as a result, their underlying computational models are state dependent. Some verification problems (such as compliance checking by which an under compliance system is verified against some regulations and rules) have not a strong notion of state nor transition. Behalf of it, these systems have a strong notion of value symbols and declarative rules defined on them. SARV (Stateless And Rule-Based Verification) is a verification framework that designed to simplify the overall process of verification for stateless and rule-based verification problems (e.g. compliance checking). In this paper, a formal logic-based framework for creating intelligent compliance checking systems is presented. We define and introduce this framework, report a case study and present results of an experiment on it. The case study is about protocol compliance checking for smart cities. Using this solution, a Rescue Scenario use case and its compliance checking are sketched and modeled. An automation engine for and a compliance solution with SARV are introduced. Based on 300 data experiments, the SARV-based compliance solution outperforms famous machine learning methods on a 3125-records software quality dataset.

Related papers

• Verification-Aware Training for Speculative Decoding [57.84976863792784]
  We introduce Verification-Aware Training (VAT), a plug-in framework that simulates verification at every training step and turns the resulting accept and reject patterns into supervision.<n>VAT modifies only the training objective, so it can be layered on top of existing methods without changing the draft architecture, the target model, or the inference procedure.<n>VAT improves average acceptance length by up to 11.4% and wall-clock speedup by up to 8.7%, with consistent gains across math, code, and chat benchmarks.
  arXiv  Detail & Related papers  (2026-08-31T01:42:10Z)
• LLM-based Framework for Generating and Verifying Parallel DEVS Statecharts [0.4779196219827507]
  This research introduces an agentic PDEVS-LLM framework to assist human modelers in generating and verifying PDEVS statecharts.<n>A controlled-correction mechanism is developed to verify the logical consistency of the plausible facts.<n>The evaluation of the proposed verification mechanism shows a substantial improvement in the logical consistency of generated statecharts.
  arXiv  Detail & Related papers  (2026-08-15T01:08:39Z)
• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world where they act on persistent operational data.<n>Existing approaches do not provide such system-level guarantees.<n>We study here the verification of agentic systems comprising a single LLM and a tool orchestration harness over relational operational data.
  arXiv  Detail & Related papers  (2026-08-04T13:01:30Z)
• Ontological Knowledge Blocks: Executable Compliance and Profile-Based Validation for Trustworthy AI Systems [0.0]
  This paper introduces Ontological Knowledge Blocks (OKBs), a programmable governance infrastructure that compiles regulatory obligations into machine-checkable constraints.<n>A deterministic regulatory compiler translates structured Intermediate Representation (IR) records into composable KB modules, enabling profile-based governance provenance.<n>Results demonstrate profile-sensitive validation, strictly additive violation accumulation, SHACL validation reconfiguration latency between 12.6 ms and 100.3 ms, and profile equivalence testing confirming Combined as the strictly most comprehensive profile.
  arXiv  Detail & Related papers  (2026-05-22T07:14:31Z)
• MathLedger: A Verifiable Learning Substrate with Ledger-Attested Feedback [0.0]
  Contemporary AI systems achieve extraordinary performance yet remain opaque and non-verifiable.<n>We introduce MathLedger, a substrate for verifiable machine cognition that integrates formal verification, cryptographic attestation, and learning dynamics.<n>The contribution is infrastructural: a working prototype of ledger-attested learning that enables auditability at scale.
  arXiv  Detail & Related papers  (2025-12-22T19:27:55Z)
• Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis [49.31947916567367]
  Hamilton-Jacobi (J) reachability analysis is a popular formal verification tool for general nonlinear systems that can compute optimal reachable under worst-case uncertainties.<n>This work is the first HJ-based reachability-based system verification framework for the Robust Verification Controllers via HJ rover.<n>Within Ro-CoRe, we propose novel methods for safety verification and controller design.
  arXiv  Detail & Related papers  (2025-11-18T18:55:20Z)
• "Show Me You Comply... Without Showing Me Anything": Zero-Knowledge Software Auditing for AI-Enabled Systems [2.2981698355892686]
  This paper introduces ZKMLOps, a novel MLOps verification framework.<n>It operationalizes Zero-Knowledge Proofs (ZKPs)-cryptographic protocols allowing a prover to convince a verifier that a statement is true.<n>We evaluate the framework's practicality through a study of regulatory compliance in financial risk auditing.
  arXiv  Detail & Related papers  (2025-10-30T15:03:32Z)
• Learn, Check, Test -- Security Testing Using Automata Learning and Model Checking [0.0]
  We will investigate a cyber-physical systems as a black box using its external communication interface.<n>We first annotate the model with propositions by mapping context information from the respective protocol to the model.<n>We define generic security properties based on basic security requirements.
  arXiv  Detail & Related papers  (2025-09-26T11:29:53Z)
• Tool-Assisted Conformance Checking to Reference Process Models [0.9117519504551699]
  Conformity checks are crucial to maintain quality and consistency in various processes.<n>This paper explores automated conformance checks for concrete process models against reference models.
  arXiv  Detail & Related papers  (2025-08-01T16:08:24Z)
• Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects [0.0]
  VERIFAI1 aims to investigate automated and semi-automated approaches to bridge this gap.<n>This position paper presents a preliminary synthesis of relevant literature to identify recurring challenges and prospective research directions.
  arXiv  Detail & Related papers  (2025-07-18T19:15:50Z)
• Neural Model Checking [10.376573742987917]
  We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification. Our new approach combines machine learning and symbolic reasoning by using neural networks as formal proof certificates for linear temporal logic. We experimentally demonstrate that our method outperforms the state-of-the-art academic and commercial model checkers on a set of standard hardware designs written in SystemVerilog.
  arXiv  Detail & Related papers  (2024-10-31T10:17:04Z)
• Automatically Adaptive Conformal Risk Control [49.95190019041905]
  We propose a methodology for achieving approximate conditional control of statistical risks by adapting to the difficulty of test samples. Our framework goes beyond traditional conditional risk control based on user-provided conditioning events to the algorithmic, data-driven determination of appropriate function classes for conditioning.
  arXiv  Detail & Related papers  (2024-06-25T08:29:32Z)
• Bisimulation Learning [55.859538562698496]
  We compute finite bisimulations of state transition systems with large, possibly infinite state space. Our technique yields faster verification results than alternative state-of-the-art tools in practice.
  arXiv  Detail & Related papers  (2024-05-24T17:11:27Z)
• OpenFactCheck: Building, Benchmarking Customized Fact-Checking Systems and Evaluating the Factuality of Claims and LLMs [59.836774258359945]
  OpenFactCheck is a framework for building customized automatic fact-checking systems.<n>It allows users to easily customize an automatic fact-checker and verify the factual correctness of documents and claims.<n>CheckerEVAL is a solution for gauging the reliability of automatic fact-checkers' verification results using human-annotated datasets.
  arXiv  Detail & Related papers  (2024-05-09T07:15:19Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  We develop scalable formal verification algorithms without shifting the problem to unrealistic assumptions. In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates. We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope.
  arXiv  Detail & Related papers  (2024-03-15T17:32:02Z)
• Early Verification of Legal Compliance via Bounded Satisfiability Checking [4.304202636346692]
  Metric first-order temporal logic (MFOTL) provides a rich formalism for specifying legal properties. No solution exists for MFOTL-based verification in early-stage system development captured by requirements. We propose a practical, sound, and complete satisfiability checking approach for MFOTL.
  arXiv  Detail & Related papers  (2022-09-08T22:41:40Z)
• Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version) [67.99023219822564]
  We introduce the general framework of relational action bases (RABs) RABs generalize existing models by lifting both restrictions. We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes.
  arXiv  Detail & Related papers  (2022-08-12T17:03:50Z)
• Value-Consistent Representation Learning for Data-Efficient Reinforcement Learning [105.70602423944148]
  We propose a novel method, called value-consistent representation learning (VCR), to learn representations that are directly related to decision-making. Instead of aligning this imagined state with a real state returned by the environment, VCR applies a $Q$-value head on both states and obtains two distributions of action values. It has been demonstrated that our methods achieve new state-of-the-art performance for search-free RL algorithms.
  arXiv  Detail & Related papers  (2022-06-25T03:02:25Z)
• Learning Robust Output Control Barrier Functions from Safe Expert Demonstrations [50.37808220291108]
  This paper addresses learning safe output feedback control laws from partial observations of expert demonstrations. We first propose robust output control barrier functions (ROCBFs) as a means to guarantee safety. We then formulate an optimization problem to learn ROCBFs from expert demonstrations that exhibit safe system behavior.
  arXiv  Detail & Related papers  (2021-11-18T23:21:00Z)
• Complete Agent-driven Model-based System Testing for Autonomous Systems [0.0]
  A novel approach to testing complex autonomous transportation systems is described. It is intended to mitigate some of the most critical problems regarding verification and validation.
  arXiv  Detail & Related papers  (2021-10-25T01:55:24Z)
• Compliance checking in reified IO logic via SHACL [0.0]
  Reified Input/Output (I/O) logic[21] has been recently proposed to model real-world norms in terms of the logic in [11] This paper presents a methodology to carry out compliance checking on reified I/O logic formulae.
  arXiv  Detail & Related papers  (2021-10-13T21:09:47Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  We introduce the CoCoMoT (Computing Conformance Modulo Theories) framework. First, we show how SAT-based encodings studied in the pure control-flow setting can be lifted to our data-aware case. Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering.
  arXiv  Detail & Related papers  (2021-03-18T20:22:50Z)

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.