Huan Zhang, Krishnamurthy Dvijotham, Zico Kolter, Suhas Kotha, Christopher Brix
We lifted 6 functions out of this paper's own repositories and ran 0 of them in a sandbox. "Ran" means the function executed on a synthesized input and returned a value. It is not a reproduction of the paper's results.
| Repository | Role | Ran |
|---|---|---|
| kothasuhas/verify-input | canonical | 0 of 6 |
| Function | Status | Where it lives |
|---|---|---|
| _get_relu_state_masks | Not yet run | kothasuhas/verify-input/reproduce_paper/crown/crown.py pointer only (licence: NONE) · get_code("daa5c49fe4662973") |
| get_Omega | Not yet run | kothasuhas/verify-input/reproduce_paper/crown/crown.py pointer only (licence: NONE) · get_code("095d426f7fe1db6d") |
| get_bias_lbs | Not yet run | kothasuhas/verify-input/reproduce_paper/crown/crown.py pointer only (licence: NONE) · get_code("f7bd485aa6a7a27d") |
| get_crown_bounds | Not yet run | kothasuhas/verify-input/reproduce_paper/crown/crown.py pointer only (licence: NONE) · get_code("9a6aff8656d29c80") |
| get_diagonals | Not yet run | kothasuhas/verify-input/reproduce_paper/crown/crown.py pointer only (licence: NONE) · get_code("f9f378e63602dbda") |
| optimize_bound | Not yet run | kothasuhas/verify-input/reproduce_paper/crown/crown.py pointer only (licence: NONE) · get_code("6aa65dbdbffcb257") |
Some links come from the archived Papers with Code dataset (CC BY-SA 4.0): attribution and licence.
Most work on the formal verification of neural networks has focused on bounding the set of outputs that correspond to a given set of inputs (for example, bounded perturbations of a nominal input). However, many use cases of neural network verification require solving the inverse problem, or over-approximating the set of inputs that lead to certain outputs. We present the INVPROP algorithm for verifying properties over the preimage of a linearly constrained output set, which can be combined with branch-and-bound to increase precision. Contrary to other approaches, our efficient algorithm is GPU-accelerated and does not require a linear programming solver. We demonstrate our algorithm for identifying safe control regions for a dynamical system via backward reachability analysis, verifying adversarial robustness, and detecting out-of-distribution inputs to a neural network. Our results show that in certain settings, we find over-approximations over 2500× tighter than prior work while being 2.5× faster. By strengthening robustness verification with output constraints, we consistently verify more properties than the previous state-of-the-art on multiple benchmarks, including a large model with 167k neurons in VNN-COMP 2023. Our algorithm has been incorporated into the α,β-CROWN verifier, available at https://abcrown.org. * Equal contribution, † Equal advising Instructions for reproducing our results are available at https://github.com/kothasuhas/verify-input 37th Conference on Neural Information Processing Systems (NeurIPS 2023).
The same record, over MCP at https://syntology.ai/mcp:
get_harvested_code_for_paper("2302.01404")
get_code_for_paper("2302.01404")
have("2302.01404")
Connect an agent — have() is free.