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

Formal verification of neural networks (NNs) is a challenging and importantproblem. Existing efficient complete solvers typically require thebranch-and-bound (BaB) process, which splits the problem domain intosub-domains and solves each sub-domain using faster but weaker incompleteverifiers, such as Linear Programming (LP) on linearly relaxed sub-domains. Inthis paper, we propose to use the backward mode linear relaxation basedperturbation analysis (LiRPA) to replace LP during the BaB process, which canbe efficiently implemented on the typical machine learning accelerators such asGPUs and TPUs. However, unlike LP, LiRPA when applied naively can produce muchweaker bounds and even cannot check certain conflicts of sub-domains duringsplitting, making the entire procedure incomplete after BaB. To address thesechallenges, we apply a fast gradient based bound tightening procedure combinedwith batch splits and the design of minimal usage of LP bound procedure,enabling us to effectively use LiRPA on the accelerator hardware for thechallenging complete NN verification problem and significantly outperformLP-based approaches. On a single GPU, we demonstrate an order of magnitudespeedup compared to existing LP-based approaches.

Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers