NL2SMT-A LLM based SMT-LIB generation framework

Miao, Zhiyuan

doi:10.1016/j.infsof.2026.108229

NL2SMT-A LLM based SMT-LIB generation framework

2026-07-01

0

PRE

AI

DOI：10.1016/j.infsof.2026.108229

原文链接

原文求助

摘要

En 中文

背景：SMT-LIB是用于SMT-可满足性模块理论的最广泛采用的标准语言，这是自动推理中的一个基础问题。将自然语言（NL）翻译成SMT-LIB公式是实现形式化验证更易访问和自动化的关键步骤。大型语言模型（LLMs）的近期进展为NL到形式化翻译提供了有希望的基础，但由于SMT-LIB断言的复杂逻辑结构和严格的语法要求，将LLMs应用于SMT-LIB仍然具有挑战性。目标：本文旨在利用大型语言模型解决NL到SMT的翻译问题，通过设计一个基于LLM的两阶段框架，结合提示与模型微调。方法：我们提出一个基于LLM的两阶段框架用于NL到SMT的翻译。首先，我们通过应用少量提示的LLMs对从SMT-LIB基准中提取的SMT断言进行操作，构建了一个包含5000多对NL-SMT的语料库。在翻译阶段，为了弥合自然语言与SMT-LIB之间的差距，每个NL输入通过语法感知提示被转换为一个结构化的中间表示，以反映其底层的语法和逻辑结构。然后，一个微调的语言模型将此中间表示转换为相应的SMT断言。结果：实验结果表明，所提出的基于LLM的两阶段框架显著优于直接端到端的LLM提示，通过结合GPT-4o提示和一个微调的T5-large模型，准确率达到90.56%。结论：这项工作表明，一个基于LLM的两阶段框架能够有效解决将自然语言翻译成SMT-LIB断言的挑战。通过结合LLM驱动的语法感知提示与LLM微调，所提出的方法提高了翻译准确率，优于端到端的LLM提示。结果还表明，这种以LLM为中心的分解可能对其他NL到形式化翻译任务有益。

Keyword:

SMT-LIB

Large language model

Model finetuning

Prompt engineering

NL2SMT-A LLM based SMT-LIB generation framework

摘要

期刊

机构

引用论文