Tools to encode PyTorch modules as Z3 constraints
Lantern: safer than a torch
Lantern is a software package to support SMT analysis of affine multiplexing neural networks using PyTorch and Z3.
See: docs/lantern/ for (generated) documentation.
See: requirements.txt for dependencies.
example.py demonstrates basic usage.
Lantern was developed against
Linear Real Arithmetic appears to be stable, but we have noticed some changes
to the floating point solvers as z3 continues to be developed.
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.