aai-institute/veriflow

Normalizing flows for neuro-symbolic AI

Veriflow: Generative Flow Based Density Estimators for Neuro-Symbolic Verification

VeriFlow provides a stable and convenient library of flow based general purpose density models with flexibile base distributions, which are specifically tailored towards the use in neuro-symbolic verification procedures. The major goal is to provide models that can represent reference distributions which are suitable for satisfiability based approaches, abstract interpretation, and hypothesis testing simultaneously. The implemented layer are carefully designed to guarntee the following properties:

• Efficient computation of exact densities as well as efficient sampling.
• A piece-wise affine log-density function for all models with (leaky-)ReLU nonlinearity and Laplacian base distribution.
• UDL preserving layers map the upper density level sets of the data distribution to the upper density level sets of the base Distribution.
• Direct onnx export of log_prob and sampling methods.

Installation

1. Clone Project:

git clone [email protected]:aai-institute/VeriFlow.git

2. Install poetry

curl -sSL https://install.python-poetry.org | python3 -

3. Finally, within the veriflow project directory:

poetry install

Experiments

Veriflow comes with a lightweigt experimentation library that allow effortless configuaration, e.g. of hyperparameter optimzation experiments via yaml config files. Additionally, we define several benchmarking experiments.

Run an experiment

Within the projects script folder you'll find a a script called run_experiment.py. You can use it to conduct an experiment from the a config file.

poetry run python run_experiment.py --config <config file> --report_dir <log dir>

veriflow's Issues

Fix pipelines

ONNX export

Implement convenience function for onnx support

Remove hardcoded base distributions in HyperOptExperiment

Improve Testing

VeriFlow

• linalg
• networks
• transforms
• flows
  • Onnx export

ExpLib

• config_parser
• base
• hyperopt
• datasets

HyperoptExperiment with NiceFlow on mps

Problem

HyperoptExperiment fails with NiceFlow on mps devices.

Analysis

• Verified for permutation == "half"
• Error: Permutations seem to be not on device?!?
• works with NiceMaskedConvFlow

Improve REAMDE.md

• Implementation based on pyro
• Installation
• Getting started
• Layers

Implement LU-layers

Implement LU layers as non url preserving layers

Onnx export with LU transform not supported

Description

Calling to_onnx on a flow with LU layers raises a NotImplementedError. Reason is that the function linalg_inv is not implemented in onnx

Suggestion

A possible workaround could be to export a surrogate model with precomputed inverse matrix instead.

Implement Additive Autoregressive Layer

Implement a layer that replaces additive coupling with additive autoregression.

Create Build Docs Pipeline

Outdated experiment configs

Several experiment configs are outdated and cannot be run currently.

Missing import in explib/base.py

deepcopy import missing

Implement Test Pipeline

Basic MNIST Experiment with training once with all flow architectures

Rename Library

Rename to veriflow

Proper list handling of config parser

Proper handling of lists with atomic types during recursion

Refactor documentation

Problem

• Some of the code documentation is outdated/incomplete/inconsistent format

Todos

VeriFlow

• linalg
• networks
• transforms
• flows

ExpLib

• config_parser
• base
• hyperopt
• datasets

Improve Data Preprocessing

• Simple configuration in yaml
  • Downscaling
  • Reshaping
  • Dequantization
• Remove any hardcoded downscaling

HyperOptExperiment: improve evaluation

• Final evaluation of best model on test set.
• Options for visualizing intermediate results, e.g. plotting samples.
• Improve final reporting