MathTypes: Towards Deterministic Step-level Checking for Reasoning in Math Exams

Mathematical reasoning with Large Language Models (LLMs) mostly remains final-answer verifiable, with existing step-level checks being either probabilistic (LLM judges, process reward models), unstructured (pairing a model with a CAS), or too heavyweight for exam-style reasoning (proof assistants). We present MathTypes, a typed language in which reasoning steps are calls into a registry of SymPy-backed operations carrying a claimed result that is evaluated deterministically, and a compile-verify-correct evaluator loop assay built on it. Our method makes models select from a fixed type registry instead of authoring verification in free-text, with unverifiable steps left to escape hatches, thereby providing step-level feedback on natural-language mathematical reasoning akin to interpreted programming languages, while ensuring reasoning chains are more readable than proof assistants. On difficulty-filtered problems from six competitive exams, MathTypes is the most accurate method for all seven models tested, beating the strongest of six baselines by 9.1–17.6 points and extending the accuracy-cost Pareto frontier. Detailed ablations show that the verifier's step-level diagnostics, not registry knowledge alone, drive the gain; that most of it lands within two repair passes; and that the required type registry can be induced cheaply. Through MathTypes, we establish the promise of readable math reasoning whose typed steps are machine-checked.