Research map / Large language models / Agents, code and math
Evaluating Program Semantics Reasoning with Type Inference in System $F$
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Introduces TF-Bench, a benchmark of 188 Haskell type-inference tasks in System F (plus an NL-stripped variant TF-Bench-pure) to evaluate program semantics reasoning in LLMs, with robustness and reasoning-effectiveness metrics.
Problem
Existing code reasoning benchmarks cannot isolate whether LLMs reason about program semantics or exploit natural-language and identifier cues, and lack a formal deductive oracle.
Approach
Use type inference in System F/Haskell Prelude functions as an upstream reasoning task with verifiable alpha-equivalence oracle, and apply alpha-rewrites that remove NL types, type variables and binding names to create a purely semantic variant; propose Robustness Score and Reasoning Effectiveness metrics.
Key results
- Claude-3.7-sonnet achieves 55.85% accuracy on TF-Bench-pure, the best on the NL-free variant, versus 90.42% on TF-Bench.
- Qwen3-32B reaches 87.94% on TF-Bench; GPT-O3 has the highest robustness score (64.29).
- Reasoning effectiveness is 3.90 for Gemini-2.5-flash and 3.41 for Claude-3.7-sonnet; fine-tuning on code sometimes lowers accuracy while math fine-tuning consistently helps.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Remove natural-language elements with alpha-rewrite (ablation) | evaluated LLMs · TF-Bench versus TF-Bench pure | accuracy | Hurt |
| Enable test-time compute reasoning (ablation) | Claude-3.7-sonnet · TF-Bench | accuracy: 87.77 -> 90.42 | Helped |
| Enable test-time compute reasoning (ablation) | Claude-3.7-sonnet · TF-Bench pure | accuracy: 46.81 -> 55.85 | Helped |
| Enable test-time compute reasoning (ablation) | Gemini-2.5-flash · TF-Bench | accuracy: 78.19 -> 83.51 | Helped |
| Enable test-time compute reasoning (ablation) | Gemini-2.5-flash · TF-Bench pure | accuracy: 30.32 -> 51.06 | Helped |
| Enable test-time compute reasoning (ablation) | Qwen3-235B-FP8 · TF-Bench | accuracy: 80.49 -> 86.70 | Helped |
| Enable test-time compute reasoning (ablation) | Qwen3-235B-FP8 · TF-Bench pure | accuracy: 35.64 -> 44.15 | Helped |
| Fine-tune on code (ablation) | Qwen2.5-7B · TF-Bench | accuracy: 65.96 -> 61.17; decrease 4.79 | Hurt |
| Fine-tune on code (ablation) | Codestral-22B (Mistral-22B) · TF-Bench pure | accuracy: 19.68 -> 11.17; decrease 8.51 | Hurt |
| Fine-tune on code (ablation) | Qwen2.5-Coder-32B (Qwen2.5-32B) · TF-Bench pure | accuracy: 36.17 -> 31.91; decrease 4.26 | Hurt |
| Fine-tune on math (ablation) | Mistral-7B and Qwen2-7B/72B · TF-Bench pure | accuracy: 7.99 -> 15.43; 3.19 -> 10.64; 21.81 -> 33.51 | Helped |
| Fine-tune on code (ablation) | DeepSeek-V2-16B/236B · TF-Bench | accuracy: 29.79 -> 55.32; 38.30 -> 80.85 | Helped |
Surprising findings
- Fine-tuning on code data sometimes decreases accuracy (e.g., Qwen2.5-7B drops 4.79 points on TF-Bench), while math fine-tuning consistently improves performance.
- Smaller distilled GPT-5 variants match GPT-5 on TF-Bench but perform substantially worse on TF-Bench-pure.
Limitations
- Benchmark limited to 188 function-level tasks drawn from the Haskell Prelude, which may be memorized by models trained on public code.
- Open-weight models were run via Ollama on 8 H100s; some models used API access (DeepSeek) due to compute limits.
- Fine-tuning analysis pairs are not exact base-model matches (Qwen2-Math vs Qwen2.5-Coder).
Experimental setup
Datasets: Haskell Prelude (ghc-internal) functions
Benchmarks: TF-Bench TF-Bench-pure
Metrics: accuracy alpha-equivalence accuracy robustness score reasoning effectiveness
Baselines: Claude-3.7-sonnet GPT-O3 GPT-O1 DeepSeek-R1 Gemini-2.5-pro Qwen3-32B
Builds on: Hindley-Milner type inference System F Curry-Howard isomorphism
Closest papers by meaning
- CoRe: Benchmarking LLMs’ Code Reasoning Capabilities through Static Analysis Tasks (NeurIPS 2025 · similarity 0.91)
- TypyBench: Evaluating LLM Type Inference for Untyped Python Repositories (ICML 2025 · similarity 0.89)
- Lemur: Integrating Large Language Models in Automated Program Verification (ICLR 2024 · similarity 0.89)
- SemCoder: Training Code Language Models with Comprehensive Semantics Reasoning (NeurIPS 2024 · similarity 0.88)
- Verified Code Transpilation with LLMs (NeurIPS 2024 · similarity 0.87)
- Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages (NeurIPS 2024 · similarity 0.86)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.