arXiv:2503.19599v1 宣传类型：交叉 摘要：虽然软件需求通常用自然语言表达，但验证程序是否符合自然语言需求是一个困难且尚未充分探索的问题。大型语言模型（LLMs）是解决这一挑战的有前景的方法，然而我们的经验表明，它们在这个任务中效果不佳，经常无法检测到甚至简单的错误。为了解决这一问题，我们引入了HoarePrompt，这是一种新颖的方法，将程序分析和验证的基本思想应用到自然语言的工件中。受到后件最强计算的启发，HoarePrompt采用了一种系统且逐步的过程，在此过程中，LLM生成代码各部分可达程序状态的自然语言描述。为了处理循环，我们提出了基于少样本学习的k-归纳法，这是广泛用于模型校验的k-归纳法的一种适应。一旦程序状态被描述，HoarePrompt利用LLM评估标注有这些状态描述的程序是否符合自然语言需求。为了评估对自然语言需求的程序正确性分类器的质量，我们构建了CoCoClaNeL，这是一个具有挑战性的数据集，包含编程比赛问题的解决方案。我们的实验表明，与直接使用零样本-CoT提示进行正确性分类相比，HoarePrompt将MCC提高了62%。此外，HoarePrompt通过将MCC提高93%，优于使用LLM基于测试生成进行正确性评估的分类器。归纳推理机制使得MCC提高了28%，突显了其在处理循环方面的有效性。