面向 LLM 生成输出的自动形式化：用于需求验证

自动形式化（即将非正式语句翻译为正式逻辑的过程）因强大大型语言模型（LLMs）的出现而重新受到关注。尽管 LLMs 在从自然语言（NL）生成结构化输出方面显示出前景，例如从 NL 功能需求生成 Gherkin 场景，但目前尚无方法可验证这些输出是否准确。本文通过探索使用简单 LLM 基于自动形式化器来验证 LLM 生成的输出是否符合一小组自然语言需求，作为解决这一空白的初步步骤。我们进行了两项实验。首先，自动形式化器成功识别出两个不同措辞的 NL 需求在逻辑上等价，表明该管道在一致性检查方面的潜力。其次，自动形式化器用于识别给定 NL 需求与 LLM 生成输出之间的逻辑不一致，突显其作为形式化验证工具的实用性。尽管这些发现有限，但表明自动形式化在确保 LLM 生成输出的忠实性和逻辑一致性方面具有重要潜力，为未来更广泛的研究奠定了关键基础。