@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Kuldeep S. Meel's publication pages at
@COMMENT http://www.comp.nus.edu.sg/~meel/publications/
@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.
  },
}