ALPS: Measuring Valid Creativity in Large Language Models with Mathematical Construction
2026-08-17 • Artificial Intelligence
Artificial Intelligence
AI summaryⓘ
The authors created ALPS, a test to see if language models can truly create new and correct mathematical proofs or structures. The test involves tricky math problems that need either building a special infinite structure or proving none exists. Their automated system checks solutions without humans, making sure models aren’t just repeating known answers. Results show current models and provers solve only a small fraction of problems, revealing the difficulty of creating original math reasoning. The authors provide the full test setup for others to try and improve on.
large language modelsproof synthesisequational lawsautomated theorem provinginfinite mathematical structuresproof verificationbenchmarkmathematical creativityautomated judgeopen-ended problems
Authors
Eric Xie, Wenqian Ye, Aidong Zhang
Abstract
Large language models produce outputs presented as discoveries - new proofs, conjectures, or molecules. Whether such an output that appears creative is truly original and effective is hard to establish: open-ended outputs require subjective judgment, the output may replicate something seen in training, or the task may be too simple to need creativity. We present ALPS (Austin-Law Proof-Synthesis), a benchmark that designs a task to measure valid creativity: producing a solution that is original and can be proven correct. Each instance is a single equational law, certified to require either the construction of an infinite mathematical structure satisfying the law, or a proof that no such structure exists. Submissions are verified by automated proof checking with no human involvement, and a public generator produces new instances without limit, so LLMs are never evaluated on problems they may have seen. A portfolio of eight configurations of leading automated provers resolves 2.2% of the 4,141-law evaluation pool, and a twentyfold budget increase adds 0.6%: the obstacle is not compute, but the absence of any method that produces the tailored structure each law requires. Under a fixed protocol, the strongest reasoning model we test succeeds in 14% of instances on the proof side, but none on the construction side. The remaining 97.2% of the pool is unresolved at every configuration and budget we test. We release ALPS in full: the corpus, the generator, and the automated judge.