Liam Davis

AI Researcher, Engineer, Quant

About Me

Liam is a junior at Amherst College majoring in Mathematics and Computer Science with experience in AI research, software engineering, and quantitative research. He combines theoretical knowledge with practical engineering and business experience, bringing his pragmatic approach to solving complex problems across multiple domains.

Interests

Artificial Intelligence
Automated Reasoning
Formal Methods

Education

BA Mathematics and Computer Science
Amherst College
Breakthrough Tech AI Fellow
MIT
Certificate in Software Engineering
CodePath

📚 My Research

My research focuses on the formal verification of AI systems, and in particular, I am a developer of the Marabou verification framework. I also contribute to the alpha-beta-CROWN framework.

I’m currently working with several people, but my main advisor is Andrew Wu at Amherst College. Through my collaborations with the Marabou and alpha-beta-CROWN teams, I also work with Clark Barrett at Stanford, Guy Katz at Hebrew University of Jerusalem, and Huan Zhang at UIUC.

Evaluating SAT and SMT Solvers on Large-Scale Sudoku Puzzles

We benchmark traditional SAT Solvers and modern SMT Solvers against each other with 25x25 Sudoku, deriving insights on the evolution of satisfiability.

Liam Davis

• Jan 15, 2025

Educational Technology

RBlocks: Block Programming IDE for R

RBlocks is a block-based R IDE designed to be an introductory programming interface for Statistics students.

Liam Davis

• Jan 2, 2025

Artificial Intelligence

Lookahead Branching for Neural Network Verification

We present a general lookahead branching method for branch-and-bound in neural network verification, and demonstrate that spending more time at key points in branch-and-bound evaluating branching decisions leads to more efficient verification.

Liam Davis

• Dec 1, 2024

Formal Methods

Two Strategies to Improve the Stålmarck Procedure

We develop an open source modern re-implementation Stålmarck procedure for boolean satisfiability, and explore two strategies in CDB and DPO to improve the performance of the procedure.

Liam Davis

• Mar 1, 2024

Awards

Y Combinator AI Startup School Fellow

Y Combinator ∙ June 2025

I was selected amongst ~20k applicants as a Y Combinator AI Startup School fellow that led to the opportunity to meet people like Satya Nadella, Fei Fei Li, Andrej Karpathy, and John Jumper.

2nd Prize at 2025 Cubist Hackathon

Cubist Systematic Strategies ∙ April 2025

I won 2nd Prize at the 2025 Cubist Hackathon by Cubist Systematic Strategies and Point72, making me the only every two-time winner of the Cubist Hackathon. I built an advanced data visualization tool for NYC congestion data that serves as an all-in-one EDA playground, as well as streams live data for anomaly detection.

Two Sigma New Seeker’s Summit Fellow

Two Sigma ∙ January 2025

I was selected to participate in Two Sigma’s New Seeker’s Summit to engage with quant developers and researchers at Two Sigma and learn about the firm.

2nd Prize at 2024 Cubist Hackathon

Cubist Systematic Strategies ∙ April 2024

I won 2nd Prize at the 2024 Cubist Hackathon by Cubist Systematic Strategies and Point72 as the only first year undergrad invited amongst Masters and PhD students. For the hackathon, I built Vendor Map, an end-to-end web application that streams live NYC foot traffic data and combines it with game theory principles to optimally allocate food vendors across the city.

Best Use of External Data at ASA Five College Datafest

American Statisticians Association ∙ April 2025

I won best use of external data at the Five College Datafest hosted by the American Statisticians Association the same week I won the 2025 Cubist Hackathon. It was not a bad weekend.

United States National Finalist at the 2025 Hult Prize Startup Pitch Challenge

Hult International ∙ March 2025

I am was named a national finalist for the 2025 Hult Prize by pitching TalentNexus, an personalized AI onboarding experience to go from new hire to high performer.