用LLM将自然语言需求转为逻辑表达式，验证生成内容是否正确
Towards Autoformalization of LLM-generated Outputs for Requirement Verification
- 用LLM将自然语言需求转为形式化逻辑表达式
- 发现两个不同表述的需求逻辑等价，识别出生成输出的矛盾
- 适合关注大模型输出可靠性的开发者与验证研究者
自动形式化，即把非正式陈述转化为形式逻辑，随着强大大语言模型（LLMs）的出现而重新受到关注。尽管LLMs在从自然语言（NL）生成结构化输出（如将需求转为Gherkin场景）方面展现出潜力，但目前尚无正式方法验证这些输出的准确性。本文初步探索了基于简单LLM的自动形式化工具，用于验证LLM生成的输出是否符合少量自然语言需求。我们进行了两项实验：第一项中，该工具成功识别出两个不同表述的自然语言需求在逻辑上等价，展示了其在一致性检查方面的潜力；第二项中，该工具识别出给定自然语言需求与一个LLM生成输出之间的逻辑矛盾，凸显其作为形式化验证工具的价值。尽管研究范围有限，但结果表明自动形式化在确保大模型输出的准确性和逻辑一致性方面具有巨大潜力，为未来更广泛的研究奠定了重要基础。
原文摘要 · Abstract (English)
Autoformalization, the process of translating informal statements into formal logic, has gained renewed interest with the emergence of powerful Large Language Models (LLMs). While LLMs show promise in generating structured outputs from natural language (NL), such as Gherkin Scenarios from NL feature requirements, there's currently no formal method to verify if these outputs are accurate. This paper takes a preliminary step toward addressing this gap by exploring the use of a simple LLM-based autoformalizer to verify LLM-generated outputs against a small set of natural language requirements. We conducted two distinct experiments. In the first one, the autoformalizer successfully identified that two differently-worded NL requirements were logically equivalent, demonstrating the pipeline's potential for consistency checks. In the second, the autoformalizer was used to identify a logical inconsistency between a given NL requirement and an LLM-generated output, highlighting its utility as a formal verification tool. Our findings, while limited, suggest that autoformalization holds significant potential for ensuring the fidelity and logical consistency of LLM-generated outputs, laying a crucial foundation for future, more extensive studies into this novel application.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。