paper-with-me

홈 › Papers

Efficient Verification of Neural Networks Against LVM-Based Specifications

2023-01-01 · CVPR 2023 1 · Harleen Hanspal, Alessio Lomuscio

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.

📄 PDF Abstract BibTeX

Code (0)

등록된 구현이 없습니다.

Tasks

Decoder

Similar Papers 제목 키워드 기반

Verification and Validation of Semantic Annotations

2019-04-02 · Oleksandra Panasiuk, Omar Holzknecht, Umutcan Şimşek, Elias Kärle 외

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

2025-03-04 · Mehran Hosseini, Alessio Lomuscio, Nicola Paoletti

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 Models

Joint Verification and Refinement of Language Models for Safety-Constrained Planning

2024-10-18 · Yunhao Yang, William Ward, Zichao Hu, Joydeep Biswas 외

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 Modelling

Verification of Hyperproperties for Uncertain Dynamical Systems via Barrier Certificates

2021-05-12 · Mahathi Anand, Vishnu Murali, Ashutosh Trivedi, Majid Zamani

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

2022-07-06 · Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, Michael Wooldridge

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 …