ALPS：用数学构造度量大语言模型的有效创造力

大语言模型会产出以发现面目出现的输出——新证明、新猜想或新分子。这样一个看似有创造性的输出是否真正原创且有效，很难判定：开放式输出需要主观判断，输出可能复制训练中见过的内容，或者任务可能过于简单而无需创造力。我们提出ALPS（Austin-Law Proof-Synthesis），一个设计用来度量有效创造力的基准：产出一个既原创又能被证明正确的解。每个实例是一条单一的等式定律，并经认证：要么需要构造一个满足该定律的无限数学结构，要么需要证明不存在这样的结构。提交的解答由自动化证明检查器验证，无需人工参与；一个公开的生成器可以无限制地产生新实例，因此LLM永远不会在可能见过的问题上被评估。由八个领先自动证明器配置组成的组合解决了4,141条定律评估池中的2.2%，而预算提高二十倍仅再增加0.6%：障碍不是算力，而是缺乏能产出每条定律所需定制结构的方法。在固定协议下，我们测试的最强推理模型在证明侧14%的实例上成功，但在构造侧无一成功。评估池其余97.2%在我们测试的所有配置与预算下均未解决。我们完整发布ALPS：语料库、生成器与自动化评判器。