More Like this

1. Training for Verification: Increasing Neuron Stability to Scale DNN Verification

   https://doi.org/10.1007/978-3-031-57256-2_2  

   Xu, Dong; Mozumder, Nusrat J; Duong, Hai; Dwyer, Matthew B (April 2024, 30th International Conference Tools and Algorithms for the Construction and Analysis of Systems)

   Finkbeiner, Bernd; Kovacs, Laura (Ed.)

   With the growing use of deep neural networks(DNN) in mis- sion and safety-critical applications, there is an increasing interest in DNN verification. Unfortunately, increasingly complex network struc- tures, non-linear behavior, and high-dimensional input spaces combine to make DNN verification computationally challenging. Despite tremen- dous advances, DNN verifiers are still challenged to scale to large ver- ification problems. In this work, we explore how the number of stable neurons under the precondition of a specification gives rise to verifica- tion complexity. We examine prior work on the problem, adapt it, and develop several novel approaches to increase stability. We demonstrate that neuron stability can be increased substantially without compromis- ing model accuracy and this yields a multi-fold improvement in DNN verifier performance. 

   more » « less
2. Relational Network Verification

   https://doi.org/10.1145/3651890.3672238  

   Xu, Xieyang; Yuan, Yifei; Kincaid, Zachary; Krishnamurthy, Arvind; Mahajan, Ratul; Walker, David; Zhai, Ennan (August 2024, ACM)

   Relational network verification is a new approach for validating network changes. In contrast to traditional network verification, which analyzes specifications for a single network snapshot, it analyzes specifications that capture similarities and differences between two network snapshots (e.g., pre- and post-change snapshots). Relational specifications are compact and precise because they focus on the flows and paths that change between snapshots and then simply mandate that all other network behaviors "stay the same", without enumerating them. To achieve similar guarantees, single-snapshot specifications would need to enumerate all flow and path behaviors that are not expected to change in order to enable checking that nothing has accidentally changed. Such specifications are proportional to network size, which makes them impractical to generate for many real-world networks. We demonstrate the value of relational reasoning by developing Rela, a high-level relational specification language and verification tool for network changes. Rela compiles input specifications and network snapshot representations to finite state automata, and it then verifies compliance by checking automaton equivalence. Our experiments using data from a global backbone with over 103 routers find that Rela specifications need fewer than 10 terms for 93% of the complex, high-risk changes. Rela validates 80% of the changes within 20 minutes. 

   more » « less
3. Value Alignment Verification

   Brown, Daniel; Schneider, Jordan; Dragan, Anca; Niekum, Scott (January 2021, 38th International Conference on Machine Learning)

   As humans interact with autonomous agents to perform increasingly complicated, potentially risky tasks, it is important to be able to efficiently evaluate an agent’s performance and correctness. In this paper we formalize and theoretically analyze the problem of efficient value alignment verification: how to efficiently test whether the behavior of another agent is aligned with a human’s values. The goal is to construct a kind of “driver’s test” that a human can give to any agent which will verify value alignment via a minimal number of queries. We study alignment verification problems with both idealized humans that have an explicit reward function as well as problems where they have implicit values. We analyze verification of exact value alignment for rational agents and propose and analyze heuristic and approximate value alignment verification tests in a wide range of gridworlds and a continuous autonomous driving domain. Finally, we prove that there exist sufficient conditions such that we can verify exact and approximate alignment across an infinite set of test environments via a constant- query-complexity alignment test. 

   more » « less
4. Value Alignment Verification

   Brown, Daniel S; Schneider, Jordan; Dragan, Anca; Niekum, Scott (July 2021, International Conference on Machine Learning)

   null (Ed.)
5. From Simulation to Runtime Verification and Back: Connecting Single-Run Verification Techniques

   https://doi.org/10.23919/SpringSim.2019.8732915  

   Rozier, Kristin Yvonne (April 2019, Proceedings of the Spring Simulation Conference (SpringSim))