LLM-Assisted Unsatisfiability Proofs for SMT Queries with Closed-Box Functions

Title: LLM-Assisted Unsatisfiability Proofs for SMT Queries with Closed-Box Functions
Host Faculty: Dr. Ashish Mishra
Speaker: Gourav Takhar
Date: October 06th
Time: 11:00 pm
Venue: CS Seminar Hall, Ground Floor, EECS Building

Abstract

Modern software systems routinely invoke components whose source code is unavailable, such as proprietary libraries or cloud-based APIs. Such closed-box functions provide only oracle-style access: they can be executed on concrete inputs, but their internal logic cannot be inspected. Prior work has explored augmenting SMT solvers—the foundational engines behind contemporary automated reasoning—to handle satisfiability queries over first-order formulas containing calls to such closed-box functions. However, these approaches primarily rely on testing-based techniques to search for satisfying models and therefore do not support constructing proofs of unsatisfiability. While model search is sufficient for bug-finding tasks, the inability to generate unsatisfiability proofs fundamentally limits their applicability to formal verification.

In this work, we present the first SMT solver capable of producing proofs of unsatisfiability for first-order theories that include closed-box function calls. Our key insight is to leverage large language models (LLMs) to conjecture auxiliary lemmas—based on natural-language documentation of the closed-box functions—that capture properties relevant for reasoning about their behavior. To support this approach, we introduce an extension of the SMT-LIB language that allows the declaration of closed-box functions together with natural-language descriptions, usage documentation, examples, and oracle interfaces. We then develop NLUnsat, an SMT solver that operates over this extended syntax to find unsatisfiability proofs on SMT-LIB formulas with closed-box functions.

On a benchmark suite of 193 extended SMT-LIB problems involving closed-box functions, NLUnsat equipped with the openai.gpt-oss:20b LLM solves 89% of the instances, and a virtual best solver across five LLMs solves 98% of the instances. We further evaluate NLUnsat in the setting of deductive verification for programs containing closed-box function calls. On a collection of 15 benchmark programs, our verifier, using NLUnsat as its backend solver, successfully proves all verification goals when given access to a pool of two LLMs, openai.gpt-oss:20b and openai.gpt-oss:120b. Finally, we evaluate NLUnsat on satisfiable benchmark instances: none of these instances were incorrectly classified as unsatisfiable, and the solver successfully finds models for 57 out of 107 satisfiable instances.

Bio

Gourav Takhar is a Postdoctoral Researcher in the Department of CSE at IIT Kanpur, working with Prof. Subhajit Roy. He received his Ph.D. from IIT Kanpur, where his research focused on synthesis for security and bug detection. His research interests include formal methods, program verification, program synthesis, and computer security. He has published in leading venues such as OOPSLA, CAV, TACAS, ASE, TOSEM, HOST, and ICCAD. His work received the Best Paper Award at ICCAD. His recent research explores automated program verification using synthesis and large language models.