EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking

TL;DR

EquiBench is a new benchmark designed to evaluate large language models' ability to understand program semantics through equivalence checking, revealing current models' limitations in semantic reasoning.

Contribution

We introduce EquiBench, a comprehensive benchmark with high-confidence program pairs for assessing LLMs' semantic reasoning in code.

Findings

State-of-the-art LLMs achieve modest accuracy on EquiBench.

Models often rely on syntactic cues rather than semantic understanding.

Current models show significant room for improvement in reasoning about program semantics.

Abstract

As large language models (LLMs) become integral to code-related tasks, a central question emerges: Do LLMs truly understand program semantics? We introduce EquiBench, a new benchmark for evaluating LLMs through equivalence checking, i.e., determining whether two programs produce identical outputs for all possible inputs. Unlike prior code generation benchmarks, this task directly tests a model's ability to reason about program semantics. EquiBench consists of 2400 program pairs across four languages and six categories. These pairs are generated through program analysis, compiler scheduling, and superoptimization, ensuring high-confidence labels, nontrivial difficulty, and full automation. We evaluate 19 state-of-the-art LLMs and find that in the most challenging categories, the best accuracies are 63.8% and 76.2%, only modestly above the 50% random baseline. Further analysis reveals that models often rely on syntactic similarity rather than exhibiting robust reasoning about program semantics, highlighting current limitations. Our code and dataset are publicly available at https://github.com/Anjiang-Wei/equibench