# Evaluating Program Semantics Reasoning with Type Inference in System F

arXiv: https://arxiv.org/abs/2509.23686 · HTML: https://mlsanity.com/paper/2509.23686/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning for agents, planning and code, one of 17 directions in LLM reasoning.
- Builds on 25 of its 103 references that are in the map.
- First posted on arXiv 28 Sep 2025.

## Placed in

- LLM reasoning / [Reasoning for agents, planning and code](https://mlsanity.com/lr/reasoning-for-agents-planning-and-code/)

## Builds on (most cited first, 25 of 25)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [Qwen2.5 Technical Report](https://mlsanity.com/paper/2412.15115/) (2024)
- [Mistral 7B](https://mlsanity.com/paper/2310.06825/) (2023)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [Qwen2 Technical Report](https://mlsanity.com/paper/2407.10671/) (2024)
- [Gemma 2: Improving Open Language Models at a Practical Size](https://mlsanity.com/paper/2408.00118/) (2024)
- [Phi-3 Technical Report: A Highly Capable Language Model Locally on Your Phone](https://mlsanity.com/paper/2404.14219/) (2024)
- [Mixtral of Experts](https://mlsanity.com/paper/2401.04088/) (2024)
- [s1: Simple test-time scaling](https://mlsanity.com/paper/2501.19393/) (2025)
- [DeepSeek-V2: A Strong, Economical, and Efficient Mixture-of-Experts Language Model](https://mlsanity.com/paper/2405.04434/) (2024)
- [WizardLM: Empowering large pre-trained language models to follow complex instructions](https://mlsanity.com/paper/2304.12244/) (2023)
- [Gemma: Open Models Based on Gemini Research and Technology](https://mlsanity.com/paper/2403.08295/) (2024)
- [GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models](https://mlsanity.com/paper/2410.05229/) (2024)
- [StarCoder 2 and The Stack v2: The Next Generation](https://mlsanity.com/paper/2402.19173/) (2024)
- [DeepSeek-Coder-V2: Breaking the Barrier of Closed-Source Models in Code Intelligence](https://mlsanity.com/paper/2406.11931/) (2024)
- [CodeGemma: Open Code Models Based on Gemma](https://mlsanity.com/paper/2406.11409/) (2024)
- [Marco-o1: Towards Open Reasoning Models for Open-Ended Solutions](https://mlsanity.com/paper/2411.14405/) (2024)
- [Granite Code Models: A Family of Open Foundation Models for Code Intelligence](https://mlsanity.com/paper/2405.04324/) (2024)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference](https://mlsanity.com/paper/2503.04779/) (2025)
- [LLAMAFUZZ: Large Language Model Enhanced Greybox Fuzzing](https://mlsanity.com/paper/2406.07714/) (2024)
- [ReasonAgain: Using Extractable Symbolic Programs to Evaluate Mathematical Reasoning](https://mlsanity.com/paper/2410.19056/) (2024)

## Built on by (most cited first, 2 of 2)

- [A Comprehensive Survey on Benchmarks and Solutions in Software Engineering of LLM-Empowered Agentic System](https://mlsanity.com/paper/2510.09721/) (2025)
- [CordisBench: Can Language Models Reason About Component Lifecycles in Dynamic Agent Harnesses?](https://mlsanity.com/paper/2609.01600/) (2026)

## Abstract (arXiv)

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.