Liam Davis

I’m an undergraduate at Amherst College studying Mathematics and Computer Science. My interests lie at the intersection of formal methods and artificial intelligence. In particular, I work on using formal methods to verify the safety of AI systems, and improve the reasoning capabilities of AI.

At Amherst, I work with Professor Andrew Wu on neural network verification, particularly on the Marabou framework. I have also worked on the alpha-beta-CROWN framework. During the Spring 2026 Semester I was a visiting student at Columbia University worked with Professor Mark Santolucito and Axiom on neurosymbolic AI. Specifically, we developed the Lattice Deduction Transformer, which uses abstract interpretation to improve the reasoning capabilities of transformers. I also dabble in SAT/SMT solving.

In the summer of 2026 I’ll be a Software Engineering Intern at LinkedIn in Sunnyvale, CA.

Feel free to reach out at ljdavis27@amherst.edu.

news

Apr 15, 2026	Our paper Lookahead Branching for Neural Network Verification got accepted to IJCAI ‘26! I will be going to Bremen, Germany this August to present the work.

selected publications

IJCAI

Lookahead Branching for Neural Network Verification

Liam Davis, Duo Zhou, Huan Zhang, and 3 more authors

In To Appear at the 35th International Joint Conference on Artificial Intelligence (IJCAI ’26), 2026

Bib

@inproceedings{davis2026lookahead,
  title = {Lookahead Branching for Neural Network Verification},
  author = {Davis, Liam and Zhou, Duo and Zhang, Huan and Katz, Guy and Barrett, Clark and Wu, Haoze},
  booktitle = {To Appear at the 35th International Joint Conference on Artificial Intelligence (IJCAI '26)},
  year = {2026},
}

Lattice Deduction Transformers

Liam Davis, Leopold Haller, Alberto Alfarano, and 1 more author

. Under review at NeurIPS , 2026

Bib

Incremental Neural Network Verification via Learned Conflicts

Reem Elsaleh, Liam Davis, Haoze Wu, and 1 more author

arXiv preprint arXiv:2603.12232. Under review at FMCAD , 2026

arXiv Bib

@article{elsaleh2026incremental,
  title = {Incremental Neural Network Verification via Learned Conflicts},
  author = {Elsaleh, Reem and Davis, Liam and Wu, Haoze and Katz, Guy},
  journal = {arXiv preprint arXiv:2603.12232},
  year = {2026},
}

FMCAD

Two Optimizations on the Stålmarck Procedure

Sergei Leonov and Liam Davis

In FMCAD Student Forum, 2025

arXiv Bib