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

Mikoláš Janota, Mirek Olšák

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…