Verifying the correctness of programs written in natural language for software requirements is a challenging problem. Large-scale language models (LLMs) are promising candidates for this task, but they often fail to detect even simple bugs. In this paper, we present HoarePrompt, a novel approach that applies the fundamental ideas of program verification to natural language documents. Inspired by strongest postconditional calculus, HoarePrompt uses LLMs to stepwise generate natural language descriptions of program states reachable from various code points. To manage loops, we propose few-shot-driven k-induction, which adapts the k-induction method widely used in model checking. Once program states are described, HoarePrompt leverages LLMs to assess whether the annotated program complies with the natural language requirements. To evaluate the quality of program correctness classifiers for natural language requirements, we constructed a challenging dataset called CoCoClaNeL, consisting of solutions to programming competition problems. Experimental results show that HoarePrompt improves MCC by 61% compared to directly using Zero-shot-CoT prompts for classification accuracy, and improves MCC by 106% compared to a classifier that evaluates accuracy using LLM-based test generation. The inductive inference mechanism improves MCC by 26%, highlighting the effectiveness of loop management.
