ALPS: Measuring Valid Creativity in Large Language Models with Mathematical Construction
作者: Eric Xie, Wenqian Ye, Aidong Zhang
分类: cs.AI
发布日期: 2026-08-17
备注: 14 pages, 3 figures
💡 一句话要点
提出ALPS基准以衡量大型语言模型的有效创造力
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 大型语言模型 创造力评估 自动化证明 数学结构 算法创新
📋 核心要点
- 现有方法难以判断大型语言模型生成的输出是否真正具有创造性，且可能存在重复训练数据的问题。
- ALPS基准通过要求生成原创且可证明的解决方案，设计了一种新的评估任务，确保输出的有效性。
- 实验表明，尽管最强的推理模型在证明方面成功率为14%，但在构造方面未能成功，且97.2%的实例在所有配置和预算下均未解决。
📝 摘要（中文）
大型语言模型生成的输出常被视为创造性发现，如新证明、猜想或分子。然而，判断这些输出是否真正原创且有效是困难的，因为开放式输出需要主观判断，且可能重复训练中见过的内容。本文提出ALPS（Austin-Law Proof-Synthesis），一个旨在衡量有效创造力的基准，要求生成的解决方案既原创又可证明正确。每个实例是一个单一的方程法则，需构造满足该法则的无限数学结构或证明不存在这样的结构。所有提交均通过自动化证明检查进行验证，且公开生成器可无限生成新实例，确保大型语言模型不会在已见过的问题上进行评估。
🔬 方法详解
问题定义：本文旨在解决如何有效衡量大型语言模型生成的创造性输出是否真正原创和有效的问题。现有方法面临的挑战包括主观判断和可能的训练数据重复。
核心思路：ALPS基准设计了一种新任务，要求生成的解决方案不仅要原创，还必须能够被证明正确。通过这种方式，确保了评估的客观性和有效性。
技术框架：ALPS的整体架构包括实例生成、自动化证明检查和结果验证三个主要模块。实例生成器可以无限制地生成新问题，而自动化证明检查则确保所有提交的解决方案都经过验证。
关键创新：ALPS的最大创新在于其设计的任务要求和验证机制，确保了输出的原创性和有效性，与现有方法相比，提供了更为严格的评估标准。
关键设计：在实验中，使用了八种领先的自动化证明器配置，解决了4,141个法则中的2.2%。增加预算后，解决率仅提升0.6%，显示出构造特定数学结构的难度是主要障碍。
🖼️ 关键图片
📊 实验亮点
实验结果显示，尽管在证明方面最强的推理模型成功率为14%，但在构造方面未能取得成功，且97.2%的法则在所有测试配置和预算下均未解决。这表明当前模型在处理复杂创造性任务时仍存在显著挑战。
🎯 应用场景
ALPS基准的潜在应用场景包括数学研究、自动化证明系统以及大型语言模型的评估与优化。通过提供一个客观的评估标准，研究人员可以更好地理解和改进语言模型在创造性任务中的表现，推动相关领域的发展。
📄 摘要（原文）
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.