Static analysis of ReLU neural networks with tropical polyhedra
summary
This work abstracts ReLU feedforward nets with tropical polyhedra and a zone abstraction to compute tight output ranges, proving concrete claims: it verifies y2>y1 for a two-output example and a robustness bound y1≤0.5, and reconstructs the exact output triangle for a simple net. A prototype implements propagation, unions by tropical convex hulls and refinements by subdivision (four subdivisions yield a convex hull of four extreme points). Nonconvex checks use mixed integer linear programming (Gurobi). Method scales quickly in propagation but double-description explodes beyond ~1,500 neurons.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 0:27Tropical polyhedra
- 0:57Rational functions
- 1:24Tropical arithmetics
- 2:07Tropical half spaces
- 2:56Representation
- 3:54Over Approximation
- 4:28Internal representation
- 5:05Tropical Polydra
- 7:41Simple network
- 8:07Properties
- 9:42Abstractions
- 11:57Proofs
- 12:56Curse of dimensionality
- 13:40Future work
related talks
28mStatic analysis of ReLU neural networks with tropical polyhedra
01h 03mUnderstanding ReLU Networks Through Graph Problems and Polyhedra
18mReLU Hull Approximation
22mFormal Security Analysis of Neural Networks using Symbolic Intervals
20mSupport Triangle Machine
30mComputational Barriers For Learning Some Generalized Linear Models
01h 04mRandomized Embeddings and Neural Networks
28mReduced Products of Abstract Domains for Fairness Certification of Neural Networks