VeRA: Math Benchmarks as Executable Specifications

Most reasoning benchmarks are static: the same problems are reused repeatedly, enabling memorization, format exploitation, and saturation. To measure genuine AI progress we need evaluation that is robust by construction, not by post-hoc detection. We propose VeRA (Verified Reasoning Data Augmentation), a framework that compiles benchmark problems into executable specifications consisting of a natural-language template with slots, a coherent generator that samples valid configurations, and a deterministic verifier that validates assignments and computes canonical answers. Once a specification is validated, labels for any newly sampled instance come from executing the verifier, so correctness amortizes across an unbounded stream of fresh variants at near-zero marginal cost. VeRA has two modes. VeRA-E, the equivalent mode, rewrites problems while keeping the underlying logic intact and supports memorization and robustness diagnostics. VeRA-H and VeRA-H-Pro, the hardened modes, systematically increase complexity while remaining verifiable. Evaluating 16 frontier models on GSM8K, AIME-2024 and 2025, Beyond-AIME, AMO-Bench, and GPQA-Diamond shows that VeRA-E exposes robustness and familiarity effects, with 4× dispersion on GSM8K and a Teacher-robust, statistically significant AIME-2024 versus 2025 gap, while VeRA-H and VeRA-H-Pro generate fresh verified tasks that restore headroom on saturated benchmarks. Beyond the automatic pipeline, we release human-audited Verified datasets, comprising 220 of 220 VeRA-E items and 2,187 of 2,299 expert-audited VeRA-H and VeRA-H-Pro items at 95.13% retention, together with a stricter pair-preserving Verified Full release. All code and datasets are made open-source at https://github.com/Marco-Cheng/VeRA.