LTL Verification of Memoryful Neural Agents

TL;DR

This work introduces the first framework for verifying full $LTL_{\mathbb{R}}$ specifications of Memoryful Neural Multi-Agent Systems under uncertainty, bridging formal methods with memoryful neural policies. It develops a bounded verification pipeline with decidability results and two solving techniques, Bound Propagation Through Time and Recursive MILP, augmented by adaptive splitting to scale to memoryful agents. For unbounded specifications, it combines Bounded-Path Model Checking, lasso search, and inductive invariant synthesis to achieve sound and complete results in applicable cases, despite general undecidability. Empirically, the approach yields order-of-magnitude improvements over state-of-the-art methods on Gymnasium and PettingZoo benchmarks and demonstrates verification of both time-bounded and unbounded properties for single- and multi-agent settings, enabling rigorous safety guarantees for MN-MAS.

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.

Figures (2)

• Figure 1: A simple RNN, consisting of a feed-forward first layer $\bm{y} = \mathop{\mathrm{ReLU}}\nolimits(\bm{\omega}_1\bm{x})$, which maps the input $\bm{x}=\left(x_1x_2\right)$ to $\bm{y}=\left(y_1y_2\right)$ via left multiplication by $\bm{\omega}_1=\left(-1111\right)$. The last layer is recurrent and is defined as $z^{\langle t \rangle} = \mathop{\mathrm{ReLU}}\nolimits(\bm{\omega}_2\bm{y} + z^{\langle t-1 \rangle})$, where $\bm{\omega}_2=\left(1-1\right)$ and $z$ is the output variable with $z^{\langle 0 \rangle} = 0$. The superscript $^{\langle t \rangle}$ denotes indicates the time step and is omitted when there is no ambiguity (e.g., here, we have omitted it for $x_1, x_2, y_1$ and $y_2$, as they are not used in other time steps).
• Figure 2: The base-2 logarithm of runtimes (seconds) for verifying $\xi_t$ and $\chi_t$ using BPMC. All instances are verified using RMILP. Symbols ${\color{green!80!blue!70!black} \bullet}$ and ${\color{red!70!black}\mathsf{x}}$ denote that the algorithm returned True and False, respectively.

Theorems & Definitions (19)

• Definition 1
• Definition 2: Memoryful Neural Multi-Agent System
• Remark 1
• Definition 3: MN-MAS path
• Definition 4: Specifications
• Remark 2
• Definition 5: Satisfaction
• Definition 6: Verification Problem
• Lemma 1
• Lemma 2