Achieving the Tightest Relaxation of Sigmoids for Formal Verification
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914920450228224 |
|---|---|
| author | Chevalier, Samuel Starkenburg, Duncan Dvijotham, Krishnamurthy |
| author_facet | Chevalier, Samuel Starkenburg, Duncan Dvijotham, Krishnamurthy |
| contents | In the field of formal verification, Neural Networks (NNs) are typically reformulated into equivalent mathematical programs which are optimized over. To overcome the inherent non-convexity of these reformulations, convex relaxations of nonlinear activation functions are typically utilized. Common relaxations (i.e., static linear cuts) of "S-shaped" activation functions, however, can be overly loose, slowing down the overall verification process. In this paper, we derive tuneable hyperplanes which upper and lower bound the sigmoid activation function. When tuned in the dual space, these affine bounds smoothly rotate around the nonlinear manifold of the sigmoid activation function. This approach, termed $α$-sig, allows us to tractably incorporate the tightest possible, element-wise convex relaxation of the sigmoid activation function into a formal verification framework. We embed these relaxations inside of large verification tasks and compare their performance to LiRPA and $α$-CROWN, a state-of-the-art verification duo. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_10491 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Achieving the Tightest Relaxation of Sigmoids for Formal Verification Chevalier, Samuel Starkenburg, Duncan Dvijotham, Krishnamurthy Machine Learning Artificial Intelligence In the field of formal verification, Neural Networks (NNs) are typically reformulated into equivalent mathematical programs which are optimized over. To overcome the inherent non-convexity of these reformulations, convex relaxations of nonlinear activation functions are typically utilized. Common relaxations (i.e., static linear cuts) of "S-shaped" activation functions, however, can be overly loose, slowing down the overall verification process. In this paper, we derive tuneable hyperplanes which upper and lower bound the sigmoid activation function. When tuned in the dual space, these affine bounds smoothly rotate around the nonlinear manifold of the sigmoid activation function. This approach, termed $α$-sig, allows us to tractably incorporate the tightest possible, element-wise convex relaxation of the sigmoid activation function into a formal verification framework. We embed these relaxations inside of large verification tasks and compare their performance to LiRPA and $α$-CROWN, a state-of-the-art verification duo. |
| title | Achieving the Tightest Relaxation of Sigmoids for Formal Verification |
| topic | Machine Learning Artificial Intelligence |
| url | https://arxiv.org/abs/2408.10491 |