Benchmark

We will discuss the 2022 ARCH-COMP AINNCS benchmarks here. We plan to mostly reuse the 2021 benchmarks, which were also mostly used in the 2020 edition.

2021 benchmarks:

https://github.com/verivital/ARCH-COMP2021

2021 report "ARCH-COMP21 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants":

https://easychair.org/publications/paper/Jq4h

In this froup we discuss how to organize the automatic evaluation of benchmarks. This allows us to run all benchmarks on the same machine so that we can perform the repeatability evaluation and the collection of computation times in one go.

We'd like to propose a benchmark with linear dynamics. We consider a robot in a structured environment of polytypic obstacles, and we'd like to identify its safe regions of operation within the environment, given a trained NN.

Paper: https://dl.acm.org/doi/pdf/10.1145/3302504.3311802

Code: https://github.com/rcpsl/ReluVerify

The property is that the network should be monotonically negative for insulin inputs. (eg hold all insulin inputs constant with input range 0-0.1, hold a glucose trace constant (given the below criteria)), and as you increase insulin in one location, the predicted output should decrease. Glucose values are allowed to vary [40,400], with a max difference of 25 between two consecutive inputs eg: G(t) vs G(t-5). These networks all take $7$ glucose inputs G(t), G(t-5), ... , G(t-30) and $7$ insulin inputs u(t), .., u(t-30).

We test our tool ReachNN on the benchmarks that have the same dynamics as the benchmarks proposed in Sherlock, but with different settings of neural-network (NN) controllers. The main difference lies on the NN controller, where the NN controller we use may have different activation functions simultaneously, e.g. we have ReLU+sigmoid NN controller for Ex. \#1. The input dimension of the NN controller, which is the dimension of the system state, ranges from 2 to 4.