Evaluating Program Semantics Reasoning with Type Inference in System F
This addresses the need for formal evaluation of LLM reasoning in software engineering, though it is incremental as it introduces a new benchmark rather than a novel method.
The authors tackled the problem of evaluating whether large language models genuinely reason about program semantics rather than exploiting superficial associations, by introducing TF-Bench, a benchmark based on type inference in System F. Their analysis revealed substantial limitations, with the best-performing LLM achieving only 55.85% accuracy on a purely semantics-driven variant.
Large Language Models (LLMs) are increasingly integrated into the software engineering ecosystem. Their test-time compute (TTC) reasoning capabilities show significant potential for understanding program logic and semantics beyond mere token recognition. However, current benchmarks for code reasoning lack a formal, program-centric deductive framework to ensure sound evaluation, and are incapable of assessing whether models genuinely reason about program semantics or merely exploit superficial associations between natural language and code tokens. To bridge this gap, we introduce TF-Bench, a benchmark designed to evaluate LLM reasoning based on type inference in System F, a task we refer to as program semantics reasoning. By employing verified transformations to remove semantically irrelevant natural language, we construct TF-Bench_pure, a purely semantics-driven variant of TF-Bench. Our analysis reveals substantial limitations in state-of-the-art LLMs, with the best-performing LLM (Claude-3.7-sonnet) achieving only 55.85% accuracy on TF-Bench_pure. Additionally, we propose two novel metrics to assess robustness and the effectiveness of test-time reasoning, underscoring critical limitations in current LLM capabilities and highlighting essential directions for future research.