用等价检测评估大模型对程序语义的理解能力
EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking
- 通过程序等价性判断测试模型对语义的推理能力
- 最难点上最佳模型准确率仅63.8%至76.2%
- 适合关注代码理解与逻辑推理的开发者
随着大语言模型（LLMs）在代码任务中日益重要，一个核心问题浮现：它们是否真正理解程序语义？我们提出 EquiBench，一个通过等价检查评估 LLMs 的新基准，即判断两个程序是否对所有输入产生相同输出。与以往代码生成基准不同，该任务直接检验模型对程序语义的推理能力。EquiBench 包含跨四种语言、六类的 2400 组程序对，由程序分析、编译器调度和超优化生成，确保标签高置信度、难度非平凡且全自动化。我们评估了 19 个前沿 LLMs，发现最挑战类别中最佳准确率为 63.8% 和 76.2%，仅略高于 50% 随机基线。进一步分析表明，模型常依赖语法相似性而非稳健的语义推理，凸显当前局限。代码与数据集已公开于 https://github.com/Anjiang-Wei/equibench
原文摘要 · Abstract (English)
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
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。