Research

Propagating sets, not points

Testing a neural network means feeding it one input at a time and checking each answer. Verification asks a stronger question: what can the network output for every input in a set? The set might be every version of an image within a small change in brightness, or every state a drone could be in at take-off. Instead of sampling from that set, we push the whole set through the network, layer by layer, and look at the set of outputs it can produce.

Each linear layer maps a set to another set exactly and cheaply. The difficulty is the nonlinear activation functions, such as ReLU, which bend and fold the set as it passes through.

Exact or over-approximate?

An exact method splits the set wherever an activation can switch on or off, so the output is a union of pieces that matches exactly what the network can produce. It is sound and complete: if it reports a violation, a real counterexample exists. The price is that the number of pieces can grow exponentially with the size of the network.

An over-approximate method keeps a single convex set at each layer that is guaranteed to contain every reachable output. It scales far better and is still sound: if the over-approximation avoids the unsafe outputs, so does the network. If the two overlap, the answer is “unknown”, and the set can be split to tighten it. Tools such as NNV and n2v represent these sets as star sets, which support both kinds of analysis [1, 2].

What can be guaranteed

Once we have the output set, a property is a question about that set:

• Robustness: every perturbed version of an image receives the same label.
• Safety of a control loop: a neural network controller, run together with the system it controls, never drives the system out of its safe region. The output set of one step becomes the input set of the next [3].
• New architectures: the same questions for graph neural networks [4] and mixture-of-experts models [5].

For very large models, or inputs such as video and 3D scans, even over-approximation can be too slow. Probabilistic verification then gives a guarantee that holds with a chosen high probability, computed from samples of the network’s behaviour; learning the shape of the reachable set makes these guarantees much tighter [6, 1]. The same idea of checking a model’s output against a formal description also lets us catch and correct mistakes in the reasoning of AI systems [7].

Classical verification starts from a mathematical model of the system. Real systems rarely come with an accurate one, but we can usually observe them. I work on two different routes from data to a formal guarantee, and they give different kinds of answer.

Route 1: the scenario approach

Treat each observation, such as a recorded trajectory or a measured disturbance, as a scenario, and write it as a constraint. Then solve a convex optimisation problem that satisfies every scenario. Scenario theory, developed by Campi and Garatti, bounds the chance that the solution is violated by a new, unseen scenario: with confidence at least 1−β, the probability of violation is at most ε. The bound depends only on the number of samples and on how many of them shaped the solution. It needs no assumption about the probability distribution the data came from.

I have used this to estimate how fast the trajectories of an unknown system can spread apart, which is enough to build a finite abstraction and synthesise a controller for temporal logic specifications [1]. Scen-Opt makes the scenario approach available as a toolbox and web app for linear, quadratic and semidefinite programs [2].

Route 2: Willems’ fundamental lemma

For linear systems, and some classes of polynomial ones, a single trajectory can contain everything there is to know about the system, provided the input was varied enough. This condition is called persistence of excitation and is checked with a rank test on the recorded data. When it holds, every other trajectory of the system is a combination of the recorded one, so the unknown model can be replaced by matrices of data.

The data matrices can then be placed directly into a sum-of-squares program that searches for a control Lyapunov function (for stability) or a control barrier certificate (for safety), together with the controller that enforces it. Unlike the scenario approach, the resulting guarantee is deterministic. TRUST automates this for four classes of systems from one input-state trajectory [3]. I have extended the idea to neural network barrier certificates verified with SMT solvers [4], and to systems with algebraic constraints, where the data alone is not rich enough until it is collected in the right subspace; this enables a user to hand control safely to an autonomous controller once enough data has been gathered [5].

Which route when?

When a system is affected by noise, such as wind on a drone or demand on a power grid, no controller can promise that every run is safe. The right question becomes a probability: what is the probability that the system stays safe, or reaches its target while avoiding danger? I lead two tools that answer this question in different ways.

Abstraction: IMPaCT

The first approach divides the continuous state space into a finite grid of cells. For every cell and control input, we compute an interval that contains the probability of moving to each other cell. The result is an interval Markov decision process, a finite model that is guaranteed to contain the behaviour of the real system. An algorithm called interval iteration then computes lower and upper bounds on the probability of satisfying the specification, together with a controller that achieves the lower bound.

Abstraction handles rich specifications such as safety, reachability and reach-while-avoid, but the number of cells grows exponentially with the dimension of the system. IMPaCT tackles this by building the abstraction in parallel on CPUs and GPUs [1]. Abstractions can also be learned from data, with a quantified error, using Gaussian processes [2].

Barrier certificates: PRoTECT

The second approach avoids the grid altogether. A barrier certificate is a function over the state space that is low on the initial states, high on the unsafe states, and does not grow too quickly in expectation as the system evolves. Finding such a function proves an upper bound on the probability of ever reaching the unsafe states within a time horizon, without simulating a single run. For polynomial systems, the search for a barrier certificate becomes a sum-of-squares optimisation problem.

PRoTECT searches over several polynomial degrees in parallel and covers discrete- and continuous-time systems, both stochastic and deterministic [3]. Barrier certificates scale better with dimension than a grid, at the cost of more conservative probability bounds and a focus on safety. Both tools take part in the stochastic category of the ARCH-COMP verification competition [4].

Certified flight through a doorway

A control barrier function acts as a safety filter: it watches the commands sent to a robot and changes them only when needed to keep the robot inside a certified safe set. In a cluttered indoor space a single barrier function struggles. To cover two rooms joined by a narrow doorway it must be either so cautious that little of either room counts as safe, or so loose that its guarantee fails exactly where the space pinches.

Our approach instead covers the free space with a union of many small neural control barrier functions, each verified on its own, and certifies which handovers between them are safe. The handovers form a graph, and a mission is a path through it. Each check is exact: it either proves a piece safe or returns a concrete state where it fails, never an inconclusive answer. The same analysis says, before any training, whether a passage is simply too narrow for any such union to carry the drone through it [1].

On the drone, safety is enforced at run time in layers. A tracker steers towards the next waypoint; a supervisor keeps track of which safe region the drone is in and when it may hand over to the next; and the filter adjusts each command so the drone stays inside the active region. If no region can safely be held or entered, the supervisor stops the drone rather than guessing, and it ends the mission only if that stop lasts more than ten seconds. The drone’s position comes from visual markers around the lab, fused with its own motion sensors, and the estimate grows less certain the longer the drone goes without seeing a marker.

Across flights through the doorway and around a structural column, no logged state left the certified set while the filter was running. With the filter removed, the drone left the set and was logged outside it at more than a hundred locations. Staying inside the safe set is something the filter guarantees, not something the unfiltered controller sometimes manages [1].

Verifying behaviour trees

Behaviour trees are a popular way to program what a robot does. Small actions and conditions are arranged in a tree, and sequence and fallback nodes decide which one runs next. Trees are easy to build and reuse, but mistakes can hide in how the pieces interact, for example a fallback that is never reached or two branches that fight over the same actuator.

BehaVerify translates a behaviour tree into a model that a model checker can explore exhaustively, so properties such as “the robot always returns to base when the battery is low” are proved for every possible run. Decisions made by neural networks can be included, and the same specification generates the code that runs on the robot, so the verified model and the deployed behaviour cannot drift apart [2]. We are now extending this to teams of robots whose trees must be composed safely [3].

Safety under physical constraints

Robot arms and many physical systems are described by equations with algebraic constraints, such as links that must stay connected. I helped develop the first method to synthesise control barrier functions for these systems, demonstrated on a three-link manipulator [4].