Evaluating Program Semantics Reasoning with Type Inference in System F

📄 arXiv: 2509.23686v2 📥 PDF

作者: Yifeng He, Luning Yang, Christopher Castro Gaw Gonzalo, Hao Chen

分类: cs.CL, cs.PL, cs.SE

发布日期: 2025-09-28 (更新: 2025-10-20)

备注: NeurIPS '25, package released at: https://github.com/SecurityLab-UCD/TF-Bench

💡 一句话要点

提出TF-Bench基准测试，评估LLM在System F类型推断中的程序语义推理能力

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 程序语义推理 类型推断 System F 大语言模型 基准测试 代码理解 软件工程

📋 核心要点

  1. 现有代码推理基准缺乏形式化框架，难以评估LLM是否真正理解程序语义。
  2. 提出TF-Bench基准，基于System F类型推断评估LLM的程序语义推理能力。
  3. 实验表明，现有LLM在TF-Bench_pure上表现不佳，突显了其语义推理的局限性。

📝 摘要（中文）

大型语言模型（LLMs）正日益融入软件工程生态系统。它们的测试时计算（TTC）推理能力在理解程序逻辑和语义方面显示出巨大潜力，超越了单纯的token识别。然而，当前的代码推理基准缺乏形式化的、以程序为中心的演绎框架来确保可靠的评估，并且无法评估模型是否真正推理程序语义，还是仅仅利用自然语言和代码token之间的表面关联。为了弥合这一差距，我们引入了TF-Bench，这是一个旨在评估LLM基于System F类型推断的推理能力的基准，我们将此任务称为程序语义推理。通过采用经过验证的转换来消除语义上不相关的自然语言，我们构建了TF-Bench_pure，这是TF-Bench的一个纯粹由语义驱动的变体。我们的分析揭示了最先进的LLM的重大局限性，其中性能最佳的LLM（Claude-3.7-sonnet）在TF-Bench_pure上仅达到55.85%的准确率。此外，我们提出了两个新的指标来评估鲁棒性和测试时推理的有效性，强调了当前LLM能力的 критические 局限性，并突出了未来研究的重要方向。

🔬 方法详解

问题定义：现有的大语言模型在代码理解和推理方面展现出潜力，但现有的代码推理基准测试往往依赖于自然语言描述，这使得模型可能通过简单的token匹配而非真正的语义理解来完成任务。因此，如何设计一个能够准确评估模型程序语义推理能力的基准测试是一个关键问题。现有方法的痛点在于无法区分模型是基于语义理解还是表面关联进行推理。

核心思路：论文的核心思路是构建一个基于System F类型推断的基准测试，System F是一种具有良好形式化语义的类型化lambda演算。通过类型推断任务，可以迫使模型理解程序的语义，而不仅仅是表面语法。此外，通过移除语义无关的自然语言描述，可以进一步消除模型利用表面关联的可能性。

技术框架：TF-Bench基准测试包含两个主要部分：TF-Bench和TF-Bench_pure。TF-Bench包含带有自然语言描述的System F类型推断问题，而TF-Bench_pure则移除了这些自然语言描述，只保留纯粹的程序代码。整个流程包括：1) 生成System F类型推断问题；2) 对问题进行转换，生成TF-Bench和TF-Bench_pure两个版本；3) 使用LLM对问题进行解答；4) 评估LLM的准确率和鲁棒性。

关键创新：该论文最重要的技术创新点在于提出了TF-Bench_pure，这是一个完全基于程序语义的基准测试。通过移除自然语言描述，可以更准确地评估模型是否真正理解程序的语义。此外，论文还提出了两个新的指标来评估模型的鲁棒性和测试时推理的有效性。与现有方法相比，TF-Bench_pure能够更有效地消除模型利用表面关联的可能性，从而更准确地评估模型的程序语义推理能力。

关键设计：TF-Bench_pure的关键设计在于使用经过验证的转换来移除语义上不相关的自然语言。具体来说，论文采用了一系列规则来识别和移除自然语言描述，同时保证程序的语义不变。此外，论文还设计了两种新的评估指标：1) 鲁棒性指标，用于评估模型在面对程序代码微小变化时的表现；2) 测试时推理有效性指标，用于评估模型在测试时进行推理的能力。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，即使是性能最佳的LLM（Claude-3.7-sonnet）在TF-Bench_pure上的准确率也仅为55.85%，这表明现有LLM在程序语义推理方面存在显著局限性。此外，实验还表明，LLM在面对程序代码的微小变化时，鲁棒性较差，这进一步突出了其语义理解的不足。

🎯 应用场景

该研究成果可应用于提升大语言模型在软件开发领域的应用能力，例如代码自动补全、代码缺陷检测、程序验证等。通过更准确地评估模型的程序语义理解能力，可以推动LLM在软件工程领域的更广泛应用，并提高软件开发的效率和质量。未来的影响包括更智能化的软件开发工具和更可靠的软件系统。

📄 摘要（原文）

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.