LTL Verification of Memoryful Neural Agents

• URL: http://arxiv.org/abs/2503.02512v1
• Date: Tue, 04 Mar 2025 11:20:19 GMT
• Title: LTL Verification of Memoryful Neural Agents
• Authors: Mehran Hosseini, Alessio Lomuscio, Nicola Paoletti,
• Abstract summary: We present a framework for verifying Memoryful Neural Multi-Agent Systems (MN-MAS) against full Linear Temporal Logic (LTL) specifications.<n>Examples of MN-MAS include multi-agent systems based on feed-forward and recurrent neural networks or state-space models.
• Score: 16.353043979615496
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present a framework for verifying Memoryful Neural Multi-Agent Systems (MN-MAS) against full Linear Temporal Logic (LTL) specifications. In MN-MAS, agents interact with a non-deterministic, partially observable environment. Examples of MN-MAS include multi-agent systems based on feed-forward and recurrent neural networks or state-space models. Different from previous approaches, we support the verification of both bounded and unbounded LTL specifications. We leverage well-established bounded model checking techniques, including lasso search and invariant synthesis, to reduce the verification problem to that of constraint solving. To solve these constraints, we develop efficient methods based on bound propagation, mixed-integer linear programming, and adaptive splitting. We evaluate the effectiveness of our algorithms in single and multi-agent environments from the Gymnasium and PettingZoo libraries, verifying unbounded specifications for the first time and improving the verification time for bounded specifications by an order of magnitude compared to the SoA.

Related papers

• A Learned Proximal Alternating Minimization Algorithm and Its Induced Network for a Class of Two-block Nonconvex and Nonsmooth Optimization [4.975853671529418]
  This work proposes a general learned alternating minimization algorithm, LPAM, for solving learnable two-block nonsmooth problems. The proposed LPAM-net is parameter-efficient and has favourable performance in comparison with some state-of-the-art methods.
  arXiv  Detail & Related papers  (2024-11-10T02:02:32Z)
• Collision Avoidance Verification of Multiagent Systems with Learned Policies [9.550601011551024]
  This paper presents a backward reachability-based approach for verifying the collision avoidance properties of Multi-Agent Feedback Loops (MA-NFLs) We account for many uncertainties, making it well aligned with real-world scenarios. We demonstrate the proposed algorithm can verify collision-free properties of a MA-NFL with agents trained to imitate a collision avoidance algorithm.
  arXiv  Detail & Related papers  (2024-03-05T20:36:26Z)
• Amortizing intractable inference in large language models [56.92471123778389]
  We use amortized Bayesian inference to sample from intractable posterior distributions. We empirically demonstrate that this distribution-matching paradigm of LLM fine-tuning can serve as an effective alternative to maximum-likelihood training. As an important application, we interpret chain-of-thought reasoning as a latent variable modeling problem.
  arXiv  Detail & Related papers  (2023-10-06T16:36:08Z)
• Optimization Guarantees of Unfolded ISTA and ADMM Networks With Smooth Soft-Thresholding [57.71603937699949]
  We study optimization guarantees, i.e., achieving near-zero training loss with the increase in the number of learning epochs. We show that the threshold on the number of training samples increases with the increase in the network width.
  arXiv  Detail & Related papers  (2023-09-12T13:03:47Z)
• Learning Prompt-Enhanced Context Features for Weakly-Supervised Video Anomaly Detection [37.99031842449251]
  Video anomaly detection under weak supervision presents significant challenges. We present a weakly supervised anomaly detection framework that focuses on efficient context modeling and enhanced semantic discriminability. Our approach significantly improves the detection accuracy of certain anomaly sub-classes, underscoring its practical value and efficacy.
  arXiv  Detail & Related papers  (2023-06-26T06:45:16Z)
• Symmetric Tensor Networks for Generative Modeling and Constrained Combinatorial Optimization [72.41480594026815]
  Constrained optimization problems abound in industry, from portfolio optimization to logistics. One of the major roadblocks in solving these problems is the presence of non-trivial hard constraints which limit the valid search space. In this work, we encode arbitrary integer-valued equality constraints of the form Ax=b, directly into U(1) symmetric networks (TNs) and leverage their applicability as quantum-inspired generative models.
  arXiv  Detail & Related papers  (2022-11-16T18:59:54Z)
• Verifying Quantized Neural Networks using SMT-Based Model Checking [2.38142799291692]
  We develop and evaluate a symbolic verification framework using incremental model checking (IMC) and satisfiability modulo theories (SMT) We can provide guarantees on the safe behavior of ANNs implemented both in floating-point and fixed-point arithmetic. For small- to medium-sized ANNs, our approach completes most of its verification runs in minutes.
  arXiv  Detail & Related papers  (2021-06-10T18:27:45Z)
• Neural Network-based Control for Multi-Agent Systems from Spatio-Temporal Specifications [0.757024681220677]
  We use Spatio-Temporal Reach and Escape Logic (STREL) as a specification language. We map control synthesis problems with STREL specifications to propose a combination of gradient and gradient-based methods to solve such problems. We develop a machine learning technique that uses the results of the off-line optimizations to train a neural network that gives the control inputs current states.
  arXiv  Detail & Related papers  (2021-04-06T18:08:09Z)
• Incremental Verification of Fixed-Point Implementations of Neural Networks [0.19573380763700707]
  We develop and evaluate a novel symbolic verification framework using incremental bounded model checking (BMC), satisfiability modulo theories (SMT), and invariant inference. Our approach was able to verify and produce examples for 85.8% of 21 test cases considering different input images, and 100% of the properties related to covering methods.
  arXiv  Detail & Related papers  (2020-12-21T10:03:44Z)
• Adaptive Subcarrier, Parameter, and Power Allocation for Partitioned Edge Learning Over Broadband Channels [69.18343801164741]
  partitioned edge learning (PARTEL) implements parameter-server training, a well known distributed learning method, in wireless network. We consider the case of deep neural network (DNN) models which can be trained using PARTEL by introducing some auxiliary variables.
  arXiv  Detail & Related papers  (2020-10-08T15:27:50Z)
• Statistical control for spatio-temporal MEG/EEG source imaging with desparsified multi-task Lasso [102.84915019938413]
  Non-invasive techniques like magnetoencephalography (MEG) or electroencephalography (EEG) offer promise of non-invasive techniques. The problem of source localization, or source imaging, poses however a high-dimensional statistical inference challenge. We propose an ensemble of desparsified multi-task Lasso (ecd-MTLasso) to deal with this problem.
  arXiv  Detail & Related papers  (2020-09-29T21:17:16Z)
• Communication-Efficient Distributed Stochastic AUC Maximization with Deep Neural Networks [50.42141893913188]
  We study a distributed variable for large-scale AUC for a neural network as with a deep neural network. Our model requires a much less number of communication rounds and still a number of communication rounds in theory. Our experiments on several datasets show the effectiveness of our theory and also confirm our theory.
  arXiv  Detail & Related papers  (2020-05-05T18:08:23Z)

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.