Fast Koopman Surrogate Falsification Using Linear Relaxations and Weights

Recent work demonstrated that using Koopman surrogate models to falsify black-box models against signal temporal logic specifications is highly effective. However, the bottleneck of this approach arises from the mixed-integer linear program optimization used to synthesize the falsifying trajectory. The complexity of mixed-integer linear programming can be prohibitive, increasing exponentially with the number of binary variables. In this work, we introduce a new weighted robustness encoding that eliminates the need for binary variables. We also propose a new weighting scheme for Koopman operator linearization that aims to compensate for inaccuracies in the learned model. We evaluate our approach using a set of benchmarks from the ARCH falsification competition. Our weighting methods significantly improve computational efficiency and reduce the number of simulations needed to find falsifying traces.