LLM-Assisted Unsatisfiability Proofs for Satisfiability Modulo Theories, Oracles, and Natural Language

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.