Unclear Intermediate Layer Implementation in find_adversarial_example

[ace-shifu]

Hello, I am very interested in your project, but after reading the source code of find_adversarial_example, I found that only input constraints and related output constraints are shown to be set. However, intermediate layers such as affine and ReLU layers are not explicitly called. How do you call these methods from the layers directory in find_adversarial_example to accomplish intermediate layer encoding?

[vtjeng]

Hi @ace-shifu -- thanks for your interest.

Here's an example where you specify the neural network:

MIPVerify.jl/test/integration/sequential/generated_weights/mfc+mfc+softmax.jl

Lines 29 to 39 in b0ebe49

	nn = Sequential(
	[
	Flatten(4),
	Linear(l1_kernel, l1_bias),
	MaskedReLU(m1),
	Linear(l2_kernel, l2_bias),
	MaskedReLU(m2),
	Linear(l3_kernel, l3_bias),
	],
	"tests.integration.generated_weights.mfc+mfc+softmax",
	)

Let's start by taking a look at the Sequential struct:

MIPVerify.jl/src/net_components/nets/sequential.jl

Lines 12 to 25 in b0ebe49

	struct Sequential <: NeuralNet
	layers::Array{Layer,1}
	UUID::String
	end
	function Base.show(io::IO, p::Sequential)
	println(io, "sequential net $(p.UUID)")
	for (index, value) in enumerate(p.layers)
	println(io, " ($index) $value")
	end
	end
	(p::Sequential)(x::Array{<:JuMPReal}) = x |> p.layers

The key chunk of code is the last line, where we defined p(x) = x |> p.layers (the equivalent of p.layers(x) in other programming languages).

Now, here's the important bit: x can either be a number or a JuMPLinearType:

MIPVerify.jl/src/net_components.jl

Line 5 in b0ebe49

JuMPLinearType = Union{JuMP.VariableRef,JuMP.AffExpr}

If x is a JuMPLinearType, then the output p(x) is also a JuMPLinearType, with the appropriate constraints imposed between the input and output. (This is what the output constraints are imposed on).

Feel free to reach out if you have more questions.

[ace-shifu]

Thank you for your patient response. My issue has been resolved.