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

• URL: http://arxiv.org/abs/2503.04779v3
• Date: Sat, 15 Mar 2025 10:45:06 GMT
• Title: Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference
• Authors: Thanh Le-Cong, Bach Le, Toby Murray,
• Abstract summary: 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.
• Score: 0.9319432628663639
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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%.

Related papers

• Can LLMs Formally Reason as Abstract Interpreters for Program Analysis? [2.520295252080748]
  LLMs have impressive capabilities in code generation and comprehension, but their potential in program analysis remains under-explored. We systematically investigate whether LLMs can reason about programs using a program analysis framework called abstract interpretation. We validate our approach using state-of-the-art LLMs on 22 challenging benchmark programs from the Software Verification Competition (SV-COMP) 2019 dataset. Our results show that our strategies are able to elicit abstract interpretation-based reasoning in the tested models, but LLMs are susceptible to logical errors.
  arXiv  Detail & Related papers  (2025-03-16T23:05:52Z)
• CRANE: Reasoning with constrained LLM generation [5.971462597321995]
  We propose a reasoning-augmented constrained decoding algorithm, CRANE, which balances correctness of constrained generation with flexibility of unconstrained generation.<n> CRANE significantly outperforms both state-of-the-art constrained decoding strategies and standard unconstrained decoding.
  arXiv  Detail & Related papers  (2025-02-13T08:23:42Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  Large language models (LLMs) struggle with consistent and accurate reasoning. LLMs are trained primarily on correct solutions, reducing their ability to detect and learn from errors. We propose a novel collaborative method integrating Chain-of-Thought (CoT) and Program-of-Thought (PoT) solutions for verification.
  arXiv  Detail & Related papers  (2024-10-05T05:21:48Z)
• SpecEval: Evaluating Code Comprehension in Large Language Models via Program Specifications [12.683365968483807]
  We propose SpecEval to evaluate code comprehension in large language models via program specifications. We employ formal specifications to represent program semantics and perform thorough evaluations. In particular, four specification-related tasks are designed to assess the capability of LLMs from basic to advanced levels.
  arXiv  Detail & Related papers  (2024-09-19T16:08:39Z)
• 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)
• Toward Self-Improvement of LLMs via Imagination, Searching, and Criticizing [56.75702900542643]
  We introduce AlphaLLM for the self-improvements of Large Language Models.<n>It integrates Monte Carlo Tree Search (MCTS) with LLMs to establish a self-improving loop.<n>Our experimental results show that AlphaLLM significantly enhances the performance of LLMs without additional annotations.
  arXiv  Detail & Related papers  (2024-04-18T15:21:34Z)
• 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)
• If LLM Is the Wizard, Then Code Is the Wand: A Survey on How Code Empowers Large Language Models to Serve as Intelligent Agents [81.60906807941188]
  Large language models (LLMs) are trained on a combination of natural language and formal language (code) Code translates high-level goals into executable steps, featuring standard syntax, logical consistency, abstraction, and modularity.
  arXiv  Detail & Related papers  (2024-01-01T16:51:20Z)
• 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)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  We propose a new satisfiability-aided language modeling (SatLM) approach for improving the reasoning capabilities of large language models (LLMs) We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. We evaluate SATLM on 8 different datasets and show that it consistently outperforms program-aided LMs in the imperative paradigm.
  arXiv  Detail & Related papers  (2023-05-16T17:55:51Z)

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.