paper-with-me

Papers

Verifying Global Neural Network Specifications using Hyperproperties

2023-06-21 · David Boetius, Stefan Leue

Current approaches to neural network verification focus on specifications that target small regions around known input data points, such as local robustness. Thus, using these approaches, we can not obtain guarantees for inputs that are not close to known inputs. Yet, it is highly likely that a neural network will encounter such truly unseen inputs during its application. We study global specifications that - when satisfied - provide guarantees for all potential inputs. We introduce a hyperproperty formalism that allows for expressing global specifications such as monotonicity, Lipschitz continuity, global robustness, and dependency fairness. Our formalism enables verifying global specifications using existing neural network verification approaches by leveraging capabilities for verifying general computational graphs. Thereby, we extend the scope of guarantees that can be provided using existing methods. Recent success in verifying specific global specifications shows that attaining strong guarantees for all potential data points is feasible.

📄 PDF Abstract BibTeX arXiv:2306.12495

Code (0)

등록된 구현이 없습니다.

Tasks

Fairness

Methods 이 논문이 사용한 방법론

Focus 설명 없음

Similar Papers 제목 키워드 기반

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…

Decentralized Planning Using Probabilistic Hyperproperties

2025-02-19 · Francesco Pontiggia, Filip Macák, Roman Andriushchenko, Michele Chiari 외

Multi-agent planning under stochastic dynamics is usually formalised using decentralized (partially observable) Markov decision processes ( MDPs) and reachability or expected reward specifications. In this paper, we prop…

Strategy Logic, Imperfect Information, and Hyperproperties

2025-10-04 · Raven Beutner, Bernd Finkbeiner arxiv

Strategy logic (SL) is a powerful temporal logic that enables first-class reasoning over strategic behavior in multi-agent systems (MAS). In many MASs, the agents (and their strategies) cannot observe the global state of…

Monitoring Second-Order Hyperproperties

2024-04-15 · Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, Niklas Metzger

Hyperproperties express the relationship between multiple executions of a system. This is needed in many AI-related fields, such as knowledge representation and planning, to capture system properties related to knowledge…

On Conformant Planning and Model-Checking of $\exists^*\forall^*$ Hyperproperties

2025-12-29 · Raven Beutner, Bernd Finkbeiner arxiv

We study the connection of two problems within the planning and verification community: Conformant planning and model-checking of hyperproperties. Conformant planning is the task of finding a sequential plan that achieve…