# HoarePrompt: Structural Reasoning About Program Correctness in Natural Language

arXiv: https://arxiv.org/abs/2503.19599 · HTML: https://mlsanity.com/paper/2503.19599/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning for agents, planning and code, one of 17 directions in LLM reasoning.
- Builds on 31 of its 60 references that are in the map.
- First posted on arXiv 25 Mar 2025.

## Placed in

- LLM reasoning / [Reasoning for agents, planning and code](https://mlsanity.com/lr/reasoning-for-agents-planning-and-code/)

## Builds on (most cited first, 30 of 31)

- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code](https://mlsanity.com/paper/2403.07974/) (2024)
- [Can LLMs Express Their Uncertainty? An Empirical Evaluation of Confidence Elicitation in LLMs](https://mlsanity.com/paper/2306.13063/) (2023)
- [Quantifying Language Models' Sensitivity to Spurious Features in Prompt Design or: How I learned to start worrying about prompt formatting](https://mlsanity.com/paper/2310.11324/) (2023)
- [CodeT: Code Generation with Generated Tests](https://mlsanity.com/paper/2207.10397/) (2022)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Ask Me Anything: A simple strategy for prompting language models](https://mlsanity.com/paper/2210.02441/) (2022)
- [On Memorization of Large Language Models in Logical Reasoning](https://mlsanity.com/paper/2410.23123/) (2024)
- [CodeElo: Benchmarking Competition-level Code Generation of LLMs with Human-comparable Elo Ratings](https://mlsanity.com/paper/2501.01257/) (2025)
- [Faithful Logical Reasoning via Symbolic Chain-of-Thought](https://mlsanity.com/paper/2405.18357/) (2024)
- [No More Manual Tests? Evaluating and Improving ChatGPT for Unit Test Generation](https://mlsanity.com/paper/2305.04207/) (2023)
- [Can Language Models Solve Olympiad Programming?](https://mlsanity.com/paper/2404.10952/) (2024)
- [GroupDebate: Enhancing the Efficiency of Multi-Agent Debate Using Group Discussion](https://mlsanity.com/paper/2409.14051/) (2024)
- [NExT: Teaching Large Language Models to Reason about Code Execution](https://mlsanity.com/paper/2404.14662/) (2024)
- [Reasoning Runtime Behavior of a Program with LLM: How Far Are We?](https://mlsanity.com/paper/2403.16437/) (2024)
- [What is the Role of Small Models in the LLM Era: A Survey](https://mlsanity.com/paper/2409.06857/) (2024)
- [ClarifyGPT: Empowering LLM-based Code Generation with Intention Clarification](https://mlsanity.com/paper/2310.10996/) (2023)
- [AgentCoder: Multi-Agent-based Code Generation with Iterative Testing and Optimisation](https://mlsanity.com/paper/2312.13010/) (2023)
- [CodeMind: Evaluating Large Language Models for Code Reasoning](https://mlsanity.com/paper/2402.09664/) (2024)
- [CodeJudge-Eval: Can Large Language Models be Good Judges in Code Understanding?](https://mlsanity.com/paper/2408.10718/) (2024)
- [CodeCoT: Tackling Code Syntax Errors in CoT Reasoning for Code Generation](https://mlsanity.com/paper/2308.08784/) (2023)
- [Large Language Models as Test Case Generators: Performance Evaluation and Enhancement](https://mlsanity.com/paper/2404.13340/) (2024)
- [Training on the Benchmark Is Not All You Need](https://mlsanity.com/paper/2409.01790/) (2024)
- [Verified Code Transpilation with LLMs](https://mlsanity.com/paper/2406.03003/) (2024)
- [ProBench: Benchmarking Large Language Models in Competitive Programming](https://mlsanity.com/paper/2502.20868/) (2025)
- [The Program Testing Ability of Large Language Models for Code](https://mlsanity.com/paper/2310.05727/) (2023)
- [CoCoST: Automatic Complex Code Generation with Online Searching and Correctness Testing](https://mlsanity.com/paper/2403.13583/) (2024)
- [Can Large Language Models Act as Symbolic Reasoners?](https://mlsanity.com/paper/2410.21490/) (2024)
- [Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation](https://mlsanity.com/paper/2311.10483/) (2023)
- [Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK](https://mlsanity.com/paper/2502.07728/) (2025)

## Built on by (most cited first, 7 of 7)

- [Evaluating Code Reasoning Abilities of Large Language Models Under Real-World Settings](https://mlsanity.com/paper/2512.14917/) (2025)
- [Teaching Code LLMs to Reason with Intermediate Formal Specifications](https://mlsanity.com/paper/2607.04232/) (2026)
- [Viverra: Text-to-Code with Guarantees](https://mlsanity.com/paper/2605.14972/) (2026)
- [Inferring Code Correctness from Specification](https://mlsanity.com/paper/2605.29822/) (2026)
- [Rethinking Complexity Metrics for LLM-Integrated Applications: Beyond Source Code](https://mlsanity.com/paper/2607.01903/) (2026)
- [Grounding AI Agents in Contracts: An Empirical Evaluation of Spec-Driven Test Generation](https://mlsanity.com/paper/2608.17177/) (2026)
- [SkillSpec: Intent-Masked Specification Reasoning for Agent Skill Correctness](https://mlsanity.com/paper/2609.06052/) (2026)

## Abstract (arXiv)

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 from 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.