Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors

Tianchi Li, Zhenyu Yan, Junhao Liu +2

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 reas…