LLM2SMT: Building an SMT Solver with Zero Human-Written Code

TL;DR

A case study is presented in which an LLM coding agent builds a complete DPLL(T)-style SMT solver for QF_UF with zero human-written code, and the resulting solver is competitive on SMT-LIB benchmarks.

Abstract

Whether LLMs can reason or write software is widely debated, but whether they can write software that itself reasons is largely unexplored. We present a case study in which an LLM coding agent builds a complete DPLL(T)-style SMT solver for QF_UF with zero human-written code. The solver implements the Nieuwenhuis-Oliveras congruence closure algorithm, includes preprocessing, and emits Lean proofs for unsatisfiable instances. We describe the development process and key challenges, and show that the resulting solver is competitive on SMT-LIB benchmarks.

Figures (1)

• Figure 1: Comparison with and without theory propagation.