  Specifications play a crucial role in neural network verification. They
define the precise input regions we aim to verify, typically represented as
L-infinity norm balls. While recent research suggests using neural activation
patterns (NAPs) as specifications for verifying unseen test set data, it
focuses on computing the most refined NAPs, often limited to very small regions
in the input space. In this paper, we study the following problem: Given a
neural network, find a minimal (coarsest) NAP that is sufficient for formal
verification of the network's robustness. Finding the minimal NAP specification
not only expands verifiable bounds but also provides insights into which
neurons contribute to the model's robustness. To address this problem, we
propose several exact and approximate approaches. Our exact approaches leverage
the verification tool to find minimal NAP specifications in either a
deterministic or statistical manner. Whereas the approximate methods
efficiently estimate minimal NAPs using adversarial examples and local
gradients, without making calls to the verification tool. This allows us to
inspect potential causal links between neurons and the robustness of
state-of-the-art neural networks, a task for which existing verification
frameworks fail to scale. Our experimental results suggest that minimal NAP
specifications require much smaller fractions of neurons compared to the most
refined NAP specifications, yet they can significantly expand the verifiable
boundaries to several orders of magnitude larger.
