6 papers
Learning Lookahead Lemmas for Neural Network Verification
Liam Davis, Haoze Wu
State-of-the-art neural network verifiers use the branch-and-bound procedure as their core solving mechanism. We introduce an inprocessing framework for neural network verification…
Lookahead Branching for Neural Network Verification
Liam Davis, Duo Zhou, Huan Zhang +3
In this work, we investigate the effect of lookahead branching strategies in neural network verification. We present a general recipe to integrate lookahead into any branch-and-bou…
Lattice Deduction Transformers
Liam Davis, Leopold Haller, Alberto Alfarano +1
We introduce the Lattice Deduction Transformer (LDT), a recurrent transformer that approximates logically sound deduction by projecting its latent state through a lattice between f…
Incremental Neural Network Verification via Learned Conflicts
Raya Elsaleh, Liam Davis, Haoze Wu +1
Neural network verification is often used as a core component within larger analysis procedures, which generate sequences of closely related verification queries over the same netw…
Two Optimizations on the Stålmarck Procedure
Sergei Leonov, Liam Davis
In this paper, we introduce StalmarckSAT, the a modern re-implementation of the StÃ¥lmarck Procedure for SAT solving, and present two novel strategies to improve the Procedure, Car…
Evaluating SAT and SMT Solvers on Large-Scale Sudoku Puzzles
Liam Davis, Tairan Ji
Modern SMT solvers have revolutionized the approach to constraint satisfaction problems by integrating advanced theory reasoning and encoding techniques. In this work, we evaluate…