yizhake / cegarette_nn Public

Notifications You must be signed in to change notification settings
Fork 0
Star 0

Tighter Abstract Queries in CEGAR-based Neural Network Verification

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 3 Commits
acasxu		acasxu
experiments_common_and_utils		experiments_common_and_utils
mnist		mnist
redesign		redesign
LICENSE		LICENSE
README.md		README.md
main.py		main.py
remove_maraboupy_from_env.sh		remove_maraboupy_from_env.sh
requirements.txt		requirements.txt
setup_maraboupy_to_env.sh		setup_maraboupy_to_env.sh

Repository files navigation

CEGARETE_NN

The Repository contains the implementation of the paper Tighter Abstract Queries in Neural Network Verification by Elazar Coher, Yizhak Yisrael Elboher, Clark Barrett and Guy Katz.

Quick start

MNIST

python main.py \
  --method "abstraction_refinement" \
  --output-path "./experiments/temp_experiment" \
  --property "./mnist/model2/file_properties/180_minst_property_image_5.py" \
  --network-path "tf" "./mnist/model2/model_without_softmax" \
  --abstraction-strategy "complete_right_to_left" \
  --abstraction-args "" \
  --refinement-strategy "by_max_loss" \
  --refinement-args "1"  \
  --update-property "Marabou" \
  --refine-until-not-satisfying