Finding Safety Violations of AI-Enabled Control Systems through the Lens of Synthesized Proxy Programs

TL;DR

Synthify addresses safety testing for AI-enabled control systems by combining two core ideas: synthesizing a lightweight proxy program that mimics a DRL controller and using an ε-greedy strategy to select sub-specifications for falsification, followed by a simulated-annealing search to find safety violations. The proxy enables efficient falsification, while the ε-greedy sampling improves coverage of conjunctive STL specifications, with refinement to reduce spurious results. Empirical results on 8 public control systems show Synthify achieves up to 100% falsification success and 7.8x more violations within the same time budget, along with substantial improvements in sub-specification coverage compared to PSY-TaLiRo. The work demonstrates practical gains in both effectiveness and efficiency for testing end-to-end AI-enabled control systems and outlines pathways to extend the approach to higher-dimensional inputs and integration with other safety analyses.

Abstract

Given the increasing adoption of modern AI-enabled control systems, ensuring their safety and reliability has become a critical task in software testing. One prevalent approach to testing control systems is falsification, which aims to find an input signal that causes the control system to violate a formal safety specification using optimization algorithms. However, applying falsification to AI-enabled control systems poses two significant challenges: (1)~it requires the system to execute numerous candidate test inputs, which can be time-consuming, particularly for systems with AI models that have many parameters, and (2)~multiple safety requirements are typically defined as a conjunctive specification, which is difficult for existing falsification approaches to comprehensively cover. This paper introduces Synthify, a falsification framework tailored for AI-enabled control systems. Our approach performs falsification in a two-phase process. At the start, Synthify synthesizes a program that implements one or a few linear controllers to serve as a proxy for the AI controller. This proxy program mimics the AI controller's functionality but is computationally more efficient. Then, Synthify employs the $ε$-greedy strategy to sample a promising sub-specification from the conjunctive safety specification. It then uses a Simulated Annealing-based falsification algorithm to find violations of the sampled sub-specification for the control system. To evaluate Synthify, we compare it to PSY-TaLiRo, a state-of-the-art and industrial-strength falsification tool, on 8 publicly available control systems. On average, Synthify achieves a 83.5% higher success rate in falsification compared to PSY-TaLiRo with the same budget of falsification trials. The safety violations found by Synthify are also more diverse than those found by PSY-TaLiRo, covering 137.7% more sub-specifications.

Figures (3)

• Figure 1: Architecture of an AI-enabled control system.
• Figure 2: An example of self-driving control system.
• Figure 3: Overview of Synthify.