LLM2SMT: Building an SMT Solver with Zero Human-Written Code
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911503022555136 |
|---|---|
| author | Janota, Mikoláš Olšák, Mirek |
| author_facet | Janota, Mikoláš Olšák, Mirek |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_06931 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | LLM2SMT: Building an SMT Solver with Zero Human-Written Code Janota, Mikoláš Olšák, Mirek Logic in Computer Science 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. |
| title | LLM2SMT: Building an SMT Solver with Zero Human-Written Code |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2603.06931 |