abstractNN 0.1.3

Formal verification of neural networks using abstract interpretation and affine arithmetic

AbstractNN

AbstractNN is a Python library for formal verification of neural networks using abstract interpretation and affine arithmetic. It provides mathematically sound guarantees about network behavior under input perturbations.

🎯 Key Features

• Sound Verification: Mathematically proven bounds on network outputs
• Affine Arithmetic: Symbolic tracking of input-output dependencies
• Multiple Relaxations: Linear, interval, and hybrid relaxation strategies
• ONNX Support: Works with models exported from PyTorch, TensorFlow, etc.
• Partial Evaluation: Efficient verification of network sub-regions
• Soundness Checking: Monte Carlo validation of formal bounds
• Production Ready: Well-tested, documented, and type-hinted

📦 Installation

From PyPI (recommended)

pip install abstractnn

From source

git clone https://github.com/guillaume117/abstractNN.git
cd abstractNN
pip install -e .

# Download pre-trained models
chmod +x scripts/download_models.sh
./scripts/download_models.sh

🚀 Quick Start

Basic Verification

from abstractnn import AffineEngine, BoundPropagator, ONNXParser

# Load your ONNX model
parser = ONNXParser('model.onnx')
layers = parser.parse()

# Create verification engine
engine = AffineEngine()
propagator = BoundPropagator(engine)

# Define perturbed input
import numpy as np
image = np.random.rand(3, 28, 28).astype(np.float32)
noise_level = 0.1  # L∞ perturbation radius

# Create symbolic expressions
input_exprs = engine.create_input_expressions(image, noise_level)

# Propagate through network
output_exprs = propagator.propagate(input_exprs, layers, image.shape)

# Get guaranteed output bounds
bounds = [expr.get_bounds() for expr in output_exprs]
print(f"Output bounds: [{bounds[0][0]:.4f}, {bounds[0][1]:.4f}]")

VGG16 Partial Verification

from abstractnn import verify_partial_soundness

# Verify first 5 layers of VGG16
result = verify_partial_soundness(
    model_path='vgg16.onnx',
    image=test_image,
    noise_level=0.01,
    num_layers=5,
    num_mc_samples=100
)

if result['success']:
    print(f"Sound: {result['soundness_report']['is_sound']}")
    print(f"Coverage: {result['soundness_report']['coverage_ratio']*100:.1f}%")

Command Line Interface

# Verify a model (soundness checking)
abstractnn-verify --model model.onnx --image test.npy --epsilon 0.01

# Formal evaluation with affine arithmetic (default FMNIST example)
abstractnn-eval

# Custom evaluation
abstractnn-eval --model custom.onnx --image test.png --noise 0.1 --output results.json

# With detailed report
abstractnn-eval --detailed-report --export-report-csv report.csv

# Get library info
abstractnn-info

⚠️ Large Model Files

Note: Pre-trained model files (like VGG16) are NOT included in the repository due to their large size (500+ MB).

To download models:

# Option 1: Use download script
./scripts/download_models.sh

# Option 2: Models will be automatically downloaded when running tests
python -m pytest tests/test_vgg16_formal.py

The models will be saved to the models/ directory.

🎯 Use Cases

1. Soundness Verification (abstractnn-verify)

Verify that formal bounds are sound by comparing with Monte Carlo sampling:

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

2. Formal Evaluation (abstractnn-eval)

Compute guaranteed output bounds for all classes:

# Use default FMNIST example
abstractnn-eval

# Custom model and image
abstractnn-eval \
    --model mymodel.onnx \
    --image myimage.png \
    --noise 0.05 \
    --output results.json \
    --detailed-report

📚 Documentation

Full documentation is available at abstractnn.readthedocs.io

• Installation Guide
• Quick Start Tutorial
• CLI Reference
• API Reference
• Examples

🧪 Running Tests

# Run all tests
pytest tests/ -v

# Run with coverage
pytest tests/ --cov=abstractnn --cov-report=html

# Run specific test
pytest tests/test_affine_engine.py -v

🏗️ Architecture

abstractNN/
├── abstractnn/           # Main package
│   ├── __init__.py
│   ├── affine_engine.py  # Affine expression management
│   ├── bound_propagator.py  # Layer-by-layer propagation
│   ├── relaxer.py        # Non-linear relaxations
│   ├── onnx_parser.py    # ONNX model parsing
│   ├── partial_evaluator.py  # Partial network evaluation
│   ├── soundness_checker.py  # Soundness validation
│   └── cli.py            # Command-line interface
├── tests/                # Test suite
├── docs/                 # Sphinx documentation
├── examples/             # Usage examples
└── scripts/              # Utility scripts
```## 🔬 Research & CitationsIf you use abstractNN in your research, please cite:```cite@software{abstractnn2025,  title={abstractNN: Formal Verification of Neural Networks using Abstract Interpretation},  author={Berthelot, Guillaume},  year={2025},  url={https://github.com/guillaume117/abstractNN},  version={0.1.0}}```

## 🤝 Contributing
Contributions are welcome! Please see CONTRIBUTING.md for guidelines.

```bash
# Setup development environment
git clone https://github.com/guillaume117/abstractNN.git
cd abstractNN

pip install -e .[dev]# Run testspytest tests/# Format codeblack abstractnn/ tests/isort abstractnn/ tests/# Type checkingmypy abstractnn/

📊 Comparison with Other Tools

Method	Soundness	Tightness	Scalability	Speed
Monte Carlo	❌ No	N/A	✅ High	✅ Fast
MILP	✅ Yes	✅ Exact	❌ Low	❌ Slow
Interval	✅ Yes	❌ Loose	✅ High	✅ Fast
AbstractNN	✅ Yes	❌ Loose	⚠️ Medium	⚠️ Medium