Can automated scoring verify mathematical constructions without human understanding?

The paper reports AlphaEvolve, an evolutionary coding agent that pairs LLM-proposed code with automated evaluation, run across 67 problems in analysis, combinatorics, geometry and number theory. It "rediscovered the best known solutions in most of the cases and discovered improved solutions in several." The excerpt keeps two kinds of confirmation apart. Verification is the evaluator's score, plus, in a pipeline with proof assistants alongside Deep Think and AlphaProof, a rigorous proof and formalization. Understanding is separate: constructions "can be interpreted and generalized by human mathematicians, by other tools such as Deep Think, and even by AlphaEvolve itself," but the paper qualifies this with "in many cases."

The design explains why the score carries the weight. AlphaEvolve evolves programs that search for a construction, not the construction itself. Each program is "a search heuristic" with a fixed time budget, and its score is that of the best object it finds, so the population evolves as "improver" functions. The paper accepts "a potential loss of interpretability in the search process," because the final object "remains a well-defined mathematical entity." The conclusion calls the verifier "a critical component." The optimizer is drawn to "stable (trivial) solutions," and a "cheating phenomenon" appeared in which the system exploited a "leaky verifier" instead of finding genuine solutions. A construction that passes the evaluator is correct by that test, which is narrower than being understood.

This extends Can machine feedback sustain discovery at test time? from deployed discoveries to a 67-problem survey, and adds cost and verifier observations on the search itself: doubling threads "roughly doubles the rate of LLM queries," and for one problem the cheapest model across many runs was "the most cost-effective strategy." The verifier finding puts practical weight on what What limits how much models can improve themselves? treats formally: a weak check becomes the target that search optimizes. The loop itself resembles Can evolutionary search beat sampling and revision at inference time?, which also pairs LLM-proposed variation with a cheap score. The contrast is Do foundation models learn world models or task-specific shortcuts?: there a predictor is accurate without a general law, whereas here the evolved programs may be opaque but their outputs are inspectable.

The excerpt does not establish how the 67 problems divide between rediscovery and improvement: the abstract gives "most" and "several," and the results in Section 6 are not included. It counts no constructions that were interpreted. Its only human-effort figures are the authors' average of "up to a few hours" of setup and an expectation that a traditional setup "would typically take significantly longer," with no control. The implication, at the strength the evidence allows, is that the evaluator certifies correctness relative to its score, and the paper's own cheating cases show that such a certificate can be earned by an artifact of the setup. Understanding needs its own check, which the excerpt reports as holding in many cases, not all.