Giter Club home page Giter Club logo

nnv-rs's Introduction

nnv-rs

Fast reachability analysis and sampling for deep neural networks

Based loosely on the matlab toolbox of a similar name largely developed by Dr. Hoang-Dung Tran. I'm developing this software for my dissertation and I'm happy to support other work using it. If you're using this package or working on similar problems, please let me know by email at equint at cse dot unl dot <educational ending> (sorry, trying to thwart automated mailers).

Build Python package

  1. Install Rust with curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh and re-launch your shell.
  2. Create a Python virtualenv and run pip install -r requirements.txt to install Python requirements.
  3. Clone the following Rust projects ndarray-linalg, numpy, truncnorm-rs
  4. Set the ndarray version in numpy to 15.2.0
  5. Ensure CMake 3.15 or higher is installed as well as clang
  6. Install OpenBlas (apt-get install libopenblas-dev on Ubuntu)
  7. Switch to nightly Rust with rustup default nightly
  8. Build and install the Rust-backed Python package with python ./setup.py install

Benchmarking

When benchmarking, if you want to generate a flamegraph, use the following syntax:

cargo bench --bench my_benchmark -- --profile-time 5

To do

  1. Implement proper bounds checking with DeepPoly
  • Figure out how to run DeepPoly from a star rather than input bounds
  1. Implement constellation importance sampling
  2. Implement neural network argmax

Troubleshooting

  • Build gives linker error /usr/bin/ld: cannot find -lCbcSolver: cbc solver is a default dependency of the good_lp package we're using for linear programming. Fix on Ubuntu is to run sudo apt install coinor-libcbc-dev.
  • If your issue isn't listed here, open an issue on GitHub and we'll see if we can fix/add it.

Acknowledgements

This work is not supported by anybody.

nnv-rs's People

Contributors

drkwint avatar ihowell avatar

Stargazers

avatar

Watchers

avatar avatar avatar

Forkers

placrosse

nnv-rs's Issues

Change output type of Star::get_min to Option<T>

Change output type to Option<T>

nnv-rs/src/star.rs

Lines 305 to 310 in 135fc2d

/// TODO: Change output type to Option<T>
///
/// TODO: ResolutionError::Unbounded can result whether or not the
/// constraints are infeasible if there are zeros in the
/// objective. This needs to be checked either here or in the
/// solve function. Currently this is way too hard to do, so we

This comment was generated by todo based on a TODO comment in 135fc2d in #16. cc @DrKwint.

Originally posted by @todo[bot] in #16 (comment)

!(),

nnv-rs/src/gaussian.rs

Lines 35 to 40 in f4cb763

GaussianDistribution::Gaussian { .. } => todo!(),
}
}
pub fn cdf<R: Rng>(&mut self, n: usize, rng: &mut R) -> T {
match self {

This issue was generated by todo based on a todo comment in f4cb763. It's been assigned to @DrKwint because they committed the code.

Change how StarNodes call DeepPoly

We can make calls to DeepPoly from StarNodes more efficient by caching the bounds from one StarNode and only updating the bounds that are affected by an operation (one dim in the case of a stepReLU)

This should dramatically speed up the inner loop used to decide which StarNodes to expand in a Constellation, though some benchmarking of this is warranted.

## ResolutionError::Unbounded can result whether or not the

ResolutionError::Unbounded can result whether or not the

nnv-rs/src/star.rs

Lines 307 to 312 in 135fc2d

/// TODO: ResolutionError::Unbounded can result whether or not the
/// constraints are infeasible if there are zeros in the
/// objective. This needs to be checked either here or in the
/// solve function. Currently this is way too hard to do, so we
/// panic instead. We have an assumption that we start with a
/// bounded box and therefore should never be unbounded.

This comment was generated by todo based on a TODO comment in 135fc2d in #16. cc @DrKwint.

Originally posted by @todo[bot] in #16 (comment)

ResolutionError::Unbounded does not depend of feasibility of a polytope

star::get_min and star::get_max rely on linear programming. It is assumed that the polytope constraints on the star are feasible, however if they are not feasible then an unbounded error can occur, yielding the minimum/maximum value. This is however incorrect and instead the function should be panicking.

The workaround currently in place is that in test_util the basis array, i.e. the equations being optimized, are not allowed to have coefficients of zero.

StarNode Tree in Graph Computation

Decisions made:

  • Keep a static topological sort of the computation graph for indexing purposes.
  • Use a visitor to compute individual tensors/representations for the expand function in starset
  • We are keeping the tree as branching only for ReLU divergences (on/off)
  • You can use the ancestors of a path in the starset tree to get the representation for a given representation_id
  • StarNodes need to store an index of computation done/to do, i.e. the step relu index
  • In Starset, ReLU nodes create a subtree of StepReLU nodes, so be sure to only take a leaf node as the representation after the ReLU.

Refactor Constellation and StarNode

  • Refactor the Constellation structure
    • Add select_child fn that handles checking feasibility and sampling
    • Update the arena to vector and remove root field, refactor functions appropriately
    • Look into removing input bounds field and passing as method arg instead
    • refactor sample_safe_star
      • Debug uses of fix_infeasible lambda to ensure output is used (in more than one place)
      • Split out the child selection logic
        • Call StarNodeType functions to do feasibility check and sampling
  • #10

Refactor the StarNode structure

  • IxDyn -> generic over star dim
  • Finalize StarNodeType enum
    • Create
  • Create DNNIndex object
  • Rename cdf field to star_cdf
  • Change expand function to check whether node is already expanded
    • Create a new expand fn
    • Add all match cases on StarNodeType
  • DNNIterator has return type StarNodeOperation
    • StarNodeOperation Enumeration refers to Dense, StepRelu, Dropout, which each store the information about the enumeration element.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.