Neural Proofs for Sound Verification and Control of Complex Systems

• URL: http://arxiv.org/abs/2512.18389v1
• Date: Sat, 20 Dec 2025 15:01:41 GMT
• Title: Neural Proofs for Sound Verification and Control of Complex Systems
• Authors: Alessandro Abate,
• Abstract summary: This informal contribution presents an ongoing line of research that is pursuing a new approach to the construction of sound proofs.<n>It is possible to generate provably-correct policies/strategies/controllers that, in conjunction with neural certificates, formally attain the given specifications for the models of interest.
• Score: 64.97409769546992
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This informal contribution presents an ongoing line of research that is pursuing a new approach to the construction of sound proofs for the formal verification and control of complex stochastic models of dynamical systems, of reactive programs and, more generally, of models of Cyber-Physical Systems. Neural proofs are made up of two key components: 1) proof rules encode requirements entailing the verification of general temporal specifications over the models of interest; and 2) certificates that discharge such rules, namely they are constructed from said proof rules with an inductive (that is, cyclic, repetitive) approach; this inductive approach involves: 2a) accessing samples from the model's dynamics and accordingly training neural networks, whilst 2b) generalising such networks via SAT-modulo-theory (SMT) queries that leverage the full knowledge of the models. In the context of sequential decision making problems over complex stochastic models, it is possible to additionally generate provably-correct policies/strategies/controllers, namely state-feedback functions that, in conjunction with neural certificates, formally attain the given specifications for the models of interest.

Related papers

• KBQA-R1: Reinforcing Large Language Models for Knowledge Base Question Answering [64.62317305868264]
  We present textbfKBQA-R1, a framework that shifts the paradigm from text imitation to interaction optimization via Reinforcement Learning.<n>Treating KBQA as a multi-turn decision process, our model learns to navigate the knowledge base using a list of actions.<n>Experiments on WebQSP, GrailQA, and GraphQuestions demonstrate that KBQA-R1 achieves state-of-the-art performance.
  arXiv  Detail & Related papers  (2025-12-10T17:45:42Z)
• Learning from Imperfect Data: Robust Inference of Dynamic Systems using Simulation-based Generative Model [4.430997638097218]
  We propose a Simulation-based Generative Model for Imperfect Data (SiGMoID) that enables precise and robust inference for dynamic systems.<n>We demonstrate that SiGMoID quantifies data noise, estimates system parameters, and infers unobserved system components.
  arXiv  Detail & Related papers  (2025-07-15T00:56:21Z)
• System Identification Using Kolmogorov-Arnold Networks: A Case Study on Buck Converters [0.0]
  Kolmogorov-Arnold Networks (KANs) are emerging as a powerful framework for interpretable and efficient system identification.<n>This paper investigates the application of KANs to model and analyze the dynamics of a buck converter system.
  arXiv  Detail & Related papers  (2025-06-12T07:35:30Z)
• Certified Neural Approximations of Nonlinear Dynamics [51.01318247729693]
  In safety-critical contexts, the use of neural approximations requires formal bounds on their closeness to the underlying system.<n>We propose a novel, adaptive, and parallelizable verification method based on certified first-order models.
  arXiv  Detail & Related papers  (2025-05-21T13:22:20Z)
• Fuzzy Recurrent Stochastic Configuration Networks for Industrial Data Analytics [3.8719670789415925]
  This paper presents a novel neuro-fuzzy model, termed fuzzy recurrent configuration networks (F-RSCNs) for industrial data analytics. The proposed F-RSCN is constructed by multiple sub-reservoirs, and each sub-reservoir is associated with a Takagi-Sugeno-Kang (TSK) fuzzy rule. By integrating TSK fuzzy inference systems into RSCNs, F-RSCNs have strong fuzzy inference capability and can achieve sound performance for both learning and generalization.
  arXiv  Detail & Related papers  (2024-07-06T01:40:31Z)
• How neural networks learn to classify chaotic time series [77.34726150561087]
  We study the inner workings of neural networks trained to classify regular-versus-chaotic time series. We find that the relation between input periodicity and activation periodicity is key for the performance of LKCNN models.
  arXiv  Detail & Related papers  (2023-06-04T08:53:27Z)
• Constructing Neural Network-Based Models for Simulating Dynamical Systems [59.0861954179401]
  Data-driven modeling is an alternative paradigm that seeks to learn an approximation of the dynamics of a system using observations of the true system. This paper provides a survey of the different ways to construct models of dynamical systems using neural networks. In addition to the basic overview, we review the related literature and outline the most significant challenges from numerical simulations that this modeling paradigm must overcome.
  arXiv  Detail & Related papers  (2021-11-02T10:51:42Z)
• Improving Coherence and Consistency in Neural Sequence Models with Dual-System, Neuro-Symbolic Reasoning [49.6928533575956]
  We use neural inference to mediate between the neural System 1 and the logical System 2. Results in robust story generation and grounded instruction-following show that this approach can increase the coherence and accuracy of neurally-based generations.
  arXiv  Detail & Related papers  (2021-07-06T17:59:49Z)
• The Role of Isomorphism Classes in Multi-Relational Datasets [6.419762264544509]
  We show that isomorphism leakage overestimates performance in multi-relational inference. We propose isomorphism-aware synthetic benchmarks for model evaluation. We also demonstrate that isomorphism classes can be utilised through a simple prioritisation scheme.
  arXiv  Detail & Related papers  (2020-09-30T12:15:24Z)
• Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models [70.70479436076238]
  We introduce an automated, formal, counterexample-based approach to synthesise Barrier Certificates (BC) The approach is underpinned by an inductive framework, which manipulates a candidate BC structured as a neural network, and a sound verifier, which either certifies the candidate's validity or generates counter-examples. The outcomes show that we can synthesise sound BCs up to two orders of magnitude faster, with in particular a stark speedup on the verification engine.
  arXiv  Detail & Related papers  (2020-07-07T07:39:42Z)

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.