Embedded Files
Network and specficiation
Β A group of neural networks π , π β and π β , where π β and π β are generated by slightly altering the model parameters of π.Β
The specification concerns whether its output π satisfies that π + 2.5 β₯ 0, for any input (π₯1, π₯2) β [0, 1] Γ [0, 1].Β
Verification from scratch v.s. Incremental Verification
Β Here, the template to accelerate the verification of a network π β that has the identical structure to π but slightly differs in model parameters. Ivan is illustrated in the middle.Β
Compared to re-applying BaB to π β, Ivan skips the non-leaf nodes in the template (i.e., the tree in the verification of π ) and directly starts with verification of the sub-problems identified by the leaf nodes, because during the verification of π β.Β
BaB may also be not able to terminate until it reaches the sub-problems identified by the leaf nodes. By this, Ivan can save the time spent for the non-lead nodes in verification of π β. Indeed, its superiority is illustrated: compared to BaB that needs 6 calls of the approximated verifier (Fig. 2a), Ivan requires only 3 times.
Β Olive-G identifies the leaf node, of which is 0.5 in the template, that has the same depth but smaller assessment than other leaf nodes, signifying that it is closest to specification violation. Olive-G prioritizes this node, and it immediately hits the real counterexample, which costs three sub-problem attempts for Ivan.Β
Multi-armed bandit incremental verification Olive-G v.s. Olive-B
The strategy of Olive-G is greedy, in the sense that it always prefers the nodes that are more likely to contain counterexamples according to the template. However, this strategy can fail, because it is possible that the tree of the updated network is divergent from that of the original network.Β
In this case, we need a balanced strategy, Olive-B that not only favors the suspicious nodes, but also explores other nodes to avoid being misled by an imprecise template.Β
Detailed Multi-armed Bandit for incremental verification on Olive-B
On the leaves, verification is now represented as multiple subproblems, which can be viewed as multiple tree growths, such that the distribution of counterexamples is also associated with the rewards delivered by one of the levers, as per the round of computation of the bound and the observation of the rewards. So the multiple subproblems by reusing the template are viewed as Multi-armed Bandit.
Google Sites
Report abuse