Generative large language models (LLMs) with instruct training such as GPT-4 can follow human-provided instruction prompts and generate human-like responses to these prompts. Apart from natural language responses, they have also been found to be effective at generating formal artifacts such as code, plans, and logical specifications from natural language prompts. Despite their remarkably improved accuracy, these models are still known to produce factually incorrect or contextually inappropriate results despite their syntactic coherence - a phenomenon often referred to as hallucination. This limitation makes it difficult to use these models to synthesize formal artifacts that are used in safety-critical applications. Unlike tasks such as text summarization and question-answering, bugs in code, plan, and other formal artifacts produced by LLMs can be catastrophic. We posit that we can use the satisfiability modulo theory (SMT) solvers as deductive reasoning engines to analyze the generated solutions from the LLMs, produce counterexamples when the solutions are incorrect, and provide that feedback to the LLMs exploiting the dialog capability of instruct-trained LLMs. This interaction between inductive LLMs and deductive SMT solvers can iteratively steer the LLM to generate the correct response. In our experiments, we use planning over the domain of blocks as our synthesis task for evaluating our approach. We use GPT-4, GPT3.5 Turbo, Davinci, Curie, Babbage, and Ada as the LLMs and Z3 as the SMT solver. Our method allows the user to communicate the planning problem in natural language; even the formulation of queries to SMT solvers is automatically generated from natural language. Thus, the proposed technique can enable non-expert users to describe their problems in natural language, and the combination of LLMs and SMT solvers can produce provably correct solutions.

翻译：生成式大语言模型（LLMs），例如经过指令训练的GPT-4，能够遵循人类提供的提示指令并生成类人响应。除自然语言响应外，这些模型在从自然语言提示生成代码、规划、逻辑规约等正式产物方面也表现出高效性。尽管其准确性显著提升，但此类模型仍可能产生虽句法连贯却事实错误或语境不当的结果——这一现象常被称为“幻觉”。该局限性使得此类模型难以用于安全关键应用场景中正式产物的合成。与文本摘要、问答等任务不同，LLMs生成的代码、规划及其他正式产物中的错误可能引发灾难性后果。我们提出，可运用可满足性模理论（SMT）求解器作为演绎推理引擎，分析LLMs生成的解决方案，在方案错误时生成反例，并利用指令训练LLMs的对话能力将反馈回输给模型。这种归纳式LLMs与演绎式SMT求解器之间的交互，能够迭代引导LLM生成正确响应。实验中，我们以积木领域规划作为综合任务评估该方法，使用GPT-4、GPT3.5 Turbo、Davinci、Curie、Babbage及Ada作为LLMs，Z3作为SMT求解器。该方法允许用户以自然语言描述规划问题，甚至对SMT求解器的查询公式也由自然语言自动生成。因此，所提技术可支持非专业用户用自然语言描述问题，而LLMs与SMT求解器的结合能够生成可证明正确的解决方案。