English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Recently, formal verification of deep neural networks (DNNs) has garneredconsiderable attention, and over-approximation based methods have becomepopular due to their effectiveness and efficiency. However, these strategiesface challenges in addressing the "unknown dilemma" concerning whether theexact output region or the introduced approximation error violates the propertyin question. To address this, this paper introduces the UR4NNV verificationframework, which utilizes under-approximation reachability analysis for DNNverification for the first time. UR4NNV focuses on DNNs with Rectified LinearUnit (ReLU) activations and employs a binary tree branch-basedunder-approximation algorithm. In each epoch, UR4NNV under-approximates asub-polytope of the reachable set and verifies this polytope against the givenproperty. Through a trial-and-error approach, UR4NNV effectively falsifies DNNproperties while providing confidence levels when reaching verification epochbounds and failing falsifying properties. Experimental comparisons withexisting verification methods demonstrate the effectiveness and efficiency ofUR4NNV, significantly reducing the impact of the "unknown dilemma".

UR4NNV: Neural Network Verification, Under-approximation Reachability Works!