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

TL;DR

This paper demonstrates that a large language model can autonomously develop a complete SMT solver for QF_UF, including algorithms and proof generation, without any human-written code, showing promising results on benchmarks.

Contribution

It introduces a novel approach where an LLM builds an entire SMT solver from scratch, including algorithms and proof output, without human coding.

Findings

The LLM-created solver is competitive on SMT-LIB benchmarks.

The solver implements the Nieuwenhuis-Oliveras congruence closure algorithm.

The development process highlights key challenges and solutions.

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.