EquiBench: Benchmarking Large Language Models’ Understanding of Program Semantics via Equivalence Checking

要約

大規模な言語モデル（LLM）がコード関連のタスクに不可欠になると、中心的な問題が現れます。LLMはプログラム実行セマンティクスを本当に理解していますか？
等価チェックを通じてLLMを評価するための新しいベンチマークであるEquibenchを紹介します。つまり、2つのプログラムがすべての可能な入力に対して同一の出力を生成するかどうかを判断します。
以前のコード生成ベンチマークとは異なり、このタスクはコード実行セマンティクスに関するモデルの理解を直接テストします。
Equibenchは、4つの言語にわたる2400のプログラムペアと6つのカテゴリで構成されています。
これらのペアは、プログラム分析、コンパイラスケジューリング、および超最適化を通じて生成され、自信の高いラベル、非自明の難易度、および完全な自動化を確保します。
変換は、構文の編集、構造的修正、およびアルゴリズムの変化に及び、幅広いセマンティックバリエーションをカバーしています。
19の最先端のLLMを評価し、最も挑戦的なカテゴリでは、最高の精度は63.8％と76.2％であり、50％のランダムベースラインをわずかに上回っていることがわかります。
さらなる分析により、モデルは、実行セマンティクスよりも堅牢な推論を示すのではなく、構文の類似性に依存することが多く、基本的な制限を強調していることが明らかになりました。

要約(オリジナル)

As large language models (LLMs) become integral to code-related tasks, a central question emerges: do LLMs truly understand program execution 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 understanding of code execution 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. The transformations span syntactic edits, structural modifications, and algorithmic changes, covering a broad spectrum of semantic variation. 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 over execution semantics, highlighting fundamental limitations.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google