One2One vs One2Any Property Generators in VERONA: Targeted vs Untargeted Verification

One2OnePropertyGenerator creates targeted verification specifications that check if a specific target class can outrank the original class, while One2AnyPropertyGenerator creates untargeted specifications that check if any other class can outrank the original.

VERONA is a neural network verification framework that generates VNN-Lib specifications to test how input perturbations affect classification outcomes. The difference between One2One and One2Any property generators in VERONA determines whether you are testing for a specific adversarial target or evaluating general model robustness against any possible misclassification.

Core Concepts: Targeted vs Untargeted Robustness

Neural network verification distinguishes between two attack paradigms. Targeted verification asks: "Can we force the network to classify this input as a specific class?" Untargeted verification asks: "Can we force the network to classify this input as anything other than the correct class?"

These paradigms map directly to VERONA's generator classes. One2OnePropertyGenerator implements targeted verification by encoding a single target class constraint. One2AnyPropertyGenerator implements untargeted verification by encoding disjunctive constraints over all non-original classes.

One2OnePropertyGenerator: Targeted Verification

The One2OnePropertyGenerator class in ada_verona/verification_module/property_generator/one2one_property_generator.py creates specifications that test whether a neural network can be forced to misclassify an input into a specific target class.

Constructor and Parameters

The generator requires a specific target class at initialization:

from ada_verona.verification_module.property_generator.one2one_property_generator import One2OnePropertyGenerator

generator = One2OnePropertyGenerator(
    target_class=1,        # The specific class we want to force

    number_classes=10,     # Total number of output classes

    data_lb=0.0,          # Lower bound for input data

    data_ub=1.0           # Upper bound for input data

)

Output Constraint Generation

In one2one_property_generator.py (lines 81-83), the generator creates a single output constraint asserting that the target class score must be greater than or equal to the original class score:

# From one2one_property_generator.py, lines 81-83

output_constraints = [
    f"(assert (or (and (>= Y_{self.target_class} Y_{original_class}))))"
]

This generates a VNN-Lib specification with a single disjunct. The verifier searches for any perturbation within the epsilon ball that makes Y_target ≥ Y_original, effectively forcing a specific misclassification.

One2AnyPropertyGenerator: Untargeted Verification

The One2AnyPropertyGenerator class in ada_verona/verification_module/property_generator/one2any_property_generator.py creates specifications that test whether a neural network can be forced to misclassify an input into any class other than the original.

Constructor and Parameters

Unlike the targeted variant, this generator does not require a specific target class:

from ada_verona.verification_module.property_generator.one2any_property_generator import One2AnyPropertyGenerator

generator = One2AnyPropertyGenerator(
    number_classes=10,     # Total number of output classes

    data_lb=0.0,          # Lower bound for input data

    data_ub=1.0           # Upper bound for input data

)

Output Constraint Generation

In one2any_property_generator.py (lines 79-84), the generator loops over all classes except the original class and creates a disjunctive constraint for each:

# From one2any_property_generator.py, lines 79-84

output_constraints = []
for i in range(self.number_classes):
    if i != original_class:
        output_constraints.append(
            f"(assert (or (and (>= Y_{i} Y_{original_class}))))"
        )

This generates a VNN-Lib specification with multiple disjuncts. The verifier searches for any perturbation that makes any Y_i ≥ Y_original where i is not the original class.

Key Differences at a Glance

Feature	One2OnePropertyGenerator	One2AnyPropertyGenerator
Verification Type	Targeted	Untargeted
Required Parameter	target_class	None
Output Constraints	Single clause: Y_target ≥ Y_original	Multiple clauses: Y_i ≥ Y_original for all i ≠ original
VNN-Lib Structure	One disjunct in assert (or ...)	Multiple disjuncts in assert (or ...)
Result Dictionary	{"target_class": <int>}	{} (empty)
Use Case	Testing specific adversarial targets	Testing general robustness

Practical Code Examples

The following example demonstrates how to instantiate both generators and inspect their generated VNN-Lib specifications:

import numpy as np
from ada_verona.verification_module.property_generator.one2one_property_generator import (
    One2OnePropertyGenerator,
)
from ada_verona.verification_module.property_generator.one2any_property_generator import (
    One2AnyPropertyGenerator,
)

# Toy image (flattened) and its true class

image = np.array([0.5, 0.5, 0.5])
true_class = 0
epsilon = 0.1

# ---- Targeted (One2One) ----

targeted_gen = One2OnePropertyGenerator(
    target_class=1, number_classes=10, data_lb=0, data_ub=1
)
targeted_prop = targeted_gen.create_vnnlib_property(image, true_class, epsilon)

print("One2One property name:", targeted_prop.name)
print("One2One VNN-Lib snippet:")
print("\n".join(targeted_prop.content.splitlines()[:12]))
print("Epsilon result dict:", targeted_gen.get_dict_for_epsilon_result())

# ---- Untargeted (One2Any) ----

untargeted_gen = One2AnyPropertyGenerator(number_classes=10, data_lb=0, data_ub=1)
untargeted_prop = untargeted_gen.create_vnnlib_property(image, true_class, epsilon)

print("\nOne2Any property name:", untargeted_prop.name)
print("One2Any VNN-Lib snippet:")
print("\n".join(untargeted_prop.content.splitlines()[:12]))
print("Epsilon result dict:", untargeted_gen.get_dict_for_epsilon_result())

Expected output highlights:

One2One property name: property_0_0_1
One2One VNN-Lib snippet:
; Spec for image and epsilon 0.10000
; Definition of input variables
(declare-const X_0 Real)
...
(assert (or
    (and (>= Y_1 Y_0))
))
Epsilon result dict: {'target_class': 1}

One2Any property name: property_0_0_1
One2Any VNN-Lib snippet:
; Spec for image and epsilon 0.10000
; Definition of input variables
(declare-const X_0 Real)
...
(assert (or
    (and (>= Y_1 Y_0))
    (and (>= Y_2 Y_0))
    ...
))
Epsilon result dict: {}

Summary

• One2OnePropertyGenerator implements targeted verification by generating VNN-Lib specifications that test whether a specific target class can achieve a higher score than the original class.
• One2AnyPropertyGenerator implements untargeted verification by generating specifications that test whether any class other than the original can achieve a higher score.
• Both generators inherit from the abstract PropertyGenerator base class in ada_verona/verification_module/property_generator/property_generator.py and share the same API for creating VNN-Lib properties.
• The targeted generator requires a target_class parameter and returns {"target_class": <int>} from get_dict_for_epsilon_result(), while the untargeted generator accepts no target class and returns an empty dictionary.

Frequently Asked Questions

What is the main difference between One2One and One2Any property generators?

The main difference lies in the verification objective. One2OnePropertyGenerator creates targeted specifications that check if a neural network can be forced to classify an input as a specific target class, while One2AnyPropertyGenerator creates untargeted specifications that check if the network can be forced to classify an input as any class other than the original. This distinction determines whether the generated VNN-Lib file contains a single output constraint or multiple disjunctive constraints.

When should I use One2OnePropertyGenerator over One2AnyPropertyGenerator?

Use One2OnePropertyGenerator when you need to evaluate targeted adversarial attacks or when you want to verify robustness against misclassification into a specific class. This is common in security applications where an attacker aims to force a specific incorrect label, such as making a stop sign classifier label it as a speed limit sign. Use One2AnyPropertyGenerator when measuring general model robustness or when any misclassification constitutes a failure, regardless of which incorrect class is chosen.

How do the VNN-Lib specifications differ between these generators?

The VNN-Lib specifications differ in the output assertion block. One2OnePropertyGenerator generates a single disjunct asserting that the target class score is greater than or equal to the original class score: (assert (or (and (>= Y_target Y_original)))). One2AnyPropertyGenerator generates multiple disjuncts, one for each class except the original: (assert (or (and (>= Y_1 Y_0)) (and (>= Y_2 Y_0)) ...)). This structural difference reflects the targeted versus untargeted verification semantics.

Which generator is more computationally expensive for neural network verification?

One2OnePropertyGenerator is generally more computationally expensive for the underlying solver because it imposes a stricter constraint: the verifier must find a perturbation that forces the network to classify the input as a specific target class. One2AnyPropertyGenerator is typically easier to satisfy because the verifier can choose any alternative class that is easiest to activate, providing more flexibility in the search space. However, the actual runtime depends on the network architecture and the difficulty of reaching specific output classes.

{
  "mcpServers": {
    "instagit": {
      "command": "npx",
      "args": ["-y", "instagit@latest"]
    }
  }
}