# Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference

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

## Key facts

- Cited by 16 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning for agents, planning and code, one of 17 directions in LLM reasoning.
- Builds on 23 of its 50 references that are in the map.
- First posted on arXiv 22 Feb 2025.

## Placed in

- LLM reasoning / [Reasoning for agents, planning and code](https://mlsanity.com/lr/reasoning-for-agents-planning-and-code/)

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

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Large Language Models are Zero-Shot Reasoners](https://mlsanity.com/paper/2205.11916/) (2022)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code](https://mlsanity.com/paper/2403.07974/) (2024)
- [Least-to-Most Prompting Enables Complex Reasoning in Large Language Models](https://mlsanity.com/paper/2205.10625/) (2022)
- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [CodeBERT: A Pre-Trained Model for Programming and Natural Languages](https://mlsanity.com/paper/2002.08155/) (2020)
- [Qwen2.5-Coder Technical Report](https://mlsanity.com/paper/2409.12186/) (2024)
- [DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence](https://mlsanity.com/paper/2401.14196/) (2024)
- [DeepSeek-V2: A Strong, Economical, and Efficient Mixture-of-Experts Language Model](https://mlsanity.com/paper/2405.04434/) (2024)
- [CodeSearchNet Challenge: Evaluating the State of Semantic Code Search](https://mlsanity.com/paper/1909.09436/) (2019)
- [Multi-lingual Evaluation of Code Generation Models](https://mlsanity.com/paper/2210.14868/) (2022)
- [Can Large Language Models Infer Causation from Correlation?](https://mlsanity.com/paper/2306.05836/) (2023)
- [Refining ChatGPT-Generated Code: Characterizing and Mitigating Code Quality Issues](https://mlsanity.com/paper/2307.12596/) (2023)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [Reasoning Runtime Behavior of a Program with LLM: How Far Are We?](https://mlsanity.com/paper/2403.16437/) (2024)
- [On the Generalizability of Neural Program Models with respect to Semantic-Preserving Program Transformations](https://mlsanity.com/paper/2008.01566/) (2020)
- [On the "Naturalness" of Buggy Code](https://mlsanity.com/paper/1506.01159/) (2015)
- [Ranking LLM-Generated Loop Invariants for Program Verification](https://mlsanity.com/paper/2310.09342/) (2023)
- [Robustness, Security, Privacy, Explainability, Efficiency, and Usability of Large Language Models for Code](https://mlsanity.com/paper/2403.07506/) (2024)
- [Challenging Machine Learning-based Clone Detectors via Semantic-preserving Code Transformations](https://mlsanity.com/paper/2111.10793/) (2021)
- [Towards Reliable Evaluation of Neural Program Repair with Natural Robustness Testing](https://mlsanity.com/paper/2402.11892/) (2024)

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

- [AI Agentic Programming: A Survey of Techniques, Challenges, and Opportunities](https://mlsanity.com/paper/2508.11126/) (2025)
- [The Hitchhiker's Guide to Program Analysis, Part II: Deep Thoughts by LLMs](https://mlsanity.com/paper/2504.11711/) (2025)
- [CodeReasoner: Enhancing the Code Reasoning Ability with Reinforcement Learning](https://mlsanity.com/paper/2507.17548/) (2025)
- [CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation](https://mlsanity.com/paper/2604.12268/) (2026)
- [Evaluating Code Reasoning Abilities of Large Language Models Under Real-World Settings](https://mlsanity.com/paper/2512.14917/) (2025)
- [AutoReSpec: A Framework for Generating Specification using Large Language Models](https://mlsanity.com/paper/2604.03758/) (2026)
- [VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation](https://mlsanity.com/paper/2605.08553/) (2026)
- [Evaluating Program Semantics Reasoning with Type Inference in System F](https://mlsanity.com/paper/2509.23686/) (2025)
- [Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability](https://mlsanity.com/paper/2604.00280/) (2026)
- [Perish or Flourish? A Holistic Evaluation of Large Language Models for Code Generation in Functional Programming](https://mlsanity.com/paper/2601.02060/) (2026)
- [From Benchmark Data To Applicable Program Repair: An Experience Report](https://mlsanity.com/paper/2508.16071/) (2025)
- [Enhancing Neural Code Representation with Additional Context](https://mlsanity.com/paper/2510.12082/) (2025)
- [SpecPylot: Python Specification Generation using Large Language Models](https://mlsanity.com/paper/2604.16560/) (2026)
- [Self-Spec Verifiable Code Generation](https://mlsanity.com/paper/2609.39568/) (2026)
- [Does Every User Need a Private LoRA? Decoupling Personalization from Per-User Adaptation](https://mlsanity.com/paper/2610.02353/) (2026)
- [SpecGuardBench: Can Coding Agents Construct Reliable Validation Harnesses from Natural Language Specifications?](https://mlsanity.com/paper/2610.16870/) (2026)

## Abstract (arXiv)

Large Language Models (LLMs) are increasingly being used to automate programming tasks. Yet, LLMs' capabilities in reasoning about program semantics are still inadequately studied, leaving significant potential for further exploration. This paper introduces FormalBench, a comprehensive benchmark designed to evaluate LLMs' reasoning abilities on program semantics, particularly via the task of synthesizing formal program specifications to assist verifying program correctness. This task requires both comprehensive reasoning over all possible program executions and the generation of precise, syntactically correct expressions that adhere to formal syntax and semantics. Using this benchmark, we evaluated the ability of LLMs in synthesizing consistent and complete specifications. Our findings show that LLMs perform well with simple control flows but struggle with more complex structures, especially loops, even with advanced prompting. Additionally, LLMs exhibit limited robustness against semantic-preserving transformations. We also highlight common failure patterns and design self-repair prompts, improving success rates by 25%.