TREAT: Evaluating Access to Formal Knowledge across Equivalent Mathematical Representations

The paper introduces TREAT (Theorem Recognition under Equivalence-preserving mAthematical Transformation), a benchmark for evaluating whether large language models can recover known theorem identities from equivalence-preserving formula-level transformations. The central research question is whether formal knowledge remains accessible when its representation changes.

The paper frames the core issue as 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. The authors argue this problem 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. The paper notes that a system may therefore appear to know a concept in its standard form while failing to identify or use it when the representation changes."

The 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. The paper connects this to premise selection in formal theorem proving, noting premise selection has long been identified as a major bottleneck in large mathematical libraries, and to formula-concept recognition work showing formula meaning cannot be reduced to surface notation.

The benchmark is constructed from theorem-related pages in English Wikipedia. The pipeline filters entries for usable mathematical expression forms, requiring that a retained entry 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. The final corpus contains 737 theorem identities selected from a 2456-row raw inventory.

Variant generation uses a taxonomy of equivalence-preserving transformation families, including "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. GPT-5 Pro generates candidate variants conditioned on the theorem name, canonical statement, assumptions, canonical condition, and a target transformation family, producing a transformed mathematical condition together with an inverse-mapping note explaining how the transformed form reduces back to the canonical condition. The final benchmark consists of 29,480 transformed rows."

Validation uses Gemini 3.1 Pro, which 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 is used as an additional validation layer, checking whether the transformation template preserves the encoded theorem condition by asserting the negated equivalence (C ∧ ¬V) ∨ (¬C ∧ V) and accepting when this formula is unsatisfiable under the recorded abstraction and assumptions. A manual inspection of a 100-row validation subset did not identify any mathematically wrong theorem mapping or counterexample.

The evaluation panel is designed to separate theorem unfamiliarity from representation-dependent access failure. Models are first probed for familiarity with theorem identities in standard form, and the shared-known panel is constructed from theorem concepts that appear in the common known set, sampling 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.

The 960-item panel covers 504 Analysis items, 180 Algebra/Linear Algebra items, 156 Probability/Information Theory items, 78 Number Theory items, and 42 Combinatorics/Graph Theory items. Each evaluation input contains only the transformed mathematical statement and the minimal surrounding text needed to parse it, without theorem family, subfield, candidate list, original theorem name, canonical condition, or transformation type. Models must return "a structured JSON response indicating whether a valid theorem route exists, the predicted theorem name or NONE, relevant aliases, a short connection explaining the match, a brief justification sketch, any missing assumptions, and a confidence score."

The primary metric is exact theorem-identification accuracy, with normalization handling capitalization, punctuation, possessives, parenthetical aliases, selected synonym forms, and minor eponym-order variations. Additional metrics include family accuracy, asserted rate, wrong-named rate, NONE rate, and malformed-output rate.

The headline result: "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%. The paper concludes: theorem familiarity in standard form does not guarantee access to the same theorem after an equivalence-preserving change in representation."

The gap between exact and family accuracy is small, only about 0.6–3.7 percentage points, meaning many failures are not merely alias or near-miss problems within the right area of mathematics.

The paper decomposes failures into three modes. First, abstention: the model returns NONE even though every main benchmark item has a gold theorem identity. GPT-OSS 120B abstains on 831 items; Qwen3 Coder 480B and Gemma 3 27B abstain on roughly half the panel. Second, wrong commitments: the model asserts a theorem name, but the theorem is incorrect. GPT-5.4 Pro asserts on 789 items with 73.9% exact among assertions and 21.7% wrong; Gemini 3.1 Pro asserts on 675 items with 74.7% exact and 23.6% wrong. Third, interface failure: Qwen3 Coder 480B has a 25.21% malformed-output rate despite having the highest conditional precision among asserted theorem names at 93.8%.

The paper notes: 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 changes how the leaderboard should be interpreted: Qwen3 Coder 480B has lower all-item accuracy but is exact on 93.8% of assertions, while GPT-5.4 Pro has higher coverage but more wrong-theorem risk.

The family matrix analysis shows recognition depends on the interaction between the transformed representation and the mathematical neighborhood in which the theorem lives. GPT-5.4 Pro is strongest on Analysis and Probability/Information Theory, while Gemini 3.1 Pro is higher on Algebra/Linear Algebra, Number Theory, and the small Combinatorics/Graph Theory slice.

Transformation type also matters. 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 with only 28 items. Among larger buckets, counting/combinatorial, proof-intermediate, and probabilistic/distributional transformations cluster around 44–45% mean exact accuracy. The paper concludes: 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.

The TTC study evaluates retry-after-failure prompting, family hints, and transformation-type hints on both positive rows and matched negative/bait rows. The strongest recovery 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 best for Qwen, improving from 46.88% to 77.50%, a gain of 30.62 points.

The paper emphasizes that positive recovery and safety are different properties. Gemma 27B family hints improve positive accuracy by 16.15 points but produce 329 false named routes out of 960 negative rows, or 34.27%. Gemma 12B family hints are safer, improving by 17.29 with 0/960 false routes. The paper concludes: the same intervention type can be helpful for one model and unsafe for another.

The paper lists several limitations. First, TREAT is restricted to theorem concepts with recoverable mathematical expression forms, excluding conceptual, geometric, algorithmic, or prose-based results. Second, the corpus is shaped by its source inventory and filtering pipeline, with some families and transformation buckets better represented than others. Third, 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 outside the SMT fragment. Fourth, the shared-known panel controls for theorem familiarity only approximately. Finally, the TTC study does not exhaust the space of retrieval, verification, constrained decoding, tool use, or multi-step reasoning strategies.

The paper claims four contributions: (1) formulating theorem recognition under equivalence-preserving transformation as a controlled evaluation of representation-robust access to formal knowledge; (2) introducing TREAT with formula-level transformations, recorded assumptions, inverse mappings, and validation metadata; (3) providing a six-model evaluation showing that theorem recognition remains far from saturated even on frontier models; and (4) analyzing 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.

Based on the paper, here are the specific improvements I can make to AI systems, along with what the improved system can do:

Improvement: I will add a representation-shift detection layer to the system's knowledge retrieval pipeline. Before retrieving a theorem or formal object, the system will explicitly test whether the input's mathematical form matches the canonical form of any known object. If not, it will attempt to map the input through a set of equivalence-preserving transformations (residual, slack, operator, integral, etc.) to a canonical form.

What the improved system can do:

• Recognize a known theorem even when it is presented as a residual equation, witness statement, optimization identity, set relation, or proof-intermediate form.

• Avoid false negatives where the system says I don't know simply because the surface form is unfamiliar.

• Retrieve the correct formal handle (e.g., Cauchy-Schwarz inequality) from a mathematically equivalent but structurally different condition.

The improved system will:

• Retrieve known theorems from unfamiliar but equivalent mathematical forms.

• Abstain safely when uncertain, or commit with calibrated confidence.

• Recover from failures using guided hints without increasing false routes.

• Produce structured, auditable, and machine-readable outputs.

• Route retrieval by mathematical family and transformation type for higher accuracy.

• Check assumptions and flag conditional matches.

• Adapt its retrieval policy to the task's risk tolerance and the model's strengths.

This makes the system suitable for formal theorem proving, premise selection, mathematical information retrieval, and any domain where stable access to formal knowledge under representational variation is critical.