Pith. sign in

REVIEW 5 cited by

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

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2503.04779 v4 pith:ZJYDWI4E submitted 2025-02-22 cs.PL cs.AIcs.SE

Thanh Le-Cong , Bach Le , Toby Murray This is my paper · ORCID
classification cs.PLcs.AIcs.SE
keywords llmsprogramsemanticscomprehensiveformalreasoningbenchmarkspecifications
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original 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%.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 5 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. AfterVibe: What Remains When the Conversation Ends

    cs.SE 2026-07 conditional novelty 7.5 of 10

    AfterVibe extracts natural-language specs from vibe-coding trajectories, validates them via blind regeneration scored by a three-tier verifier, and reaches mean scores of 5.06–5.74/6 on 72 industrial tasks.

  2. TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation

    cs.SE 2026-07 conditional novelty 7.0 of 10

    An exact model-checker oracle for NL-to-TLA+ still yields an elevenfold “correctness envelope” (18.7%–1.7%) once interface supply and vacuity screens are made explicit.

  3. AutoReSpec: A Framework for Generating Specification using Large Language Models

    cs.SE 2026-04 conditional novelty 6.0 of 10

    AutoReSpec dynamically pairs LLMs by control-flow type and uses verifier-guided collaborative refinement to produce 67/72 verifiable JML specs with higher success probability and completeness than prior tools.

  4. CodeReasoner: Enhancing the Code Reasoning Ability with Reinforcement Learning

    cs.SE 2025-07 conditional novelty 6.0 of 10

    CodeReasoner combines a concise execution-focused dataset, instruction tuning, and GRPO RL to make 7B/14B models match or beat GPT-4o on code reasoning benchmarks.

  5. GenOS: Compositional Certificates for Semantic Robustness in AI Code Generation

    cs.PL 2026-08 accept novelty 5.0 of 10

    GenOS proves that equivalence-compatible Markov kernels in AI code generation pipelines compose, so equivalent prompts yield equal probabilities for observer-relative events like verified commit.

Pith tools