# TREAT: Evaluating Access to Formal Knowledge across Equivalent Mathematical Representations

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 13 of its 21 references that are in the map.
- First posted on arXiv 29 Jul 2026.

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

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models](https://mlsanity.com/paper/2410.05229/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Proving Test Set Contamination in Black Box Language Models](https://mlsanity.com/paper/2310.17623/) (2023)
- [MATH-Perturb: Benchmarking LLMs' Math Reasoning Abilities against Hard Perturbations](https://mlsanity.com/paper/2502.06453/) (2025)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Is Your Model Really A Good Math Reasoner? Evaluating Mathematical Reasoning with Checklist](https://mlsanity.com/paper/2407.08733/) (2024)
- [An Investigation of Robustness of LLMs in Mathematical Reasoning: Benchmarking with Mathematically-Equivalent Transformation of Advanced Mathematical Problems](https://mlsanity.com/paper/2508.08833/) (2025)

## Abstract (arXiv)

AI systems increasingly operate between flexible input representations and formal objects used by downstream tools. A key challenge is recognizing when an unfamiliar formulation denotes a known formal object. We study this challenge through theorem recognition: given an equivalence-preserving transformation of a theorem condition, a model must recover the theorem identity associated with the standard statement. We introduce TREAT, a benchmark for evaluating whether large language models can recover known theorem identities from equivalence-preserving formula-level transformations. Rather than paraphrasing theorem text, TREAT changes the mathematical form of theorem conditions themselves, expressing known results through residual equations, witness statements, optimization identities, set relations, operator forms, and proof-intermediate characterizations. Starting from scraped theorem pages, we filter for entries with usable mathematical expression forms, extract canonical theorem conditions, and generate transformed variants with recorded assumptions and inverse mappings. The final corpus contains 737 theorem identities and 29,480 transformed rows. On a test panel, the best model retrieves the correct theorem identity in only 60.73% of cases. Other systems reveal different failure modes, including abstention, wrong detection, and malformed outputs. These suggest that theorem knowledge can be fragile under equivalent changes in representation. TREAT therefore provides a controlled testbed for evaluating representation-robust access to formal knowledge, with broader relevance to domains that require stable target objects, explicit equivalence relations, validation procedures, and auditable scoring.