Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters

• URL: http://arxiv.org/abs/2503.12686v2
• Date: Tue, 30 Sep 2025 01:21:46 GMT
• Title: Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters
• Authors: Jacqueline L. Mitchell, Brian Hyeongseok Kim, Chenyu Zhou, Chao Wang,
• Abstract summary: We introduce two novel prompting strategies that aim to elicit such reasoning from large language models (LLMs)<n>We evaluate these strategies across several state-of-the-art LLMs on 22 programs from the SV-COMP benchmark suite widely used in software verification.
• Score: 5.468061853910803
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) are increasingly used for program verification, and yet little is known about \emph{how} they reason about program semantics during this process. In this work, we focus on abstract interpretation based-reasoning for invariant generation and introduce two novel prompting strategies that aim to elicit such reasoning from LLMs. We evaluate these strategies across several state-of-the-art LLMs on 22 programs from the SV-COMP benchmark suite widely used in software verification. We analyze both the soundness of the generated invariants and the key thematic patterns in the models' reasoning errors. This work aims to highlight new research opportunities at the intersection of LLMs and program verification for applying LLMs to verification tasks and advancing their reasoning capabilities in this application.

Related papers

• LLM-based Vulnerability Discovery through the Lens of Code Metrics [6.339440992743381]
  Large language models (LLMs) excel in many tasks of software engineering.<n> progress in leveraging them for vulnerability discovery has stalled in recent years.
  arXiv  Detail & Related papers  (2025-09-23T15:03:05Z)
• Do Code Semantics Help? A Comprehensive Study on Execution Trace-Based Information for Code Large Language Models [24.14163275602762]
  We focus on investigating the usefulness of trace-based semantic information in boosting supervised fine-tuning(SFT) and post-phase inference of Code LLMs.<n>The experimental results surprisingly disagree with previous works and demonstrate that semantic information has limited usefulness for SFT and test time scaling of Code LLM.
  arXiv  Detail & Related papers  (2025-09-15T08:38:01Z)
• Iterative In-Context Learning to Enhance LLMs Abstract Reasoning: The Case-Study of Algebraic Tasks [40.48180253367968]
  We introduce an in-context learning methodology that improves the generalization capabilities of general purpose LLMs.<n>Our approach employs an iterative example selection strategy, which incrementally constructs a tailored set of few-shot examples.<n>Our experiments reveal that some LLMs achieve better generalization performances when prompted with simpler few-shot examples.
  arXiv  Detail & Related papers  (2025-09-01T08:54:45Z)
• Reasoning-Aligned Perception Decoupling for Scalable Multi-modal Reasoning [95.44766931218896]
  Multi-modal large language models (MLLMs) still lag behind text-based reasoning.<n>We introduce Perception-Reasoning Decoupling, which modularizes the MLLM's reasoning component and makes it easily replaceable.<n>We propose a novel reinforcement learning algorithm called Visual Perception Optimization (VPO) to align the MLLM's perceptual output with the final reasoning task.
  arXiv  Detail & Related papers  (2025-06-05T02:28:07Z)
• Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference [0.9319432628663639]
  Large Language Models (LLMs) are increasingly being used to automate programming tasks.<n>This paper introduces FormalBench, a benchmark designed to evaluate LLMs' reasoning abilities on program semantics.<n>Using this benchmark, we evaluated the ability of LLMs in synthesizing consistent and complete specifications.
  arXiv  Detail & Related papers  (2025-02-22T13:27:31Z)
• Embodied Agent Interface: Benchmarking LLMs for Embodied Decision Making [85.24399869971236]
  We aim to evaluate Large Language Models (LLMs) for embodied decision making.<n>Existing evaluations tend to rely solely on a final success rate.<n>We propose a generalized interface (Embodied Agent Interface) that supports the formalization of various types of tasks.
  arXiv  Detail & Related papers  (2024-10-09T17:59:00Z)
• Evaluating the Correctness of Inference Patterns Used by LLMs for Judgment [53.17596274334017]
  We evaluate the correctness of the detailed inference patterns of an LLM behind its seemingly correct outputs.<n>Experiments show that even when the language generation results appear correct, a significant portion of the inference patterns used by the LLM for the legal judgment may represent misleading or irrelevant logic.
  arXiv  Detail & Related papers  (2024-10-06T08:33:39Z)
• Can Large Language Models Understand Symbolic Graphics Programs? [136.5639211254501]
  Symbolic graphics programs are popular in computer graphics.<n>We create a benchmark for the semantic visual understanding of symbolic graphics programs.<n>We find that LLMs considered stronger at reasoning generally perform better.
  arXiv  Detail & Related papers  (2024-08-15T17:59:57Z)
• Large Language Models are Interpretable Learners [53.56735770834617]
  In this paper, we show a combination of Large Language Models (LLMs) and symbolic programs can bridge the gap between expressiveness and interpretability. The pretrained LLM with natural language prompts provides a massive set of interpretable modules that can transform raw input into natural language concepts. As the knowledge learned by LSP is a combination of natural language descriptions and symbolic rules, it is easily transferable to humans (interpretable) and other LLMs.
  arXiv  Detail & Related papers  (2024-06-25T02:18:15Z)
• Can LLM Graph Reasoning Generalize beyond Pattern Memorization? [46.93972334344908]
  We evaluate whether large language models (LLMs) can go beyond semantic, numeric, structural, reasoning patterns in the synthetic training data and improve utility on real-world graph-based tasks. We find that while post-training alignment is most promising for real-world tasks, empowering LLM graph reasoning to go beyond pattern remains an open research question.
  arXiv  Detail & Related papers  (2024-06-23T02:59:15Z)
• Q*: Improving Multi-step Reasoning for LLMs with Deliberative Planning [53.6472920229013]
  Large Language Models (LLMs) have demonstrated impressive capability in many natural language tasks. LLMs are prone to produce errors, hallucinations and inconsistent statements when performing multi-step reasoning. We introduce Q*, a framework for guiding LLMs decoding process with deliberative planning.
  arXiv  Detail & Related papers  (2024-06-20T13:08:09Z)
• A Survey Study on the State of the Art of Programming Exercise Generation using Large Language Models [0.0]
  This paper analyzes Large Language Models (LLMs) with regard to their programming exercise generation capabilities. Through a survey study, we defined the state of the art, extracted their strengths and weaknesses and proposed an evaluation matrix.
  arXiv  Detail & Related papers  (2024-05-30T15:49:34Z)
• VURF: A General-purpose Reasoning and Self-refinement Framework for Video Understanding [65.12464615430036]
  This paper introduces a Video Understanding and Reasoning Framework (VURF) based on the reasoning power of Large Language Models (LLMs)<n>Ours is a novel approach to extend the utility of LLMs in the context of video tasks, leveraging their capacity to generalize from minimal input and output demonstrations within a contextual framework.
  arXiv  Detail & Related papers  (2024-03-21T18:00:00Z)
• FAC$^2$E: Better Understanding Large Language Model Capabilities by Dissociating Language and Cognition [56.76951887823882]
  Large language models (LLMs) are primarily evaluated by overall performance on various text understanding and generation tasks. We present FAC$2$E, a framework for Fine-grAined and Cognition-grounded LLMs' Capability Evaluation.
  arXiv  Detail & Related papers  (2024-02-29T21:05:37Z)
• Rethinking Interpretability in the Era of Large Language Models [76.1947554386879]
  Large language models (LLMs) have demonstrated remarkable capabilities across a wide array of tasks. The capability to explain in natural language allows LLMs to expand the scale and complexity of patterns that can be given to a human. These new capabilities raise new challenges, such as hallucinated explanations and immense computational costs.
  arXiv  Detail & Related papers  (2024-01-30T17:38:54Z)
• LLMs for Relational Reasoning: How Far are We? [8.840750655261251]
  Large language models (LLMs) have revolutionized many areas by achieving state-of-the-art performance on downstream tasks. Recent efforts have demonstrated that the LLMs are poor at solving sequential decision-making problems.
  arXiv  Detail & Related papers  (2024-01-17T08:22:52Z)
• LogicAsker: Evaluating and Improving the Logical Reasoning Ability of Large Language Models [63.14196038655506]
  We introduce LogicAsker, a novel approach for evaluating and enhancing the logical reasoning capabilities of large language models (LLMs) Our methodology reveals significant gaps in LLMs' learning of logical rules, with identified reasoning failures ranging from 29% to 90% across different models. We leverage these findings to construct targeted demonstration examples and fine-tune data, notably enhancing logical reasoning in models like GPT-4o by up to 5%.
  arXiv  Detail & Related papers  (2024-01-01T13:53:53Z)
• Breaking the Silence: the Threats of Using LLMs in Software Engineering [12.368546216271382]
  Large Language Models (LLMs) have gained considerable traction within the Software Engineering (SE) community. This paper initiates an open discussion on potential threats to the validity of LLM-based research.
  arXiv  Detail & Related papers  (2023-12-13T11:02:19Z)
• LM-Polygraph: Uncertainty Estimation for Language Models [71.21409522341482]
  Uncertainty estimation (UE) methods are one path to safer, more responsible, and more effective use of large language models (LLMs) We introduce LM-Polygraph, a framework with implementations of a battery of state-of-the-art UE methods for LLMs in text generation tasks, with unified program interfaces in Python. It introduces an extendable benchmark for consistent evaluation of UE techniques by researchers, and a demo web application that enriches the standard chat dialog with confidence scores.
  arXiv  Detail & Related papers  (2023-11-13T15:08:59Z)
• In-Context Explainers: Harnessing LLMs for Explaining Black Box Models [28.396104334980492]
  Large Language Models (LLMs) have demonstrated exceptional capabilities in complex tasks like machine translation, commonsense reasoning, and language understanding. One of the primary reasons for the adaptability of LLMs in such diverse tasks is their in-context learning (ICL) capability, which allows them to perform well on new tasks by simply using a few task samples in the prompt. We propose a novel framework, In-Context Explainers, comprising of three novel approaches that exploit the ICL capabilities of LLMs to explain the predictions made by other predictive models.
  arXiv  Detail & Related papers  (2023-10-09T15:31:03Z)
• Towards LogiGLUE: A Brief Survey and A Benchmark for Analyzing Logical Reasoning Capabilities of Language Models [56.34029644009297]
  Large language models (LLMs) have demonstrated the ability to overcome various limitations of formal Knowledge Representation (KR) systems. LLMs excel most in abductive reasoning, followed by deductive reasoning, while they are least effective at inductive reasoning. We study single-task training, multi-task training, and "chain-of-thought" knowledge distillation fine-tuning technique to assess the performance of model.
  arXiv  Detail & Related papers  (2023-10-02T01:00:50Z)
• LMs: Understanding Code Syntax and Semantics for Code Analysis [25.508254718438636]
  We evaluate the capabilities of large language models (LLMs) and their limitations for code analysis in software engineering. We employ four state-of-the-art foundational models, GPT4, GPT3.5, StarCoder and CodeLlama-13b-instruct.
  arXiv  Detail & Related papers  (2023-05-20T08:43:49Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.