{"ID":6620552,"CreatedAt":"2026-07-15T01:01:48.440468303Z","UpdatedAt":"2026-07-15T03:28:55.185153975Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2607.12490","arxiv_id":"2607.12490","title":"When is LLM-Based Program Reasoning Correct? A Completion Semantics for LLM-Based Code Inference","abstract":"Due to token and cognitive limits, Large Language Models (LLMs) typically perform program reasoning over incomplete code fragments/prompts rather than complete programs. Such reasoning therefore must rely on {assumptions about omitted code and context. As a result, the meaning of an inference over a program fragment is not absolute, but depends on an implicit completion model describing how the fragment may be refined into a complete program. In this paper, we introduce completion semantics for LLM-based program reasoning. We formalize incomplete programs as denoting a space of possible refinements and define the correctness of existential inferences relative to a completion model. Under this view, a reported bug is correct whenever there exists a completion within the model that witnesses the bug. This perspective explains why many LLM-generated reports are neither simply correct nor incorrect, but instead depend on assumptions about omitted context. We have instantiated our approach in the form of a witness-generation workflow that concretizes completions underlying an inference by constructing executable refinements of the original program fragment. Witnesses serve both as evidence for existential claims and as a mechanism for exposing the assumptions required to support them. We evaluate our approach on real-world LLM-generated bug reports and program-analysis tasks. Our results show that witness generation effectively distinguishes inferences supported by plausible completions from those requiring unrealistic assumptions, providing a practical mechanism for validating reasoning over incomplete programs.","short_abstract":"Due to token and cognitive limits, Large Language Models (LLMs) typically perform program reasoning over incomplete code fragments/prompts rather than complete programs. Such reasoning therefore must rely on {assumptions about omitted code and context. As a result, the meaning of an inference over a program fragment is...","url_abs":"https://arxiv.org/abs/2607.12490","url_pdf":"https://arxiv.org/pdf/2607.12490v1","authors":"[\"Zhiyuan Liu\",\"Yihe Li\",\"Trevor E. Carlson\",\"Huiyan Wang\",\"Ruijie Meng\",\"Gregory J. Duck\"]","published":"2026-07-14T08:23:24Z","proceeding":"cs.PL","tasks":"[\"cs.PL\"]","methods":"[\"Large Language Model\",\"Language Model\"]","has_code":false}