Philip Torr, Harkirat Singh Behl, M Pawan Kumar, Rudy Bunel, Alessandro De Palma, Singh Behl, M Pawan
We lifted 3 functions out of this paper's own repositories and ran 2 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 |
|---|---|---|
| oval-group/oval-bab | — | 2 of 3 |
| Function | Status | Where it lives |
|---|---|---|
| adjust_artificial_caps_k | Ran | oval-group/oval-bab/plnn/explp_solver/saddle_anderson_optimization.py code served (permissive licence) · get_code("21bd468d83740981") |
| gradlike_step_size | Ran | oval-group/oval-bab/plnn/explp_solver/saddle_anderson_optimization.py code served (permissive licence) · get_code("832d315ada04c647") |
| spfw_block_k_step | Not yet run | oval-group/oval-bab/plnn/explp_solver/saddle_anderson_optimization.py code served (permissive licence) · get_code("5c397352736e64f3") |
Some links come from the archived Papers with Code dataset (CC BY-SA 4.0): attribution and licence.
Tight and efficient neural network bounding is crucial to the scaling of neural network verification systems. Many efficient bounding algorithms have been presented recently, but they are often too loose to verify more challenging properties. This is due to the weakness of the employed relaxation, which is usually a linear program of size linear in the number of neurons. While a tighter linear relaxation for piecewise-linear activations exists, it comes at the cost of exponentially many constraints and currently lacks an efficient customized solver. We alleviate this deficiency by presenting two novel dual algorithms: one operates a subgradient method on a small active set of dual variables, the other exploits the sparsity of Frank-Wolfe type optimizers to incur only a linear memory cost. Both methods recover the strengths of the new relaxation: tightness and a linear separation oracle. At the same time, they share the benefits of previous dual approaches for weaker relaxations: massive parallelism, GPU implementation, low cost per iteration and valid bounds at any time. As a consequence, we can obtain better bounds than off-the-shelf solvers in only a fraction of their running time, attaining significant formal verification speed-ups.
The same record, over MCP at https://syntology.ai/mcp:
get_harvested_code_for_paper("2101.05844")
get_code_for_paper("2101.05844")
have("2101.05844")
Connect an agent — have() is free.