一句话：通过形式化验证 LLM 的推理步骤并定位局部逻辑错误，为其循环不变式合成提供建设性反馈，显著提升成功率。
LLM 在“猜测-检查”范式中合成循环不变式时，验证失败往往只返回布尔结果，模型难以定位自身推理中的具体逻辑错误。本文提出一个框架：先让 LLM 针对失败验证条件生成逐步自然语言证明，再用 LLM 将证明步骤翻译成一阶逻辑蕴含式并自动检查；无效蕴含即精确定位推理缺陷，据此构造针对性反馈进行精化。作者实现工具 LORIS，在 460 个 C 程序主基准与 50 个含非线性性质的 C 程序基准上评估，主基准解决 445 个程序，成功率达 93.1%，并在非线性基准上展现稳健性。
We propose a novel framework that provides constructive feedback to an LLM in the “guess-and-check” paradigm by formally verifying its own thinking process and detecting local reasoning errors. We apply this framework to the loop invariant synthesis problem. We prompt the model to produce a step-by-step natural language proof justifying its thinking process for the failed verification condition of its generated loop invariants. Then, we use an LLM to translate the reasoning steps into first-order logic implications, which can be checked automatically. An invalid implication pinpoints the exact logical flaw in the LLM’s thinking process, which we then use to construct targeted feedback for refinement. We have implemented our approach in a tool called LORIS and evaluated it on a main benchmark suite of 460 C programs and an additional benchmark suite of 50 C programs each of which involves non-linear properties. On the main benchmark suite, LORIS solved 445 of the programs and achieved an overall success rate of 93.1%. LORIS also demonstrates robustness on the challenging non-linear benchmark suite.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2605-17914,
title = {Guiding LLM-Based Loop Invariant Synthesis via Feedback on Local Reasoning Errors},
author = {Tianchi Li and Zhenyu Yan and Junhao Liu and Peng Di and Xin Zhang},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {48},
number = {2},
year = {2026},
doi = {10.1145/3806652}
}