TREAT: Evaluating Access to Formal Knowledge across Equivalent Mathematical Representations

# TREAT: Evaluating Access to Formal Knowledge across Equivalent Mathematical Representations
Source: [https://arxiv.org/html/2608.07540](https://arxiv.org/html/2608.07540)
###### Abstract

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\.

## IIntroduction

A central requirement for intelligent systems is the ability to access relevant knowledge across changes in representation\. For AI systems, this creates a representation\-access problem: the same underlying concept may appear through many equivalent surface forms, but only some of them may activate the correct stored knowledge\. While the empirical evidence in this paper is limited to the theorem\-recognition setting, this issue arises in mathematical reasoning, scientific modeling, retrieval, verification, and structured decision making, where a known result or object may be expressed as a formula, constraint, optimization condition, set relation, invariant, rule, or intermediate characterization\[[1](https://arxiv.org/html/2608.07540#bib.bib1),[13](https://arxiv.org/html/2608.07540#bib.bib4),[2](https://arxiv.org/html/2608.07540#bib.bib5),[16](https://arxiv.org/html/2608.07540#bib.bib6)\]\. Although these forms can preserve the same meaning, they may provide very different cues for recognition\. A system may therefore appear to know a concept in its standard form while failing to identify or use it when the representation changes\. This paper studies that gap between possessing knowledge and accessing it under equivalent transformation\.

This problem is especially visible in mathematics, where the same content can be expressed through many equivalent forms\. A theorem may appear as an inequality, an operator equality, a zero\-residual condition, an existential witness statement, an optimization identity, a set\-membership relation, or a proof\-intermediate invariant\. These forms can be equivalent while providing very different cues for recognition\. Thus, theorem recognition offers a clean setting for studying whether a model can access known knowledge after the representation changes\.

The ability to recover known results from transformed representations matters for more than benchmark accuracy\. In formal theorem proving, a system often needs to select relevant premises before proof search can proceed; premise selection has long been identified as a major bottleneck in large mathematical libraries\[[2](https://arxiv.org/html/2608.07540#bib.bib5),[16](https://arxiv.org/html/2608.07540#bib.bib6)\]\. Related work in mathematical information retrieval also shows that formula meaning cannot be reduced to surface notation: formula\-concept recognition asks whether a formula can be matched to a unique underlying mathematical concept identifier\[[13](https://arxiv.org/html/2608.07540#bib.bib4)\]\. These settings all require access to formal knowledge under representational variation\.

Current mathematical language\-model evaluations do not directly isolate this ability\. Benchmarks such as GSM8K, MATH, and Minerva\-style evaluations test whether models can solve word problems, competition problems, or quantitative reasoning tasks and are usually scored by final answers or generated derivations\[[4](https://arxiv.org/html/2608.07540#bib.bib8),[7](https://arxiv.org/html/2608.07540#bib.bib9),[9](https://arxiv.org/html/2608.07540#bib.bib10)\]\. Formal\-theorem\-proving benchmarks evaluate proof construction or formalization ability\[[12](https://arxiv.org/html/2608.07540#bib.bib11),[18](https://arxiv.org/html/2608.07540#bib.bib12),[15](https://arxiv.org/html/2608.07540#bib.bib13)\]\. Robustness benchmarks show that mathematical performance can degrade under perturbed or equivalent problem variants\[[8](https://arxiv.org/html/2608.07540#bib.bib14),[6](https://arxiv.org/html/2608.07540#bib.bib15)\]\. However, these settings leave a complementary question underexplored: when the target is a known named theorem, can a model recover that theorem from an equivalent but unfamiliar formula\-level representation?

The central question of this paper is whether formal knowledge remains accessible when its representation changes\. We study this question through theorem recognition, asking whether models that are familiar with a theorem in its standard form can recover it from an equivalent but unfamiliar mathematical representation\. We ask four broad questions\. First, to what extent do language models retain access to known formal knowledge when its representation changes? Second, when access fails, do models abstain, retrieve the wrong object, or produce unusable outputs? Third, which properties of the transformed representation make recognition easier or harder? Finally, how can test\-time guidance improve this?

To address these questions, we buildTREAT, a benchmark for Theorem Recognition under Equivalence\-preserving mAthematical Transformation, using theorem recognition as a controlled testbed for studying representation\-robust access to formal knowledge\. Each item in the benchmark presents a transformed variant of a mathematical theorem\. Unlike natural\-language paraphrase benchmarks, the transformation is applied to the mathematical representation itself: theorem conditions may be rewritten as residual equations, witness statements, optimization identities, set relations, operator forms, distributional characterizations, or proof\-intermediate forms\.

The benchmark is constructed from theorems with mathematical expression forms\. For each theorem, we extract a canonical theorem condition, record assumptions, and generate equivalence\-preserving variants with inverse\-mapping notes\. Candidate variants are semantically validated with Gemini 3\.1 Pro, transformations were encoded symbolically and checked with Z3, and each row records validation metadata\. The resulting corpus contains 737 theorem identities and 29,480 transformed rows, with metadata supporting validation, filtering, and error analysis\. We evaluate six language models on a 960\-item shared\-known panel, where the target theorem concepts are selected from theorems that multiple models report knowing in standard form\. This design reduces the confound that a failure is simply due to unfamiliarity with the theorem\. The best model achieves 60\.73% accuracy, with different systems having different patterns of abstention and incorrect theorem detection\.

This paper makes four contributions\. First, we formulate theorem recognition under equivalence\-preserving transformation as a controlled evaluation of representation\-robust access to formal knowledge\. Second, we introduceTREAT, a benchmark with formula\-level transformations, recorded assumptions, inverse mappings, and validation metadata\. Third, we provide a six\-model evaluation showing that theorem recognition remains far from saturated even on frontier models\. Fourth, we analyze failure behavior and test\-time recovery, showing that missed theorem access can sometimes be recovered with additional guidance but must be evaluated together with false\-route risk\.

## IIRelated Work

### II\-AMathematical reasoning benchmarks\.

Most benchmarks for mathematical language models evaluate problem solving rather than recognition of known formal objects\. GSM8K tests multi\-step grade\-school word problems\[[4](https://arxiv.org/html/2608.07540#bib.bib8)\], MATH evaluates competition\-style problem solving\[[7](https://arxiv.org/html/2608.07540#bib.bib9)\], and Minerva\-style evaluations study quantitative reasoning over mathematical and scientific questions\[[9](https://arxiv.org/html/2608.07540#bib.bib10)\]\. Formal mathematics benchmarks and systems, including GPT\-f, MiniF2F, and autoformalization work, evaluate proof generation, formalization, or interaction with proof assistants\[[12](https://arxiv.org/html/2608.07540#bib.bib11),[18](https://arxiv.org/html/2608.07540#bib.bib12),[15](https://arxiv.org/html/2608.07540#bib.bib13)\]\. These settings measure whether models can solve problems or construct proofs\. In contrast,TREATasks whether a model can recover the theorem identity associated with a transformed theorem condition\. A model may know a theorem or solve related problems while still failing to identify the theorem after an equivalence\-preserving change in representation\.

### II\-BRobustness under mathematical variation\.

Recent work has shown that mathematical reasoning can be sensitive to changes in problem form\. MathCheck evaluates mathematical reasoning using checklist\-style variants\[[19](https://arxiv.org/html/2608.07540#bib.bib21)\], GSM\-Symbolic shows that GSM8K\-style performance can degrade under symbolic template changes and irrelevant clauses\[[11](https://arxiv.org/html/2608.07540#bib.bib22)\], MATH\-Perturb constructs perturbed versions of difficult MATH problems\[[8](https://arxiv.org/html/2608.07540#bib.bib14)\], and PutnamGAP studies robustness under mathematically equivalent transformations of advanced problems\[[6](https://arxiv.org/html/2608.07540#bib.bib15)\]\. Related robustness concerns also arise in step\-level mathematical verification, where evaluator judgments can change across semantically valid perturbations of solution traces\[[10](https://arxiv.org/html/2608.07540#bib.bib2)\]\. TREAT is related to this line of work but differs in the target of evaluation\. Prior robustness benchmarks typically ask whether a model can still solve a problem after perturbation\. TREAT asks whether a model can retrieve the known theorem handle behind an equivalent but structurally unfamiliar formula\-level representation\.

### II\-CFormal knowledge retrieval and theorem access\.

TREAT also connects to work on retrieving reusable knowledge objects\. Case\-based reasoning studies retrieval and adaptation of prior cases\[[1](https://arxiv.org/html/2608.07540#bib.bib1)\]; semantic parsing and entity linking map flexible inputs to structured meanings or knowledge\-base entries\[[17](https://arxiv.org/html/2608.07540#bib.bib16),[3](https://arxiv.org/html/2608.07540#bib.bib17),[14](https://arxiv.org/html/2608.07540#bib.bib3)\]\. In mathematics, formula\-concept recognition studies whether formulas can be matched to underlying mathematical concept identifiers despite variation in notation\[[13](https://arxiv.org/html/2608.07540#bib.bib4)\]\. Premise selection and retrieval\-augmented theorem proving show that formal proof systems often depend on identifying relevant prior results before proof search can proceed\[[2](https://arxiv.org/html/2608.07540#bib.bib5),[16](https://arxiv.org/html/2608.07540#bib.bib6)\]\. We isolate a complementary problem: given a transformed mathematical condition, can a language model recover the named theorem that indexes the relevant formal knowledge?

## IIIBenchmark Methodology

### III\-ATask Definition and Scope

We study theorem recognition under equivalence\-preserving transformation\. LetTTdenote a named theorem identity,CTC\_\{T\}its canonical mathematical condition, andATA\_\{T\}the assumptions under which the theorem is stated\. A transformed variantVT,jV\_\{T,j\}is intended to preserve the theorem condition under the same assumptions, i\.e\., to satisfyAT⊧CT↔VT,jA\_\{T\}\\models C\_\{T\}\\leftrightarrow V\_\{T,j\}\. This biconditional is a target rather than an assumed property of the raw generated variants\.

At evaluation time, the model receives onlyVT,jV\_\{T,j\}, together with minimal surrounding text needed to parse the mathematical statement\. It is not given the theorem name, theorem family, subfield, candidate list, canonical condition, or transformation type\. The model must recover the theorem identityTT, which serves as the handle for the canonical theorem statement stored in the benchmark\.

This task differs from mathematical problem solving and proof generation\. The goal is not to derive a numerical answer or construct a complete proof, but to determine whether a known theorem remains recognizable after its mathematical representation changes\. Theorem recognition is a useful testbed because theorem identities provide stable targets, many theorem statements contain compact formula\-level conditions, and equivalence can be audited through assumptions, inverse mappings, symbolic templates, and validation metadata\.

### III\-BBenchmark Construction

#### III\-B1Theorem Corpus

TREATis constructed from theorem\-related pages in English Wikipedia\. We use Wikipedia because it provides a broad and public source of named mathematical results with stable page titles, redirects, categories, and formula\-bearing statements\. The source choice is intentional:TREATis not designed to test whether a model has never seen a theorem, but whether a model can recover a well\-known theorem after an equivalence\-preserving change in mathematical representation\. Because not every theorem page supports formula\-level transformation, the pipeline filters entries for usable mathematical expression forms\. A retained entry must correspond to a named theorem or named mathematical result, contain a recoverable theorem\-like condition, and provide enough context to identify assumptions and scope\. The filtering stage removes broad topic pages, ambiguous mathematical objects, prose\-only entries, duplicate or near\-duplicate theorem identities, and formulas that do not function as theorem conditions\. During preprocessing, theorem pages referring to the same mathematical result under different names are collapsed into a single theorem identity, using the most common page name as the canonical label\. For each retained theorem identity, the benchmark stores the theorem name, accepted aliases when available from the source page, field metadata, canonical statement, canonical mathematical conditionCTC\_\{T\}, and assumptionsATA\_\{T\}\. The final corpus contains 737 theorem identities selected from a 2456\-row raw inventory\. The released benchmark will include source page titles, source URLs, and license metadata for attribution and reproducibility; derived entries are distributed with the required attribution and compatible licensing for Wikipedia\-derived text\.

#### III\-B2Variant Generation

TABLE I:Transformation types used to disguise a theorem concept while preserving its canonical formal content\. These are formula\-level transformations, not natural\-language paraphrases\.The benchmark is designed to intervene on mathematical representation rather than on surface wording\. Before generating variants, we define a taxonomy of equivalence\-preserving transformation families\. These include slack\-witness encodings of inequalities, residual and nonnegativity encodings, singleton and diagonal equality encodings, set\-membership reformulations, optimization and projection identities, monotone order embeddings, operator and functional encodings, integral\-transform characterizations, probabilistic and distributional reformulations, counting encodings, and theorem\-specific proof\-intermediate characterizations\. Table[I](https://arxiv.org/html/2608.07540#S3.T1)reports representative schemas for these transformation families\. The examples are schematic because the concrete instantiation depends on the theorem’s domain, variables, and assumptions\.

Given the retained theorem inventory and the predefined transformation taxonomy, GPT\-5 Pro is used to generate candidate variants\. Each prompt is conditioned on the theorem name, canonical statement, assumptions, canonical condition, and a target transformation family\. The model is asked to produce a transformed mathematical condition together with an inverse\-mapping note explaining how the transformed form reduces back to the canonical condition\. This makes generation theorem\-conditioned and transformation\-conditioned rather than open\-ended: a candidate row must instantiate a specified route of representation change and expose the mathematical path back to the original condition\. The important constraint is semantic preservation: the transformed form denotes the same theorem concept under the stored assumptions, while changing the route by which the canonical theorem condition is recognized\. The final benchmark consists of 29,480 transformed rows with a nonuniform number of transformed variants per theorem\. The goal is not to cover all mathematical theorems or transformations, but to build an auditable benchmark over theorem identities whose mathematical content can be transformed while preserving meaning under stated assumptions\.

#### III\-B3Validation

After variant generation, each candidate row is semantically validated with Gemini 3\.1 Pro\. The validator is given the theorem name, canonical statement, assumptions, canonical formula, transformed formula, claimed transformation type, and inverse\-mapping note\. It returns one of six categorical judgments: equivalent, equivalent under stated assumptions, mathematically wrong, probably stronger, probably weaker, or unclear\. Rows judged mathematically wrong are removed\. Rows judged probably stronger, probably weaker, or unclear are either rejected or sent to further review and are not used in the evaluation panel\.

Z3 was used as an additional validation layer\[[5](https://arxiv.org/html/2608.07540#bib.bib20)\]\. The Z3 layer does not prove the source theorem itself\. Instead, it checks whether the transformation template preserves the encoded theorem condition\. For a canonical conditionCCand transformed conditionVV, the checker asserts the negated equivalence,

\(C∧¬V\)∨\(¬C∧V\),\(C\\wedge\\neg V\)\\vee\(\\neg C\\wedge V\),\(1\)and accepts the template\-level check when this formula is unsatisfiable under the recorded abstraction and assumptions\.

For example, a slack transformation for an inequality checks thata≤ba\\leq bis equivalent to∃s≥0:b=a\+s\\exists s\\geq 0:b=a\+sover the relevant numeric domain\. A residual transformation checks thatF=0F=0is equivalent toF2=0F^\{2\}=0or\|F\|2=0\|F\|^\{2\}=0under nonnegativity assumptions\. Analytic transformations, distributional characterizations, and theorem\-specific proof intermediates are not always directly decidable in Z3; those rows retain semantic and metadata validation, and the Z3 layer is recorded as template\-level, axiomatized, or not applicable\.

We additionally manually inspect a 100\-row validation subset consisting of 10 theorem identities with 10 transformed variants per theorem\. The human check did not identify any mathematically wrong theorem mapping or counterexample in this subset\. Likewise, the Z3 checks pass successfully and do not find any counterexample among the symbolically encodable cases\.

## IVEvaluation Methodology

### IV\-AEvaluation Panel Selection

The evaluation panel is designed to separate theorem unfamiliarity from representation\-dependent access failure\. Before evaluating transformed variants, we first probe models for familiarity with theorem identities in their standard form\. The shared\-known panel is then constructed from theorem concepts that appear in the common known set\. From this pool, we sample 160 theorem identities and six transformed variants per theorem, yielding 960 evaluation items\.

This design is intentionally conservative\. Models are evaluated only on transformed variants of theorem concepts that were previously identified as familiar in standard form\. As a result, failure on a transformed item is less likely to reflect complete absence of the theorem from the model’s repertoire\. Instead, it more directly measures whether the theorem remains accessible after its condition has been rewritten into an equivalent but structurally different representation\.

The 960\-item panel covers five broad mathematical families: 504 Analysis items, 180 Algebra/Linear Algebra items, 156 Probability/Information Theory items, 78 Number Theory items, and 42 Combinatorics/Graph Theory items\. It also spans nine transformation buckets\. The transformation\-bucket composition is reported in Fig\.[3](https://arxiv.org/html/2608.07540#S5.F3)\. Buckets with small support, such as residual/nonnegativity and characterization/iff, are included for coverage but are not used for strong bucket\-level conclusions\. Family labels are assigned at the theorem\-identity level using the source page categories, field metadata, and the primary mathematical context of the canonical statement\. Boundary cases are assigned to the family most directly associated with the theorem identity used in the benchmark\. We therefore treat family accuracy as a coarse diagnostic of neighborhood\-level retrieval, not as a complete mathematical ontology\.

### IV\-BRecognition Task

Each evaluation input contains only the transformed mathematical statement and the minimal surrounding text needed to parse it\. The model is not given the theorem family, subfield, candidate theorem list, original theorem name, canonical condition, or transformation type\. It must return a structured JSON response indicating whether a valid theorem route exists, the predicted theorem name orNONE, relevant aliases, a short connection explaining the match, a brief justification sketch, any missing assumptions, and a confidence score\. The theorem name is used as the scored handle for the canonical theorem form stored in the benchmark\. This is a practical choice because named theorem identities have aliases, field labels, and canonical statements that can be normalized for evaluation\. The explanatory fields are not the primary target of scoring; they are included to discourage unsupported name guessing and to support later audit of model behavior\.

### IV\-CScoring Metrics

The primary metric is exact theorem\-identification accuracy\. A prediction is counted as correct when the normalized predicted theorem name matches the gold theorem identity\. Normalization handles capitalization, punctuation, possessives, parenthetical aliases, selected synonym forms, and minor eponym\-order variations\. We also report family accuracy, which credits predictions that identify a theorem from the correct mathematical family\. The small exact\-to\-family gaps across models suggest that the headline result is not mainly driven by minor naming variants\.

To characterize model behavior beyond top\-line accuracy, we report four additional quantities\. The asserted rate is the share of items for which the model returns a theorem name rather thanNONE\. The wrong\-named rate measures cases where the model asserts a theorem identity but the identity is incorrect\. TheNONErate measures abstention or failure to retrieve a theorem concept\. The malformed\-output rate measures invalid JSON or responses that violate the required schema\. These metrics are important because models with similar exact accuracy may behave very differently: one may aggressively commit to theorem names and incur more wrong\-theorem errors, while another may abstain on many recoverable items\.

### IV\-DTest\-Time Computation Setting

The main evaluation uses the zero\-hint setting described above\. We also evaluate test\-time computation \(TTC\) interventions as a secondary analysis of recoverability and reliability\. These interventions are not used to define the primary benchmark score\. Instead, they test whether missed recognitions can be recovered when the model receives additional guidance, such as retry prompting, family or subfield hints, or transformation\-type hints\.

Because such interventions can also encourage over\-recognition, TTC is evaluated on both valid transformed theorem rows and matched negative or bait rows whose correct answer isNONE\. This allows us to distinguish useful recovery from unsafe theorem routing: an intervention is valuable only if it improves recognition on valid items without substantially increasing false theorem routes on invalid statements\.

## VResults

The panel contains 960 transformed variants of 160 theorem concepts, with six variants per concept\. Every item has a gold canonical theorem handle by construction, so aNONEresponse is a failed retrieval on this benchmark rather than a true negative\.

TABLE II:Shared\-known 960\-item canonical\-form retrieval results\. Exact counts are out of 960\.### V\-AAccess Under Representation Change

Table[II](https://arxiv.org/html/2608.07540#S5.T2)gives the main answer to the first question\. Recognition remains far from saturated even under the shared\-known design\. GPT\-5\.4 Pro is the strongest system, with 583 exact matches out of 960 items, or 60\.73%, but it still fails to retrieve the correct theorem identity on 377 transformed variants\. The middle group ranges from 46\.88% to 52\.81%, while GPT\-OSS 120B reaches 11\.15%\. Thus, theorem familiarity in standard form does not guarantee access to the same theorem after an equivalence\-preserving change in representation\.

The small gap between exact accuracy and family accuracy is also informative\. For most models, family accuracy improves exact accuracy by only about 0\.6–3\.7 percentage points\. This means that many failures are not merely alias or near\-miss problems within the right area of mathematics\. They often reflect either abstention or retrieval of a different theorem concept\. In this retrieval setting, the model does not just need to know the broad domain; it must recover the correct formal handle\.

### V\-BFailure Behavior: Abstention, Wrong Retrieval, and Output Reliability

Top\-line accuracy hides different access policies\. Table[III](https://arxiv.org/html/2608.07540#S5.T3)conditions on the cases where a model asserted a theorem concept rather than returningNONE\. GPT\-5\.4 Pro has the highest coverage, asserting a theorem on 789 items, but only 73\.9% of those assertions are exact and 21\.7% are wrong named\-theorem commitments\. Gemini 3\.1 Pro shows a similar high\-coverage profile, with 675 asserted theorem names, 74\.7% exact among assertions, and 23\.6% wrong among assertions\. By contrast, Qwen3 Coder 480B asserts on only 480 items, but 93\.8% of those assertions are exact and only 5\.0% are wrong\. Gemma 3 27B is similarly selective, with 509 assertions, 88\.6% exact among assertions, and 9\.8% wrong among assertions\.

TABLE III:Retrieval\-policy decomposition\. Assertednnis the number of items on which the model returned a theorem concept\. Conditional exact and wrong rates are computed over asserted items\. Malformed output is reported separately\.Fig\.[1](https://arxiv.org/html/2608.07540#S5.F1)visualizes these differences\. The models are not arranged along a single ability axis\. GPT\-5\.4 Pro and Gemini 3\.1 Pro retrieve often, which gives them higher all\-item recall but also a larger wrong\-theorem risk\. Qwen3 Coder 480B and Gemma 3 27B are more conservative: when they commit, they are usually correct, but they leave roughly half of the panel unresolved\. GPT\-OSS 120B is dominated by abstention, returningNONEon 831 items\.

![Refer to caption](https://arxiv.org/html/2608.07540v1/x1.png)Figure 1:Retrieval\-policy map on the 960\-item panel\. The x\-axis shows abstention/NONErate, the y\-axis shows exact retrieval accuracy, and bubble size reflects wrong named\-theorem assertions\.This distinction matters because the failure modes have different consequences\. A wrong theorem route may send a proof search, verifier, retrieval system, or explanation toward the wrong formal object\. Abstention is safer but limits usefulness when a system needs to hand off to a formal artifact\. Structured\-output reliability adds a third dimension to the error analysis\. The malformed\-output rates are reported in Tables[II](https://arxiv.org/html/2608.07540#S5.T2)and[III](https://arxiv.org/html/2608.07540#S5.T3); Qwen3 Coder 480B’s malformed outputs persisted across repeated runs under the same structured\-output protocol\. It recorded a 25\.21% malformed\-output rate, despite having the highest conditional precision among asserted theorem names in Table[III](https://arxiv.org/html/2608.07540#S5.T3)\. This separates mathematical recoverability from interface reliability: a model may often identify the right theorem when it commits, yet still be difficult to use in a structured task\.

### V\-CWhere Representation Change Is Easier or Harder

We next ask which properties of the transformed representation affect recognition\. Fig\.[2](https://arxiv.org/html/2608.07540#S5.F2)visualizes exact theorem identification by mathematical family matrix\. Analysis family has the largest support at 504 items, so its estimates are the most stable\. Combinatorics/Graph Theory has only 42 items, so results in that column should be treated as diagnostic rather than definitive\.

![Refer to caption](https://arxiv.org/html/2608.07540v1/x2.png)Figure 2:Family\-level exact retrieval accuracy heatmap\. Numbers are percentages\. Small\-family cells, especially Combinatorics/Graph Theory, should be read as diagnostic rather than definitive\.The family matrix argues against treating theorem recognition as a single undifferentiated math\-knowledge score\. GPT\-5\.4 Pro is the strongest aggregate system, but Gemini 3\.1 Pro is higher on Algebra/Linear Algebra, Number Theory, and the small Combinatorics/Graph Theory slice\. GPT\-5\.4 Pro is stronger on Analysis and Probability/Information Theory\. These differences suggest that recognition depends on the interaction between the transformed representation and the mathematical neighborhood in which the theorem lives\. Some families contain distinctive formal signatures, while others contain broad inequalities, extremal principles, or analytic conditions that overlap across multiple named results\.

Transformation type is another source of variation\. Fig\.[3](https://arxiv.org/html/2608.07540#S5.F3)reports the transformation\-bucket distribution in the shared\-known panel, while Table[IV](https://arxiv.org/html/2608.07540#S5.T4)ranks buckets by six\-model mean exact accuracy\. Optimization/projection variants are the hardest major bucket, with a six\-model mean of 37\.9%\. Integral\-transform variants have the highest mean at 58\.3%, but their support is only 28 items, so they should not be overinterpreted\. Among larger buckets, counting/combinatorial, proof\-intermediate, and probabilistic/distributional transformations cluster around 44–45% mean exact accuracy\. These results show that the benchmark is not merely testing theorem rarity\. A theorem can become easier or harder to recognize depending on whether it is exposed through an optimization identity, a counting invariant, a distributional condition, or a proof\-intermediate characterization\.

TABLE IV:Transformation buckets ranked by six\-model mean exact accuracy\.![Refer to caption](https://arxiv.org/html/2608.07540v1/x3.png)Figure 3:Transformation\-bucket distribution of the 960\-item shared\-known panel\. Proof\-intermediate variants are the largest bucket; residual/nonnegativity and characterization/iff have small support and not to be overinterpreted\.
### V\-DTest\-Time Recovery and False\-Route Risk

The final question is whether missed recognitions can be recovered without encouraging unsafe over\-recognition\. The main results above use the zero\-hint setting\. We therefore evaluate test\-time computation \(TTC\) as a secondary analysis\. TTC means additional second\-pass computation or additional prompt\-side information; model parameters are not updated\. On positive rows, TTC is applied only when the baseline row is a detectable failure, either because the model returned a false route decision or because the output was malformed\. Baseline exact successes are preserved\. On negative or bait rows, each row is forced through the same TTC method using a fake failed baseline\. These negative rows are paired with tempting source theorems, but their displayed statements are invalid or perturbed, so the correct answer isNONE\.

We evaluate retry\-after\-failure prompting, family and subfield hints, and transformation\-type hints\. Table[V](https://arxiv.org/html/2608.07540#S5.T5)reports the main TTC results\. The strongest recovery pattern appears for Qwen3\. Retry, family hints, and transform hints all improve exact accuracy by more than 26 percentage points while producing 0/960 false routes on matched negative controls\. Family hinting is the best method for Qwen, improving from 46\.88% to 77\.50%, a gain of 30\.62 points\. The TTC results also show that positive recovery and safety are different properties\. Gemma 27B illustrates the risk most clearly: family hints improve positive accuracy by 16\.15 points, but produce 329 false named routes out of 960 negative rows\. Gemma 12B family hints are safer in this sweep, improving by 17\.29 with 0/960 false routes\. Thus, the same intervention type can be helpful for one model and unsafe for another\.

TABLE V:Test\-time computation results on positives and matched negative/bait controls\. False routes count named\-theorem assertions on 960 negative rows whose correct answer isNONE\.

## VIDiscussion

### VI\-AAccessibility Under Representation Change

The central question of this paper is whether formal knowledge remains accessible when its representation changes\. The results support a bounded but important answer: for theorem concepts with usable mathematical expression forms, models that appear familiar with a theorem in standard form often fail to recover the correct theorem identity from an equivalent formula\-level variant\. The shared\-known design reduces the simplest confound, namely that the model did not know the theorem at all\. It does not reveal the model’s internal representation of the theorem, but it makes the observed failures more plausibly about access under representation change than about complete absence of the theorem name\.

This finding matters because formal knowledge is useful only when it can be connected to the forms in which problems, constraints, or intermediate results actually appear\. InTREAT, the target object is a named theorem identity, which serves as an auditable handle for a stored canonical statement and condition\. In other domains, the corresponding target might be a library entry, verification rule, schema element, ontology identifier, invariant, or executable specification\. We do not claim that theorem\-domain accuracies numerically predict behavior in those settings\. Rather, the theorem setting provides a controlled testbed for measuring a broader pressure point: whether equivalent but unfamiliar representations still lead a model to the formal object needed for use, retrieval, or audit\.

### VI\-BAccuracy, Abstention, and Wrong Retrieval

Top\-line exact accuracy is only one part of representation\-robust access\. Models differ not only in how often they recover the correct theorem, but also in how they fail\. Some failures are abstentions: the model returnsNONEeven though every main benchmark item has a gold theorem identity\. GPT\-OSS 120B is the clearest example, with 831 abstentions out of 960 items, while Qwen3 Coder 480B and Gemma 3 27B abstain on roughly half of the panel\. Other failures are wrong commitments: the model asserts a theorem name, but the theorem is incorrect\. GPT\-5\.4 Pro and Gemini 3\.1 Pro have higher coverage, but roughly one\-fifth to one\-quarter of their asserted theorem names are wrong\. A third failure mode is interface failure, where the model does not satisfy the required structured\-output format, as reflected in Qwen3 Coder 480B ’s 25\.21% malformed\-output rate\.

These errors have different consequences\. A wrong theorem route may direct a proof search, verifier, retrieval system, or explanation toward the wrong formal object\. Abstention is safer, but it limits usefulness\. The policy decomposition therefore changes how the leaderboard should be interpreted\. Qwen3 Coder 480B has lower all\-item exact accuracy than Gemma 3 12B, but among asserted theorem names it is exact on 93\.8% of cases\. GPT\-5\.4 Pro obtains the highest all\-item exact score because it covers more of the panel, but this comes with more wrong\-theorem risk\. For formal applications, the preferred operating point may depend on whether the system values coverage, precision, abstention, or schema reliability\.

### VI\-CStructured Representation Effects

The family and transformation analyses show that representation failure is not uniform\. Recognition varies across mathematical families, transformation types, and theorem identities\. This argues against treating theorem recognition as a single undifferentiated measure of mathematical knowledge\. A theorem with a distinctive algebraic signature may remain recognizable after some transformations, while a theorem expressed through a generic inequality, extremal principle, convergence statement, or distributional condition may be easier to confuse with nearby results\.

The transformation results are especially important for interpreting what the benchmark measures\.TREATdoes not merely paraphrase theorem text\. It changes the mathematical form of the theorem condition through witness encodings, residual forms, optimization identities, set\-membership reformulations, operator forms, distributional characterizations, and proof\-intermediate invariants\. These transformations can preserve truth under the recorded assumptions while changing the route by which the theorem is recognized\. This places the benchmark between ordinary name recognition and full proof reconstruction: the model is not asked to prove the theorem from first principles, but it must recover the correct stored theorem handle when familiar surface cues are removed\.

### VI\-DTest\-Time Guidance

The TTC results add a second layer to the main finding\. Some failures are recoverable, which suggests that representation failure is not always an absence of theorem knowledge\. In several cases, the model appears to need help localizing the relevant theorem neighborhood\. The results indicate that narrowing the search space to a coherent mathematical neighborhood can make latent theorem access more effective\.

The TTC results also show that guidance must be evaluated for safety, not only for positive recovery\. Matched negative and bait rows are essential because an intervention can improve recognition on valid theorem variants while also encouraging false theorem routes on invalid statements\. Gemma 27B illustrates this risk: family hints improve positive accuracy by 16\.15 points, but produce 329 false named routes out of 960 negative rows, or 34\.27%\. By contrast, Gemma 12B family hints are safer in this sweep, giving a 17\.29\-point gain with no false routes on matched negatives\. Thus, the same intervention type can be useful for one model and unsafe for another\.

Overall, the TTC study changes the interpretation of the benchmark\. The zero\-hint results show that representation change disrupts direct access to known theorem identities\. The TTC results show that some of this lost access can be recovered with additional localization\. But the negative controls show that recovery must be coupled with refusal behavior: a useful intervention must improve recognition on valid transformed statements while preserving the ability to returnNONEwhen no valid theorem route exists\.

## VIILimitations and Future Work

This study has several limitations\. First,TREATis restricted to theorem concepts with recoverable mathematical expression forms\. Many mathematical results are conceptual, geometric, algorithmic, or prose\-based, and are therefore outside the current benchmark\. The benchmark should thus be read as measuring representation\-robust theorem recognition for a subset of theorems, not for all mathematical knowledge\.

Second, the corpus is shaped by its source inventory and filtering pipeline\. The scraped theorem pages vary in coverage, notation, and quality, and some theorem families and transformation buckets are better represented than others\. Small\-support buckets should therefore be interpreted cautiously\. Future versions should expand and better balance theorem families, subfields, and transformation types to separate domain effects from representation effects\.

Third, although transformed variants are filtered using explicit assumptions, inverse mappings, and validation labels and Z3 template checks and a small human audit confirmed the validity, the corpus is still not proof\-assistant\-certified\. Z3 applies only to encodable transformation templates, and analytic, distributional, and proof\-intermediate variants may require assumptions or reasoning outside the SMT fragment\. Another validation risk is stronger/weaker drift and missing side condition leakage\. Therefore, larger expert audits and proof\-assistant formalization for selected subsets are important directions for future work\.

Fourth, the shared\-known panel controls for theorem familiarity only approximately\. It reduces the likelihood that failures are caused by complete absence of the theorem, but it does not prove identical model exposure to theorem names or source formulations\. Similarly, the TTC study shows that prompt\-side guidance can recover some missed recognitions, but it does not exhaust the space of retrieval, verification, constrained decoding, tool use, or multi\-step reasoning strategies\.

Future work should study stronger recovery mechanisms such as theorem\-library search, symbolic preprocessing, proof\-state context, calibrated abstention, and constrained decoding\. These methods should be evaluated with both positive transformed items and matched invalid controls, so that improved recovery is not confused with unsafe over\-recognition\.

Finally, future work could test whether this evaluation protocol transfers beyond mathematics, to domains such as software verification, database query rewriting, scientific equation retrieval, ontology linking, or rule\-based decision systems\. Such extensions would require domain\-specific target objects, equivalence relations, transformation families, and validation procedures\.

## Appendix APrompt Details

For theorem recognition, the prompt contract was: “You are given a transformed mathematical statement\. The statement is intended to be mathematically equivalent to the canonical formal form of a known mathematical concept, usually a named theorem, but it may be written in a noncanonical formula or condition form\. Task: retrieve the underlying mathematical concept and its standard theorem identity\. Treat the theorem identity as the handle for the canonical formal form\. Do not rely on topic metadata, theorem lists, family hints, or candidate names\. Use only the mathematical content of the transformed statement\. Return valid JSON only with fieldsrecognized,theorem\_name,aliases,connection,justification\_sketch,missing\_assumptions, andconfidence\. If no named theorem concept can be responsibly retrieved, setrecognizedtofalseandtheorem\_nametoNONE\.”

Before transformed\-form evaluation, models were also given a familiarity probe: “You are given a list of named mathematical theorems\. For each theorem, answer whether you recognize the theorem in its standard form\. Mark a theorem as known only if you can identify the standard theorem concept and would be able to state its usual mathematical content\. Return JSON withtheorem\_name,known, andbrief\_standard\_content\.” The shared\-known panel was sampled from theorem identities marked known by the familiarity\-probed models, with six transformed variants per selected theorem\.

## References

- \[1\]A\. Aamodt and E\. Plaza\(1994\)Case\-based reasoning: foundational issues, methodological variations, and system approaches\.AI Communications7\(1\),pp\. 39–59\.Cited by:[§I](https://arxiv.org/html/2608.07540#S1.p1.1),[§II\-C](https://arxiv.org/html/2608.07540#S2.SS3.p1.1)\.
- \[2\]A\. A\. Alemi, F\. Chollet, N\. Een, G\. Irving, C\. Szegedy, and J\. Urban\(2016\)DeepMath: deep sequence models for premise selection\.InAdvances in Neural Information Processing Systems,Cited by:[§I](https://arxiv.org/html/2608.07540#S1.p1.1),[§I](https://arxiv.org/html/2608.07540#S1.p3.1),[§II\-C](https://arxiv.org/html/2608.07540#S2.SS3.p1.1)\.
- \[3\]J\. Berant, A\. Chou, R\. Frostig, and P\. Liang\(2013\-10\)Semantic parsing on Freebase from question\-answer pairs\.InProceedings of the 2013 Conference on Empirical Methods in Natural Language Processing,Seattle, Washington, USA,pp\. 1533–1544\.External Links:[Link](https://aclanthology.org/D13-1160/)Cited by:[§II\-C](https://arxiv.org/html/2608.07540#S2.SS3.p1.1)\.
- \[4\]K\. Cobbe, V\. Kosaraju, M\. Bavarian, M\. Chen, H\. Jun, L\. Kaiser, M\. Plappert, J\. Tworek, J\. Hilton, R\. Nakano, C\. Hesse, and J\. Schulman\(2021\)Training verifiers to solve math word problems\.InarXiv preprint arXiv:2110\.14168,Cited by:[§I](https://arxiv.org/html/2608.07540#S1.p4.1),[§II\-A](https://arxiv.org/html/2608.07540#S2.SS1.p1.1)\.
- \[5\]L\. de Moura and N\. Bjørner\(2008\)Z3: an efficient SMT solver\.InTools and Algorithms for the Construction and Analysis of Systems,Lecture Notes in Computer Science, Vol\.4963,Berlin, Heidelberg,pp\. 337–340\.External Links:[Document](https://dx.doi.org/10.1007/978-3-540-78800-3%5F24),[Link](https://doi.org/10.1007/978-3-540-78800-3_24)Cited by:[§III\-B3](https://arxiv.org/html/2608.07540#S3.SS2.SSS3.p2.2)\.
- \[6\]Y\. Hao, X\. Wan, and C\. Zhai\(2025\)An investigation of robustness of llms in mathematical reasoning: benchmarking with mathematically\-equivalent transformation of advanced mathematical problems\.arXiv preprint arXiv:2508\.08833\.Cited by:[§I](https://arxiv.org/html/2608.07540#S1.p4.1),[§II\-B](https://arxiv.org/html/2608.07540#S2.SS2.p1.1)\.
- \[7\]D\. Hendrycks, C\. Burns, S\. Kadavath, A\. Arora, S\. Basart, E\. Tang, D\. Song, and J\. Steinhardt\(2021\)Measuring mathematical problem solving with the math dataset\.InProceedings of the Neural Information Processing Systems Track on Datasets and Benchmarks,Cited by:[§I](https://arxiv.org/html/2608.07540#S1.p4.1),[§II\-A](https://arxiv.org/html/2608.07540#S2.SS1.p1.1)\.
- \[8\]K\. Huang, J\. Guo, Z\. Li, X\. Ji, J\. Ge, W\. Li, Y\. Guo, T\. Cai, H\. Yuan, R\. Wang, Y\. Wu, M\. Yin, S\. Tang, Y\. Huang, C\. Jin, X\. Chen, C\. Zhang, and M\. Wang\(2025\)MATH\-perturb: benchmarking llms’ math reasoning abilities against hard perturbations\.arXiv preprint arXiv:2502\.06453\.Cited by:[§I](https://arxiv.org/html/2608.07540#S1.p4.1),[§II\-B](https://arxiv.org/html/2608.07540#S2.SS2.p1.1)\.
- \[9\]A\. Lewkowycz, A\. Andreassen, D\. Dohan, E\. Dyer, H\. Michalewski, V\. Ramasesh, A\. Slone, C\. Anil, I\. Schlag, T\. Gutman\-Solo, Y\. Wu, B\. Neyshabur, G\. Gur\-Ari, and V\. Misra\(2022\)Solving quantitative reasoning problems with language models\.InAdvances in Neural Information Processing Systems,Cited by:[§I](https://arxiv.org/html/2608.07540#S1.p4.1),[§II\-A](https://arxiv.org/html/2608.07540#S2.SS1.p1.1)\.
- \[10\]F\. Mazdarani and C\. Toxtli\(2026\-07\)Beyond the answer key: robustness evaluation of large language models for step\-level mathematical verification\.Note:ResearchGate preprintPreprintExternal Links:[Document](https://dx.doi.org/10.13140/RG.2.2.11471.65443),[Link](https://doi.org/10.13140/RG.2.2.11471.65443)Cited by:[§II\-B](https://arxiv.org/html/2608.07540#S2.SS2.p1.1)\.
- \[11\]I\. Mirzadeh, K\. Alizadeh, H\. Shahrokhi, O\. Tuzel, S\. Bengio, and M\. Farajtabar\(2025\)GSM\-Symbolic: understanding the limitations of mathematical reasoning in large language models\.InProceedings of the International Conference on Learning Representations,Cited by:[§II\-B](https://arxiv.org/html/2608.07540#S2.SS2.p1.1)\.
- \[12\]S\. Polu and I\. Sutskever\(2020\)Generative language modeling for automated theorem proving\.arXiv preprint arXiv:2009\.03393\.Cited by:[§I](https://arxiv.org/html/2608.07540#S1.p4.1),[§II\-A](https://arxiv.org/html/2608.07540#S2.SS1.p1.1)\.
- \[13\]P\. Scharpf, M\. Schubotz, H\. S\. Cohl, C\. Breitinger, and B\. Gipp\(2023\)Discovery and recognition of formula concepts using machine learning\.Scientometrics128,pp\. 2715–2737\.Cited by:[§I](https://arxiv.org/html/2608.07540#S1.p1.1),[§I](https://arxiv.org/html/2608.07540#S1.p3.1),[§II\-C](https://arxiv.org/html/2608.07540#S2.SS3.p1.1)\.
- \[14\]W\. Shen, J\. Wang, and J\. Han\(2015\)Entity linking with a knowledge base: issues, techniques, and solutions\.IEEE Transactions on Knowledge and Data Engineering27\(2\),pp\. 443–460\.Cited by:[§II\-C](https://arxiv.org/html/2608.07540#S2.SS3.p1.1)\.
- \[15\]Y\. Wu, A\. Q\. Jiang, W\. Li, M\. N\. Rabe, C\. Staats, M\. Jamnik, and C\. Szegedy\(2022\)Autoformalization with large language models\.InAdvances in Neural Information Processing Systems,Cited by:[§I](https://arxiv.org/html/2608.07540#S1.p4.1),[§II\-A](https://arxiv.org/html/2608.07540#S2.SS1.p1.1)\.
- \[16\]K\. Yang, A\. M\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. Prenger, and A\. Anandkumar\(2023\)LeanDojo: theorem proving with retrieval\-augmented language models\.InAdvances in Neural Information Processing Systems,Cited by:[§I](https://arxiv.org/html/2608.07540#S1.p1.1),[§I](https://arxiv.org/html/2608.07540#S1.p3.1),[§II\-C](https://arxiv.org/html/2608.07540#S2.SS3.p1.1)\.
- \[17\]L\. S\. Zettlemoyer and M\. Collins\(2005\)Learning to map sentences to logical form: structured classification with probabilistic categorial grammars\.InProceedings of the Twenty\-First Conference on Uncertainty in Artificial Intelligence,UAI ’05,Arlington, Virginia, USA,pp\. 658–666\.External Links:[Link](https://dl.acm.org/doi/10.5555/3020336.3020416)Cited by:[§II\-C](https://arxiv.org/html/2608.07540#S2.SS3.p1.1)\.
- \[18\]K\. Zheng, J\. M\. Han, and S\. Polu\(2021\)MiniF2F: a cross\-system benchmark for formal olympiad\-level mathematics\.arXiv preprint arXiv:2109\.00110\.Cited by:[§I](https://arxiv.org/html/2608.07540#S1.p4.1),[§II\-A](https://arxiv.org/html/2608.07540#S2.SS1.p1.1)\.
- \[19\]Z\. Zhou, S\. Liu, M\. Ning, W\. Liu, J\. Wang, D\. F\. Wong, X\. Huang, Q\. Wang, and K\. Huang\(2025\)Is your model really a good math reasoner? evaluating mathematical reasoning with checklist\.InProceedings of the International Conference on Learning Representations,Cited by:[§II\-B](https://arxiv.org/html/2608.07540#S2.SS2.p1.1)\.