一句话：首个能为含闭盒函数调用的 SMT 公式生成不可满足性证明的求解器，借助 LLM 从自然语言文档猜想辅助引理。
现代软件常调用源码不可见的闭盒函数，只能以 oracle 方式执行，已有 SMT 扩展多依赖测试式模型搜索，无法构造不可满足性证明，难以用于形式验证。本文提出首个能为含闭盒函数调用的 SMT 公式生成不可满足性证明的求解器。关键思路是用 LLM 根据自然语言文档猜想辅助引理；并扩展 SMT-LIB，支持声明闭盒函数及其描述、示例与 oracle 接口。作者实现 NLUnsat。在 193 个扩展 SMT-LIB 问题上，配 openai.gpt-oss:20b 求解 89%，五个 LLM 的虚拟最佳达 98%；在 15 个演绎验证程序上，用两个 LLM 证明全部目标；在 107 个可满足实例中无错判，并为 57 个找到模型。
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.
@article{paperbot12155,
title = {LLM-Assisted Unsatisfiability Proofs for Satisfiability Modulo Theories, Oracles, and Natural Language},
author = {Gourav Takhar and Sumit Lahiri and Pankaj Kumar Kalita and Subhajit Roy},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839451}
}