一句话：提出 HoarePrompt，将最强后置条件与 k-归纳引入 LLM，用自然语言推理程序对需求的正确性。
该论文关注依据自然语言需求验证程序正确性这一困难且研究不足的问题，指出现有 LLM 即使对简单错误也常无法识别。HoarePrompt 从程序验证中汲取思想，模仿最强后置条件演算，让 LLM 逐步生成各代码点可达程序状态的自然语言描述，并用少样本驱动的 k-归纳处理循环。随后，LLM 基于这些状态注解判断程序是否符合自然语言需求。作者构建了 CoCoClaNeL 数据集，包含编程竞赛题解。实验表明，相比 Zero-shot-CoT，HoarePrompt 将正确性分类的 MCC 提升 61%；相比基于 LLM 测试生成的分类器提升 106%；归纳推理机制带来 26% 的 MCC 增益，证明其处理循环的有效性。
While software requirements are often expressed in natural language, verifying the correctness of a program against such requirements is a hard and underexplored problem. Large language models (LLMs) are promising candidates for addressing this challenge, however, our experience shows that they are ineffective in this task, often failing to detect even straightforward bugs. To address this gap, we introduce HoarePrompt, a novel approach that adapts fundamental ideas from program verification to natural language artifacts. Inspired by the strongest postcondition calculus, HoarePrompt employs a systematic, step-by-step process in which an LLM generates natural language descriptions of reachable program states at various code points. To manage loops, we propose few-shot-driven k-induction, an adaptation of the k-induction method widely used in model checking. Once program states are described, HoarePrompt leverages the LLM to assess whether the program, annotated with these state descriptions, conforms to the natural language requirements. For evaluating the quality of classifiers of program correctness with respect to natural language requirements, we constructed CoCoClaNeL, a challenging dataset of solutions to programming competition problems. Our experiments show that HoarePrompt improves the MCC by 61% compared to directly using Zero-shot-CoT prompts for correctness classification. Furthermore, HoarePrompt outperforms a classifier that assesses correctness via LLM-based test generation by an MCC increase of 106%. The inductive reasoning mechanism contributes a 26% boost to MCC, underscoring its effectiveness in managing loops.
@inproceedings{abs-2503-19599,
title = {HoarePrompt: Structural Reasoning About Program Correctness in Natural Language},
author = {Dimitrios Stamatios Bouras and Yihan Dai and Tairan Wang and Yingfei Xiong and Sergey Mechtaev},
booktitle = {ICSE},
year = {2026},
doi = {10.1145/3744916.3773206}
}