Gourav Takhar

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 S...