Hugo Academic CV Theme

Liam Davis

AI Researcher, Engineer, Quant

About Me

Liam is a sophomore 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, including Andrew Wu at Amherst College, 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

Online Learning for Neural Network Verification

This ongoing research explores the application of online learning techniques to improve neural network verification efficiency. By developing reinforcement learning methods that adapt branching strategies during verification, we aim to significantly reduce computational costs while maintaining formal guarantees. Our work extends the Marabou verification framework with learned decision heuristics that show promise for overcoming scalability challenges in neural network safety verification.

Liam Davis

• Dec 1, 2024

Formal Methods

Optimizations on the Stalmarck Procedure

We make optimizations in the form of clause learning and directional heuristics on the Stålmarck procedure for boolean satisfiability. This research explores how modern SAT solving techniques can enhance the classical Stålmarck algorithm, making it more practical for industry applications.

Liam Davis

• Mar 1, 2024

Awards

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.

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.