search

dlshriver / dnnf

Deep Neural Network Falsification
https://dnnf.readthedocs.io/
MIT License
7 stars 4 forks source link

Running ACAS-Xu benchmark in a container created from your dnnf image #15

Closed shenw000 closed 1 year ago

shenw000 commented 1 year ago

First I was able to run the DNNF-GHPR benchmark in a container created from your dnnf image. So I think that my setup for running container is correct.

However, when I run the ACAS-Xu benchmark in the same container, it simply can't finish for several days. The command that I tested is dnnf properties/property_1.py --network N onnx/N_1_1.onnx --backend cleverhans.projected_gradien_descent

The output of the ACAS-Xu benchmark run of above command is below: Falsifying: Forall(x, ((([[ 0.6 -0.5 -0.5 0.45 -0.5 ]] <= x) & (x <= [[ 0.68 0.5 0.5 0.5 -0.45]])) ==> (N(x)[(0, 0)] <= 3.991125645861615)))

Network N: Input_0 : Input([1 5], dtype=float32) Gemm_0 : Gemm(Input_0, ndarray(shape=(50, 5)), ndarray(shape=(50,)), transpose_a=0, transpose_b=1, alpha=1.000000, beta=1.000000) Relu_0 : Relu(Gemm_0) Gemm_1 : Gemm(Relu_0, ndarray(shape=(50, 50)), ndarray(shape=(50,)), transpose_a=0, transpose_b=1, alpha=1.000000, beta=1.000000) Relu_1 : Relu(Gemm_1) Gemm_2 : Gemm(Relu_1, ndarray(shape=(50, 50)), ndarray(shape=(50,)), transpose_a=0, transpose_b=1, alpha=1.000000, beta=1.000000) Relu_2 : Relu(Gemm_2) Gemm_3 : Gemm(Relu_2, ndarray(shape=(50, 50)), ndarray(shape=(50,)), transpose_a=0, transpose_b=1, alpha=1.000000, beta=1.000000) Relu_3 : Relu(Gemm_3) Gemm_4 : Gemm(Relu_3, ndarray(shape=(50, 50)), ndarray(shape=(50,)), transpose_a=0, transpose_b=1, alpha=1.000000, beta=1.000000) Relu_4 : Relu(Gemm_4) Gemm_5 : Gemm(Relu_4, ndarray(shape=(50, 50)), ndarray(shape=(50,)), transpose_a=0, transpose_b=1, alpha=1.000000, beta=1.000000) Relu_5 : Relu(Gemm_5) Gemm_6 : Gemm(Relu_5, ndarray(shape=(5, 50)), ndarray(shape=(5,)), transpose_a=0, transpose_b=1, alpha=1.000000, beta=1.000000)

Can you provide some suggestions and directions about solve this problem?

Your help is greatly appreciated.

dlshriver commented 1 year ago

That property is probably not falsifiable, so pgd will just run forever. Dnnf cannot prove that a property is true. You can specify a maximum number of retries with the --n_starts option if you want dnnf to stop. Or you can use an external tool to kill dnnf after a certain amount of time has passed.