skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


This content will become publicly available on July 22, 2026

Title: NeuralSAT: A High-Performance Verification Tool for Deep Neural Networks
Abstract Deep Neural Networks (DNNs) are increasingly deployed in critical applications, where ensuring their safety and robustness is paramount. We present$$_\text {CAV25}$$ CAV 25 , a high-performance DNN verification tool that uses the DPLL(T) framework and supports a wide-range of network architectures and activation functions. Since its debut in VNN-COMP’23, in which it achieved the New Participant Award and ranked 4th overall,$$_\text {CAV25}$$ CAV 25 has advanced significantly, achieving second place in VNN-COMP’24. This paper presents and evaluates the latest development of$$_\text {CAV25}$$ CAV 25 , focusing on the versatility, ease of use, and competitive performance of the tool.$$_\text {CAV25}$$ CAV 25 is available at:https://github.com/dynaroars/neuralsat.  more » « less
Award ID(s):
2129824 2019239 2217071
PAR ID:
10644016
Author(s) / Creator(s):
; ;
Publisher / Repository:
Springer Nature Switzerland
Date Published:
Page Range / eLocation ID:
409 to 423
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Abstract We study certain one-parameter families of exponential sums of Airy–Laurent type. Their general theory was developed in Katz and Tiep (Airy sheaves of Laurent type: an introduction,https://web.math.princeton.edu/~nmk/kt31_11sept.pdf). In the present paper, we make use of that general theory to compute monodromy groups in some particularly simple families (in the sense of “simple to remember), realizing Weyl groups of type$$E_6$$ E 6 and$$E_8$$ E 8
    more » « less
  2. Abstract Let$$p_{1},\ldots ,p_{n}$$ p 1 , , p n be a set of points in the unit square and let$$T_{1},\ldots ,T_{n}$$ T 1 , , T n be a set of$$\delta $$ δ -tubes such that$$T_{j}$$ T j passes through$$p_{j}$$ p j . We prove a lower bound for the number of incidences between the points and tubes under a natural regularity condition (similar to Frostman regularity). As a consequence, we show that in any configuration of points$$p_{1},\ldots , p_{n} \in [0,1]^{2}$$ p 1 , , p n [ 0 , 1 ] 2 along with a line$$\ell _{j}$$ j through each point$$p_{j}$$ p j , there exist$$j\neq k$$ j k for which$$d(p_{j}, \ell _{k}) \lesssim n^{-2/3+o(1)}$$ d ( p j , k ) n 2 / 3 + o ( 1 ) . It follows from the latter result that any set of$$n$$ n points in the unit square contains three points forming a triangle of area at most$$n^{-7/6+o(1)}$$ n 7 / 6 + o ( 1 ) . This new upper bound for Heilbronn’s triangle problem attains the high-low limit established in our previous work arXiv:2305.18253. 
    more » « less
  3. Abstract It has been recently established in David and Mayboroda (Approximation of green functions and domains with uniformly rectifiable boundaries of all dimensions.arXiv:2010.09793) that on uniformly rectifiable sets the Green function is almost affine in the weak sense, and moreover, in some scenarios such Green function estimates are equivalent to the uniform rectifiability of a set. The present paper tackles a strong analogue of these results, starting with the “flagship degenerate operators on sets with lower dimensional boundaries. We consider the elliptic operators$$L_{\beta ,\gamma } =- {\text {div}}D^{d+1+\gamma -n} \nabla $$ L β , γ = - div D d + 1 + γ - n associated to a domain$$\Omega \subset {\mathbb {R}}^n$$ Ω R n with a uniformly rectifiable boundary$$\Gamma $$ Γ of dimension$$d < n-1$$ d < n - 1 , the now usual distance to the boundary$$D = D_\beta $$ D = D β given by$$D_\beta (X)^{-\beta } = \int _{\Gamma } |X-y|^{-d-\beta } d\sigma (y)$$ D β ( X ) - β = Γ | X - y | - d - β d σ ( y ) for$$X \in \Omega $$ X Ω , where$$\beta >0$$ β > 0 and$$\gamma \in (-1,1)$$ γ ( - 1 , 1 ) . In this paper we show that the Green functionGfor$$L_{\beta ,\gamma }$$ L β , γ , with pole at infinity, is well approximated by multiples of$$D^{1-\gamma }$$ D 1 - γ , in the sense that the function$$\big | D\nabla \big (\ln \big ( \frac{G}{D^{1-\gamma }} \big )\big )\big |^2$$ | D ( ln ( G D 1 - γ ) ) | 2 satisfies a Carleson measure estimate on$$\Omega $$ Ω . We underline that the strong and the weak results are different in nature and, of course, at the level of the proofs: the latter extensively used compactness arguments, while the present paper relies on some intricate integration by parts and the properties of the “magical distance function from David et al. (Duke Math J, to appear). 
    more » « less
  4. Abstract Given a suitable solutionV(t, x) to the Korteweg–de Vries equation on the real line, we prove global well-posedness for initial data$$u(0,x) \in V(0,x) + H^{-1}(\mathbb {R})$$ u ( 0 , x ) V ( 0 , x ) + H - 1 ( R ) . Our conditions onVdo include regularity but do not impose any assumptions on spatial asymptotics. We show that periodic profiles$$V(0,x)\in H^5(\mathbb {R}/\mathbb {Z})$$ V ( 0 , x ) H 5 ( R / Z ) satisfy our hypotheses. In particular, we can treat localized perturbations of the much-studied periodic traveling wave solutions (cnoidal waves) of KdV. In the companion paper Laurens (Nonlinearity. 35(1):343–387, 2022.https://doi.org/10.1088/1361-6544/ac37f5) we show that smooth step-like initial data also satisfy our hypotheses. We employ the method of commuting flows introduced in Killip and Vişan (Ann. Math. (2) 190(1):249–305, 2019.https://doi.org/10.4007/annals.2019.190.1.4) where$$V\equiv 0$$ V 0 . In that setting, it is known that$$H^{-1}(\mathbb {R})$$ H - 1 ( R ) is sharp in the class of$$H^s(\mathbb {R})$$ H s ( R ) spaces. 
    more » « less
  5. Abstract A search for exotic decays of the Higgs boson ($$\text {H}$$ H ) with a mass of 125$$\,\text {Ge}\hspace{-.08em}\text {V}$$ Ge V to a pair of light pseudoscalars$$\text {a}_{1} $$ a 1 is performed in final states where one pseudoscalar decays to two$${\textrm{b}}$$ b quarks and the other to a pair of muons or$$\tau $$ τ leptons. A data sample of proton–proton collisions at$$\sqrt{s}=13\,\text {Te}\hspace{-.08em}\text {V} $$ s = 13 Te V corresponding to an integrated luminosity of 138$$\,\text {fb}^{-1}$$ fb - 1 recorded with the CMS detector is analyzed. No statistically significant excess is observed over the standard model backgrounds. Upper limits are set at 95% confidence level ($$\text {CL}$$ CL ) on the Higgs boson branching fraction to$$\upmu \upmu \text{ b } \text{ b } $$ μ μ b b and to$$\uptau \uptau \text{ b } \text{ b },$$ τ τ b b , via a pair of$$\text {a}_{1} $$ a 1 s. The limits depend on the pseudoscalar mass$$m_{\text {a}_{1}}$$ m a 1 and are observed to be in the range (0.17–3.3) $$\times 10^{-4}$$ × 10 - 4 and (1.7–7.7) $$\times 10^{-2}$$ × 10 - 2 in the$$\upmu \upmu \text{ b } \text{ b } $$ μ μ b b and$$\uptau \uptau \text{ b } \text{ b } $$ τ τ b b final states, respectively. In the framework of models with two Higgs doublets and a complex scalar singlet (2HDM+S), the results of the two final states are combined to determine upper limits on the branching fraction$${\mathcal {B}}(\text {H} \rightarrow \text {a}_{1} \text {a}_{1} \rightarrow \ell \ell \text{ b } \text{ b})$$ B ( H a 1 a 1 b b ) at 95%$$\text {CL}$$ CL , with$$\ell $$ being a muon or a$$\uptau $$ τ lepton. For different types of 2HDM+S, upper bounds on the branching fraction$${\mathcal {B}}(\text {H} \rightarrow \text {a}_{1} \text {a}_{1} )$$ B ( H a 1 a 1 ) are extracted from the combination of the two channels. In most of the Type II 2HDM+S parameter space,$${\mathcal {B}}(\text {H} \rightarrow \text {a}_{1} \text {a}_{1} )$$ B ( H a 1 a 1 ) values above 0.23 are excluded at 95%$$\text {CL}$$ CL for$$m_{\text {a}_{1}}$$ m a 1 values between 15 and 60$$\,\text {Ge}\hspace{-.08em}\text {V}$$ Ge V
    more » « less