wenkokke / amethyst Goto Github PK
View Code? Open in Web Editor NEWAgda library for verifying neural networks.
Home Page: https://wenkokke.github.io/amethyst/
License: Other
Agda library for verifying neural networks.
Home Page: https://wenkokke.github.io/amethyst/
License: Other
I'm trying to get an auto-encoder example up and running and to do so I need to refer to the values of the neurons in the hidden layer inside the constraints, rather than just the network inputs and outputs.
While I was investigating how best to do this, I notice that we don't have an SMT variable for each neuron value but instead just define the expression for the ouput of layer
For example, even with a simple 1 hidden layer network
layer1 : Layer Float 2 1
layer1 = record
{ weights = [ 3.0 ] ∷ [ 2.0 ] ∷ []
; biases = [ 0.2 ]
; activation = relu
}
layer2 : Layer Float 1 2
layer2 = record
{ weights = (-2.0 ∷ -1.0 ∷ []) ∷ []
; biases = -0.1 ∷ -0.2 ∷ []
; activation = relu
}
we get the expression:
(assert (and (= __1 (ite (<= (+ (- 0.1) (+ (* (ite (<= (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0))) 0.0) 0.0 (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0)))) (- 2.0)) 0.0)) 0.0) 0.0 (+ (- 0.1) (+ (* (ite (<= (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0))) 0.0) 0.0 (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0)))) (- 2.0)) 0.0)))) (and (= __0 (ite (<= (+ (- 0.2) (+ (* (ite (<= (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0))) 0.0) 0.0 (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0)))) (- 1.0)) 0.0)) 0.0) 0.0 (+ (- 0.2) (+ (* (ite (<= (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0))) 0.0) 0.0 (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0)))) (- 1.0)) 0.0)))) true)))
which contains the subexpression (+ (* (ite (<= (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0))) 0.0) 0.0 (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0)))
no less then four times.
I'm not sure how clever z3
and marabou
are, and if they do common subexpression identification, but even so I'm pretty sure that any solver is going to choke if we continue to take this approach for deeper networks. Not to mention that Amethyst may fall over even generating such expressions.
I would recommend that we switch to generating a variable for the output of each neuron in the network. @wenkokke is there any reason why this representation would have drawbacks? Obviously there's an increase in the number of variables, but I feel like this gives the solvers more flexibility as it is presumably much easier for them to eliminate the extra variables if they want to, but much harder for them to recover them.
At the moment I can't seem to get z3
to fail. For example if in AND-Gate-2-Sigmoid-1
we have the following code which type checks fine:
script : Script [] (Reals 2 ++ Reals 1) (SAT ∷ [])
script = withReflectedNetworkAsScript model $ λ where
-- give names to input and output nodes
iv@(i₀ ∷ i₁ ∷ []) ov@(o₀ ∷ [])
-- give remainder of the smt-lib script
→ assert (i₀ == 0·0f ∧ i₁ == 0·0f ⇒ o₀ == 0·0f)
∷ assert (i₀ == 0·0f ∧ i₁ == 1·0f ⇒ o₀ == 0·0f)
∷ assert (i₀ == 1·0f ∧ i₁ == 0·0f ⇒ o₀ == 0·0f)
∷ assert (i₀ == 1·0f ∧ i₁ == 1·0f ⇒ o₀ == 1·0f)
∷ check-sat
∷ []
_ : z3 script ≡ sat ∷ []
_ = refl
However changing the first assertion to:
assert (i₀ == 0·0f ∧ i₁ == 0·0f ⇒ o₀ == 1·0f)
also appears to type-check which is more than a little worrying....
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.