Week #3: MNIST Examples

Summary of contributions

Testing

In this blog I will continue the benchmarking and testing done in Week #2, following the suggestion of the NeuralVerification developers, I began testing the new algorithm Ai2z using the neural networks MNIST from the NeuralVerification repository, these networks are much bigger than the networks tested in the last blog. To run these tests, I had to change the code in NueralVerification a bit, since MaxSens has a bug when partitioning the initial set (Being solved in NeuralVerification#105). The change was the following:

inputs = partition(problem.input, solver.resolution)
Julia

to

inputs = [problem.input]
Julia

with this change, MaxSens won't partition the initial set, so it may lose precision gained when paritioning

Methods to be compared:

  • MaxSens: the only rechability method that would not time out in the used tests, takes hyperrectangles.

    solve(MaxSens(0.6), ...)
    Julia

    0.6 being the resolution of the partition, during the tests this was not used.

  • Ai2z: algorithm implemented based on zonotopes

    solve(Ai2z(), ...)
    Julia

  • Box: algorithm implemented based on hyperrectangles

    solve(Box(), ...)
    Julia

The tests were obtained from https://github.com/sisl/NeuralVerification.jl/blob/master/test/runtime1.jl

For each of them I will be comparing the speed, width of the final layer and the result of given property

using Revise, Suppressor, LazySets, NeuralVerification, Plots, LinearAlgebra
Shift+Enter to run
Julia
Julia 1.4.1

MNIST1 1 dimensional

Input size: 784

1 hidden layer of size: 25

output size: 1

@suppress_err begin
     mnist1 = read_nnet("/home/sguadalupe/.julia/dev/NeuralVerification/examples/networks/mnist1_out1.nnet")
    # entry 23 in MNIST datset
    input_center = [0.0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,121,254,136,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,13,230,253,248,99,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,4,118,253,253,225,42,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,61,253,253,253,74,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,32,206,253,253,186,9,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,211,253,253,239,69,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,254,253,253,133,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,142,255,253,186,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,149,229,254,207,21,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,54,229,253,254,105,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,152,254,254,213,26,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,112,251,253,253,26,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,29,212,253,250,149,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,36,214,253,253,137,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,75,253,253,253,59,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,93,253,253,189,17,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,224,253,253,84,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,43,235,253,126,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,99,248,253,119,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,225,235,49,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]
    output_center = [-1311.1257826380004,4633.767704436501,-654.0718535670002,-1325.349417307,1175.2361184373997,-1897.8607293569007,-470.3405972940001,830.8337987382,-377.7467076115001,572.3674015264198]
    in_epsilon = 1.0 #0-255
    out_epsilon = 10.0 #logit domain
    input_low = input_center .- in_epsilon
    input_high = input_center .+ in_epsilon
    output_low = output_center .- out_epsilon
    output_high = output_center .+ out_epsilon
    inputSet = Hyperrectangle(low=input_low, high=input_high)
    A = Matrix(undef, 2, 1)
    A = [1.0, -1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0 ,0.0]'
    b = [0.0]
    outputSet = HPolytope(A, b)
    out_hyper = Hyperrectangle(low=[-5000.0], high=[-200.0])
    problem_mnist1 = Problem(mnist1, inputSet, out_hyper)
    solver = MaxSens(resolution = 0.6)
    println("MaxSens - problem_mnist1_small")
    timed_result =@timed solve(solver, problem_mnist1)
    println(" - Time: " * string(timed_result[2]) * " s")
    print(" - Output: ")
    println(timed_result[1].status)
    print(" - width of output layer: ")
    println(diameter(overapproximate((timed_result[1].reachable[1]), Hyperrectangle)))
    println("")
    
    solver = Ai2z()
    println("Ai2z - problem_mnist1_small")
    timed_result =@timed solve(solver, problem_mnist1)
    println(" - Time: " * string(timed_result[2]) * " s")
    print(" - Output: ")
    println(timed_result[1].status)
    print(" - width of output layer: ")
    println(diameter(overapproximate((timed_result[1].reachable)[1], Hyperrectangle)))
    println("")
    solver = Box()
    println("Box - problem_mnist1_small")
    timed_result =@timed solve(solver, problem_mnist1)
    println(" - Time: " * string(timed_result[2]) * " s")
    print(" - Output: ")
    println(timed_result[1].status)
    print(" - width of output layer: ")
    println(diameter(overapproximate((timed_result[1].reachable[1]), Hyperrectangle)))
    println("")
end
Shift+Enter to run
Julia
Julia 1.4.1
MaxSens - problem_mnist1_small - Time: 0.000118609 s - Output: holds - width of output layer: 234.37309067640308 Ai2z - problem_mnist1_small - Time: 0.003171489 s - Output: holds - width of output layer: 62.28187921706412 Box - problem_mnist1_small - Time: 5.698e-5 s - Output: holds - width of output layer: 221.43633330929265

MNIST1

Input size: 784

1 hidden layer of size: 25

output size: 10

@suppress_err begin
    mnist1 = read_nnet("/home/sguadalupe/.julia/dev/NeuralVerification/examples/networks/mnist1.nnet")
    input_center = [0.0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,121,254,136,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,13,230,253,248,99,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,4,118,253,253,225,42,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,61,253,253,253,74,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,32,206,253,253,186,9,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,211,253,253,239,69,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,254,253,253,133,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,142,255,253,186,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,149,229,254,207,21,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,54,229,253,254,105,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,152,254,254,213,26,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,112,251,253,253,26,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,29,212,253,250,149,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,36,214,253,253,137,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,75,253,253,253,59,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,93,253,253,189,17,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,224,253,253,84,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,43,235,253,126,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,99,248,253,119,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,225,235,49,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]
    output_center = [-1311.1257826380004,4633.767704436501,-654.0718535670002,-1325.349417307,1175.2361184373997,-1897.8607293569007,-470.3405972940001,830.8337987382,-377.7467076115001,572.3674015264198]
    in_epsilon = 1.0 #0-255
    out_epsilon = 10.0 #logit domain
    input_low = input_center .- in_epsilon
    input_high = input_center .+ in_epsilon
    output_low = output_center .- out_epsilon
    output_high = output_center .+ out_epsilon
    inputSet = Hyperrectangle(low=input_low, high=input_high)
    outputSet = Hyperrectangle(low=output_low, high=output_high)
    problem_mnist = Problem(mnist1, inputSet, outputSet)
    
    
    plot(Projection(outputSet, [1, 2]), label="output Set")
    
    
    solver = MaxSens(resolution = 0.6)
    println("MaxSens - mnist1")
    timed_result =@timed solve(solver, problem_mnist)
    println(" - Time: " * string(timed_result[2]) * " s")
    print(" - Output: ")
    println(timed_result[1].status)
    print(" - width of output layer: ")
    println(diameter(overapproximate((timed_result[1].reachable[1]), Hyperrectangle)))
    println()
    
    plot!(Projection(timed_result[1].reachable[1], [1, 2]), label="MaxSens")
    
    
    solver = Ai2z()
    println("Ai2z - mnist1")
    timed_result =@timed solve(solver, problem_mnist)
    println(" - Time: " * string(timed_result[2]) * " s")
    print(" - Output: ")
    println(timed_result[1].status)
    print(" - width of output layer: ")
    println(diameter(overapproximate((timed_result[1].reachable[1]), Hyperrectangle)))
    println()
    
    plot!(Projection(timed_result[1].reachable[1], [1, 2]), label="Ai2z")
    
    
    solver = Box()
    println("Box - mnist1")
    timed_result =@timed solve(solver, problem_mnist)
    println(" - Time: " * string(timed_result[2]) * " s")
    print(" - Output: ")
    println(timed_result[1].status)
    print(" - width of output layer: ")
    println(diameter(overapproximate((timed_result[1].reachable[1]), Hyperrectangle)))
    plot!(Projection(timed_result[1].reachable[1], [1, 2]), label="Box")
end
Shift+Enter to run
Julia
Julia 1.4.1
MaxSens - mnist1 - Time: 0.000136739 s - Output: violated - width of output layer: 665.394559293125 Ai2z - mnist1 - Time: 0.001370936 s - Output: violated - width of output layer: 228.5702022310056 Box - mnist1 - Time: 0.000102936 s - Output: violated - width of output layer: 634.374095734256

MNIST2

Input size: 784

1 hidden layer of size: 100

output size: 10

@suppress_err begin
    mnist2 = read_nnet("/home/sguadalupe/.julia/dev/NeuralVerification/examples/networks/mnist2.nnet")
    input_center = [0.0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,121,254,136,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,13,230,253,248,99,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,4,118,253,253,225,42,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,61,253,253,253,74,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,32,206,253,253,186,9,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,211,253,253,239,69,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,254,253,253,133,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,142,255,253,186,8,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,149,229,254,207,21,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,54,229,253,254,105,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,152,254,254,213,26,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,112,251,253,253,26,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,29,212,253,250,149,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,36,214,253,253,137,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,75,253,253,253,59,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,93,253,253,189,17,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,224,253,253,84,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,43,235,253,126,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,99,248,253,119,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,225,235,49,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]
    output_center = [-1311.1257826380004,4633.767704436501,-654.0718535670002,-1325.349417307,1175.2361184373997,-1897.8607293569007,-470.3405972940001,830.8337987382,-377.7467076115001,572.3674015264198]
    in_epsilon = 1.0 #0-255
    out_epsilon = 10.0 #logit domain
    input_low = input_center .- in_epsilon
    input_high = input_center .+ in_epsilon
    output_low = output_center .- out_epsilon
    output_high = output_center .+ out_epsilon
    inputSet = Hyperrectangle(low=input_low, high=input_high)
    outputSet = Hyperrectangle(low=output_low, high=output_high)
    problem_mnist = Problem(mnist2, inputSet, outputSet)
    
    
    plot(Projection(outputSet, [1, 2]), label="output Set")
    
    
    solver = MaxSens(resolution = 0.6)
    println("MaxSens - mnist2")
    timed_result =@timed solve(solver, problem_mnist)
    println(" - Time: " * string(timed_result[2]) * " s")
    print(" - Output: ")
    println(timed_result[1].status)
    print(" - width of output layer: ")
    println(diameter(overapproximate((timed_result[1].reachable[1]), Hyperrectangle)))
    println()
    
    plot!(Projection(timed_result[1].reachable[1], [1, 2]), label="MaxSens")
    
    
    solver = Ai2z()
    println("Ai2z - mnist2")
    timed_result =@timed solve(solver, problem_mnist)
    println(" - Time: " * string(timed_result[2]) * " s")
    print(" - Output: ")
    println(timed_result[1].status)
    print(" - width of output layer: ")
    println(diameter(overapproximate((timed_result[1].reachable[1]), Hyperrectangle)))
    
    plot!(Projection(timed_result[1].reachable[1], [1, 2]), label="Ai2z")
    
    
    solver = Box()
    println("Box - mnist2")
    timed_result =@timed solve(solver, problem_mnist)
    println(" - Time: " * string(timed_result[2]) * " s")
    print(" - Output: ")
    println(timed_result[1].status)
    print(" - width of output layer: ")
    println(diameter(overapproximate((timed_result[1].reachable[1]), Hyperrectangle)))
    
    plot!(Projection(timed_result[1].reachable[1], [1, 2]), label="Box")
end
Shift+Enter to run
Julia
Julia 1.4.1
MaxSens - mnist2 - Time: 0.000320499 s - Output: violated - width of output layer: 1281.2267218103152 Ai2z - mnist2 - Time: 0.002087208 s - Output: violated - width of output layer: 302.42543589818916 Box - mnist2 - Time: 0.000342137 s - Output: violated - width of output layer: 1211.7721628585864

ACAS

Input size: 5

6 hidden layer of size: 50

output size: 5

acas_file = "/home/sguadalupe/.julia/dev/NeuralVerification/examples/networks/ACASXU_run2a_4_5_batch_2000.nnet"
acas_nnet = read_nnet(acas_file, last_layer_activation = Id())
A0 = Matrix{Float64}(I, 5, 5)
A1 = -Matrix{Float64}(I, 5, 5)
A = vcat(A0, A1)
b_lower = [ 0.21466922,  0.11140846, -0.4999999 ,  0.3920202 ,  0.4      ]
b_upper = [ 0.58819589,  0.4999999 , -0.49840835,  0.66474747,  0.4      ]
in_hyper  = Hyperrectangle(low = b_lower, high = b_upper)
inputSet = convert(HPolytope, in_hyper)
A = Matrix(undef, 2, 1)
A = [1.0, 0.0, 0.0, 0.0, -1.0]'
b = [0.0]
outputSet = HPolytope(A, b)
problem_polytope_polytope_acas = Problem(acas_nnet, inputSet, outputSet)
problem_acas = Problem(acas_nnet, in_hyper, outputSet)
#plot(Projection(outputSet, [1, 2]))
solver = MaxSens(1.0, false)
println("MaxSens - acas")
timed_result =@timed solve(solver, problem_acas)
println(" - Time: " * string(timed_result[2]) * " s")
print(" - Output: ")
println(timed_result[1].status)
print(" - width of output layer: ")
println(diameter(overapproximate((timed_result[1].reachable[1]), Hyperrectangle)))
#plot(Projection(timed_result[1].reachable[1], [1, 2]), label="MaxSens")
solver = Ai2z()
println("Ai2z - acas")
timed_result =@timed solve(solver, problem_acas)
println(" - Time: " * string(timed_result[2]) * " s")
print(" - Output: ")
println(timed_result[1].status)
print(" - width of output layer: ")
println(diameter(overapproximate((timed_result[1].reachable[1]), Hyperrectangle)))
plot(Projection(timed_result[1].reachable[1], [1, 2]), label="Ai2z")
solver = Box()
println("Box - acas")
timed_result =@timed solve(solver, problem_acas)
println(" - Time: " * string(timed_result[2]) * " s")
print(" - Output: ")
println(timed_result[1].status)
print(" - width of output layer: ")
println(diameter(overapproximate((timed_result[1].reachable[1]), Hyperrectangle)))
plot!(Projection(timed_result[1].reachable[1], [1, 2]), label="Box")
Shift+Enter to run
Julia
Julia 1.4.1
MaxSens - acas - Time: 0.000184581 s - Output: violated - width of output layer: 534083.7356066649 Ai2z - acas - Time: 0.001636253 s - Output: violated - width of output layer: 332.5758840908533 Box - acas - Time: 5.9375e-5 s - Output: violated - width of output layer: 9068.090897675178

In this last example the MaxSens set was not plotted as it was too big, the others sets cold not be seen, and the output set was not ploted because it was unbounded

As we can see, the output set in the MNIST tests was not correct, so I will only use them as a comparison for speed and precision.

Runtimes (1)