lcss21.md

nn_partition

This code is based on ideas from the following paper:

• Michael Everett, Golnaz Habibi, Jonathan P. How, "Robustness Analysis of Neural Networks via Efficient Partitioning with Applications in Control Systems", IEEE LCSS 2020 & ACC 2021.

About

We introduce the concepts of Analyzer, Propagator, and Partitioner in our LCSS/ACC '21 paper and implement several instances of each concept as a starting point. This modular view on NN robustness analysis essentially defines an API that decouples each component. This decoupling enables improvements in either Propagator or Partitioner algorithms to have a wide impact across many analysis/verification problems.

Reproduce Figures from LCSS/ACC 2021 Paper

Figure 4

Figure 4a (Lower Bounds):

python -m nn_partition.example \
	--partitioner GreedySimGuided \
	--propagator CROWN_LIRPA \
	--term_type time_budget \
	--term_val 2 \
	--interior_condition lower_bnds \
	--model random_weights \
	--activation relu \
	--show_input --show_output

Figure 4b (Linf Ball):

python -m nn_partition.example \
	--partitioner GreedySimGuided \
	--propagator CROWN_LIRPA \
	--term_type time_budget \
	--term_val 2 \
	--interior_condition linf \
	--model random_weights \
	--activation relu \
	--show_input --show_output

Figure 4c (Convex Hull):

python -m nn_partition.example \
	--partitioner GreedySimGuided \
	--propagator CROWN_LIRPA \
	--term_type time_budget \
	--term_val 2 \
	--interior_condition convex_hull \
	--model random_weights \
	--activation relu \
	--show_input --show_output

Fig 4a	Fig 4b	Fig 4c
Lower Bounds	Linf Ball	Convex Hull

Figure 5

Figure 5a (SG+IBP):

python -m nn_partition.example \
	--partitioner SimGuided \
	--propagator IBP_LIRPA \
	--term_type time_budget \
	--term_val 2 \
	--interior_condition convex_hull \
	--model random_weights \
	--activation relu \
	--input_plot_labels None None \
	--show_input --skip_show_output \
	--input_plot_aspect equal

Figure 5b (SG+CROWN):

python -m nn_partition.example \
	--partitioner SimGuided \
	--propagator CROWN_LIRPA \
	--term_type time_budget \
	--term_val 2 \
	--interior_condition convex_hull \
	--model random_weights \
	--activation relu \
	--input_plot_labels None None \
	--show_input --skip_show_output \
	--input_plot_aspect equal

Figure 5c (GSG+CROWN):

python -m nn_partition.example \
	--partitioner GreedySimGuided \
	--propagator CROWN_LIRPA \
	--term_type time_budget \
	--term_val 2 \
	--interior_condition convex_hull \
	--model random_weights \
	--activation relu \
	--input_plot_labels None None \
	--show_input --skip_show_output \
	--input_plot_aspect equal

Figure 5d (GSG+CROWN):

python -m nn_partition.example \
	--partitioner AdaptiveGreedySimGuided \
	--propagator CROWN_LIRPA \
	--term_type time_budget \
	--term_val 2 \
	--interior_condition convex_hull \
	--model random_weights \
	--activation relu \
	--input_plot_labels None None \
	--show_input --skip_show_output \
	--input_plot_aspect equal

Fig 5a	Fig 5b	Fig 5c	Fig 5d
SG+IBP	SG+CROWN	GSG+IBP	GSG+CROWN

Figure 6

Figure 6a (SG+IBP):

python -m nn_partition.example \
	--partitioner SimGuided \
	--propagator IBP_LIRPA \
	--term_type time_budget \
	--term_val 2 \
	--interior_condition convex_hull \
	--model robot_arm \
	--activation tanh \
	--output_plot_labels x y \
	--output_plot_aspect equal \
	--skip_show_input

Figure 6b (AGSG+CROWN):

python -m nn_partition.example \
	--partitioner AdaptiveGreedySimGuided \
	--propagator CROWN_LIRPA \
	--term_type time_budget \
	--term_val 2 \
	--interior_condition convex_hull \
	--model robot_arm \
	--activation tanh \
	--output_plot_labels x y \
	--output_plot_aspect equal \
	--skip_show_input

Fig 6a	Fig 6b
SG+IBP	AGSG+CROWN

Figure 7

This figure unfortunately requires code for the RL implementation that is under IP protection from our research sponsor.

Figure 8

Info coming soon...

Animations

For any of the above examples, you can add the --make_animation flag which will save a .gif in results/animations/, e.g.,

python -m nn_partition.example \
	--partitioner GreedySimGuided \
	--propagator CROWN_LIRPA \
	--term_type time_budget \
	--term_val 5 \
	--interior_condition lower_bnds \
	--model random_weights \
	--activation relu \
	--show_input --show_output \
	--make_animation

will produce something like this: