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

Understand

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.