# Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 18 of its 43 references that are in the map.
- First posted on arXiv 16 Mar 2025.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 18 of 18)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Llama 2: Open Foundation and Fine-Tuned Chat Models](https://mlsanity.com/paper/2307.09288/) (2023)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [Qwen2 Technical Report](https://mlsanity.com/paper/2407.10671/) (2024)
- [How to use and interpret activation patching](https://mlsanity.com/paper/2404.15255/) (2024)
- [HelpSteer2-Preference: Complementing Ratings with Preferences](https://mlsanity.com/paper/2410.01257/) (2024)
- [Algorithm of Thoughts: Enhancing Exploration of Ideas in Large Language Models](https://mlsanity.com/paper/2308.10379/) (2023)
- [Diagnostic Reasoning Prompts Reveal the Potential for Large Language Model Interpretability in Medicine](https://mlsanity.com/paper/2308.06834/) (2023)
- [Finding Inductive Loop Invariants using Large Language Models](https://mlsanity.com/paper/2311.07948/) (2023)
- [Ranking LLM-Generated Loop Invariants for Program Verification](https://mlsanity.com/paper/2310.09342/) (2023)
- [Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models](https://mlsanity.com/paper/2412.10483/) (2024)
- [Unsupervised Concept Vector Extraction for Bias Control in LLMs](https://mlsanity.com/paper/2502.19721/) (2025)
- [PromptExp: Multi-granularity Prompt Explanation of Large Language Models](https://mlsanity.com/paper/2410.13073/) (2024)
- [Frame Representation Hypothesis: Multi-Token LLM Interpretability and Concept-Guided Text Generation](https://mlsanity.com/paper/2412.07334/) (2024)
- [Interpretable Cross-Examination Technique (ICE-T): Using highly informative features to boost LLM performance](https://mlsanity.com/paper/2405.06703/) (2024)
- [Uniform Discretized Integrated Gradients: An effective attribution based method for explaining large language models](https://mlsanity.com/paper/2412.03886/) (2024)

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

- [GTA: Graph Theory Agent and Benchmark for Algorithmic Graph Reasoning with LLMs](https://mlsanity.com/paper/2609.12265/) (2026)

## Abstract (arXiv)

Large language models (LLMs) are increasingly used for program verification, and yet little is known about 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.