Command Line Interface

abstractNN provides three command-line tools for neural network verification and evaluation.

Overview

# Soundness verification
abstractnn-verify --model model.onnx --image test.npy --epsilon 0.01

# Formal evaluation
abstractnn-eval --model model.onnx --image test.png --noise 0.05

# Library information
abstractnn-info

abstractnn-verify

Verify neural network soundness by comparing formal bounds with Monte Carlo sampling.

Synopsis

abstractnn-verify [OPTIONS]

Description

This command performs soundness verification by:

1. Computing formal bounds using affine arithmetic

2. Running Monte Carlo sampling with random perturbations

3. Comparing formal bounds with observed values

4. Reporting violations and coverage metrics

Options

-m, --model MODEL

Required. Path to ONNX model file.

-i, --image IMAGE

Required. Path to input image (.npy format).

-e, --epsilon FLOAT

Perturbation radius (L-infinity norm). Default: 0.01

-l, --layers INT

Number of layers to verify. Default: all layers (999)

-s, --samples INT

Monte Carlo samples for soundness checking. Default: 100

-o, --output FILE

Output JSON report file. Optional.

-v, --verbose

Enable verbose output.

--version

Show version and exit.

Examples

Basic verification:

abstractnn-verify --model mnist.onnx --image test.npy --epsilon 0.1

Verify first 5 layers of VGG16:

abstractnn-verify --model vgg16.onnx --image img.npy --epsilon 0.01 --layers 5

With detailed report:

abstractnn-verify \
    --model model.onnx \
    --image data.npy \
    --epsilon 0.05 \
    --output report.json \
    --verbose

Output Format

The command outputs verification results to stdout:

======================================================
VERIFICATION RESULTS
======================================================
Sound: ✅ YES
Coverage: 98.5%
Violations: 15/1000

If --output is specified, a detailed JSON report is saved:

{
  "success": true,
  "soundness_report": {
    "is_sound": true,
    "violation_count": 0,
    "total_outputs": 1000,
    "coverage_ratio": 1.0,
    "violations": [],
    "safety_margins_lower": [...],
    "safety_margins_upper": [...]
  },
  "num_layers": 5,
  "num_outputs": 1000,
  "noise_level": 0.01,
  "num_mc_samples": 100
}

Exit Codes

• 0: Verification successful and sound

• 1: Verification successful but not sound (violations detected)

• 2: Error during verification

abstractnn-eval

Perform formal evaluation using affine arithmetic to compute guaranteed output bounds.

Synopsis

abstractnn-eval [OPTIONS]

Description

This command performs formal evaluation by:

1. Parsing the ONNX model

2. Creating symbolic affine expressions for inputs

3. Propagating expressions through network layers

4. Computing guaranteed bounds for all output classes

5. Identifying robustly classified inputs

Options

-m, --model MODEL

Path to ONNX model file. Default: examples/fmnist_cnn.onnx

-i, --image IMAGE

Path to input image (.png or .npy). Default: examples/fmnist_sample_0_Ankle_boot.png

-n, --epsilon FLOAT

Noise level epsilon. Default: 0.001

-o, --output FILE

Output JSON file. Default: results.json

--device {cpu,gpu}

Device to use. Default: cpu

--detailed-report

Generate detailed propagation report.

--export-report-csv FILE

Export detailed report as CSV.

--version

Show version and exit.

Examples

Use default FMNIST example:

abstractnn-eval

Custom model and image:

abstractnn-eval \
    --model custom_model.onnx \
    --image test.png \
    --epsilon 0.01

With detailed report:

abstractnn-eval \
    --model mymodel.onnx \
    --image myimage.png \
    --epsilon 0.05 \
    --detailed-report \
    --output results.json

Output Format

The command outputs evaluation results to stdout:

==========================================================
EVALUATION RESULTS
==========================================================
Robust class: 5
Execution time: 12.34s
Results saved to: results.json

Bounds per class (sample):
  Class 0: [-2.1543, 1.8765]
  Class 1: [-1.2345, 2.3456]
  Class 2: [-0.9876, 3.4567]
  Class 3: [-1.5432, 2.1098]
  Class 4: [-2.3456, 1.6543]

The JSON output contains:

{
  "bounds_per_class": {
    "0": [-2.1543, 1.8765],
    "1": [-1.2345, 2.3456],
    ...
  },
  "robust_class": 5,
  "intermediate_bounds": [...],
  "execution_time": 12.34,
  "noise_level": 0.05,
  "activation_relaxation": "linear"
}

Activation Relaxation

:

Linear Relaxation (default):

For ReLU when \(l < 0 < u\):

\[\text{ReLU}(x) \in \left[0, u \cdot \frac{x - l}{u - l}\right]\]

abstractnn-info

Display library information and usage help.

Synopsis

abstractnn-info

Description

Displays:

• Library version

• Author information

• Installation instructions

• Quick start guide

• Available commands

• Documentation links

Example Output

abstractNN - Neural Network Formal Verification
================================================

Version: 0.1.0
Author: Guillaume Berthelot
License: MIT

Installation:
  pip install abstractNN

Documentation:
  https://abstractnn.readthedocs.io

GitHub:
  https://github.com/guillaume117/abstractNN

Quick Start:
  from abstractnn import AffineEngine, BoundPropagator, ONNXParser

  parser = ONNXParser('model.onnx')
  layers = parser.parse()

  engine = AffineEngine()
  propagator = BoundPropagator(engine)

  # Verify network...

Available Commands:
  abstractnn-verify  - Verify neural network soundness
  abstractnn-eval    - Formal evaluation with affine arithmetic
  abstractnn-info    - Display library information

For help:
  abstractnn-verify --help
  abstractnn-eval --help

Common Workflows

Workflow 1: Quick Soundness Check

# 1. Verify with small epsilon
abstractnn-verify --model model.onnx --image test.npy --epsilon 0.001

# 2. If sound, increase epsilon
abstractnn-verify --model model.onnx --image test.npy --epsilon 0.01

# 3. Find maximum robust epsilon
for eps in 0.001 0.005 0.01 0.05 0.1; do
    echo "Testing epsilon=$eps"
    abstractnn-verify --model model.onnx --image test.npy --epsilon $eps
done

Workflow 2: Formal Evaluation Pipeline

# 1. Evaluate with default settings
abstractnn-eval --model mymodel.onnx --image test.png

# 2. Generate detailed report
abstractnn-eval \
    --model mymodel.onnx \
    --image test.png \
    --detailed-report \
    --output detailed_results.json

# 3. Try different relaxation strategies
abstractnn-eval \
    --model mymodel.onnx \
    --image test.png \
    --activation-relaxation quadratic

Workflow 3: Batch Processing

#!/bin/bash
# Verify multiple images

for img in images/*.npy; do
    echo "Verifying $img"
    abstractnn-verify \
        --model model.onnx \
        --image "$img" \
        --epsilon 0.01 \
        --output "results/$(basename $img .npy).json"
done

Troubleshooting

Common Issues

Error: “Model file not found”

Ensure the model file exists:

ls -lh model.onnx

Error: “Only .npy format supported”

For abstractnn-verify, convert your image to NumPy format:

import numpy as np
from PIL import Image

img = Image.open('test.png')
img_array = np.array(img, dtype=np.float32) / 255.0
np.save('test.npy', img_array)

Out of Memory

Reduce the number of layers:

abstractnn-verify --model large_model.onnx --image test.npy --layers 5

Or reduce Monte Carlo samples:

abstractnn-verify --model model.onnx --image test.npy --samples 50

Slow Execution

Enable GPU (if available):

abstractnn-eval --model model.onnx --image test.png --device gpu

Use simpler relaxation:

abstractnn-eval --model model.onnx --image test.png --activation-relaxation linear

Performance Tips

1. Start small: Test on a few layers first

2. Use appropriate epsilon: Smaller epsilon = faster

3. Reduce samples: For quick tests, use --samples 10

4. Cache results: Save output with --output to avoid recomputation

See Also

• installation: Installation guide

• Quick Start Guide: Quick start tutorial

• api/modules: API reference

• advanced/troubleshooting: Detailed troubleshooting