• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Solution-Aware Vs Global ReLU Selection: Partial MILP Strikes Back for DNN Verification .
Yuke Liao, Blaise Genest, Kuldeep S. Meel and Shaan Aryaman.
In Proceedings of International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 299–320, 2025.
To handle complex instances, we revisit a divide-and-conquer approach to break down the complexity: instead of few complex BaB calls, we rely on many small partial MILP calls. The crucial step is to select very few but very important ReLUs to treat using (costly) binary variables. The previous attempts were suboptimal in that respect. To select these important ReLU variables, we propose a novel solution-aware ReLU scoring (\sf SAS), as well as adapt the BaB-SR and BaB-FSB branching functions as global ReLU scoring (\sf GS) functions. We compare them theoretically as well as experimentally, and \sf SAS is more efficient at selecting a set of variables to open using binary variables. Compared with previous attempts, SAS reduces the number of binary variables by around 6 times, while maintaining the same level of accuracy. Implemented in Hybrid MILP, calling first $alpha,beta$-CROWN with a short time-out to solve easier instances, and then partial MILP, produces a very accurate yet efficient verifier, reducing by up to $40%$ the number of undecided instances to low levels ($8-15%$), while keeping a reasonable runtime ($46s-417s$ on average per instance), even for fairly large CNNs with 2 million parameters.
@inproceedings{LGMA25,
title={
Solution-Aware Vs Global ReLU Selection: Partial MILP Strikes Back for DNN
Verification
},
author={
Liao, Yuke and Genest, Blaise and Meel, Kuldeep S. and Aryaman, Shaan
},
booktitle=ATVA,
pages={299--320},
year={2025},
bib2html_rescat={Formal Methods 4 ML},
bib2html_pubtype={Refereed Conference},
bib2html_dl_pdf={https://arxiv.org/pdf/2507.23197},
abstract={
To handle complex instances, we revisit a divide-and-conquer approach to
break down the complexity: instead of few complex BaB calls, we rely on many
small {\em partial} MILP calls. The crucial step is to select very few but
very important ReLUs to treat using (costly) binary variables. The previous
attempts were suboptimal in that respect. To select these important ReLU
variables, we propose a novel {\em solution-aware} ReLU scoring ({\sf SAS}),
as well as adapt the BaB-SR and BaB-FSB branching functions as {\em global}
ReLU scoring ({\sf GS}) functions. We compare them theoretically as well as
experimentally, and {\sf SAS} is more efficient at selecting a set of
variables to open using binary variables. Compared with previous attempts,
SAS reduces the number of binary variables by around 6 times, while
maintaining the same level of accuracy. Implemented in {\em Hybrid MILP},
calling first $alpha,beta$-CROWN with a short time-out to solve easier
instances,
and then partial MILP, produces a very accurate yet efficient verifier,
reducing by up to $40\%$ the number of undecided instances to low levels
($8-15\%$), while keeping a reasonable runtime ($46s-417s$ on average per
instance), even for fairly large CNNs with 2 million parameters.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21