Efficient Verification of Neural Networks Against LVM-Based Specifications
The deployment of perception systems based on neural networks in safety critical applications requires assurance on their robustness. Deterministic guarantees on network robustness require formal verification. Standard approaches for verifying robustness analyse invariance to analytically defined transformations, but not the diverse and ubiquitous changes involving object pose, scene viewpoint, occlusions, etc. To this end, we present an efficient approach for verifying specifications definable using Latent Variable Models that capture such diverse changes. The approach involves adding an invertible encoding head to the network to be verified, enabling the verification of latent space sets with minimal reconstruction overhead. We report verification experiments for three classes of proposed latent space specifications, each capturing different types of realistic input variations. Differently from previous work in this area, the proposed approach is relatively independent of input dimensionality and scales to a broad class of deep networks and real-world datasets by mitigating the inefficiency and decoder expressivity dependence in the present state-of-the-art.
Code (0)
등록된 구현이 없습니다.
Tasks
DecoderSimilar Papers 제목 키워드 기반
Verification and Validation of Semantic Annotations
In this paper, we propose a framework to perform verification and validation of semantically annotated data. The annotations, extracted from websites, are verified against the schema.org vocabulary and Domain Specificati…
LTL Verification of Memoryful Neural Agents
We present a framework for verifying Memoryful Neural Multi-Agent Systems (MN-MAS) against full Linear Temporal Logic (LTL) specifications. In MN-MAS, agents interact with a non-deterministic, partially observable enviro…
State Space ModelsJoint Verification and Refinement of Language Models for Safety-Constrained Planning
Although pre-trained language models can generate executable plans (e.g., programmatic policies) for solving robot tasks, the generated plans may violate task-relevant logical specifications due to the models' black-box …
Language ModelingLanguage ModellingVerification of Hyperproperties for Uncertain Dynamical Systems via Barrier Certificates
Hyperproperties are system properties that require quantification over multiple execution traces of a system. Hyperproperties can express several specifications of interest for cyber-physical systems--such as opacity, ro…
On the Complexity of Rational Verification
Rational verification refers to the problem of checking which temporal logic properties hold of a concurrent multiagent system, under the assumption that agents in the system choose strategies that form a game-theoretic …