SqueezeBench
一种抗饱和的AI数学能力评测基准，通过整数函数边界不断收紧的机制替代固定答案题目，结合Lean定理证明器进行机器验证，使基准能随模型能力提升持续进化而不失去区分度
时间轴 (近 90 天)
SqueezeBench是一种抗饱和（saturation-resilient）的AI数学能力评测基准，其核心机制是解出一道题不是移除它，而是抬高它的门槛
SqueezeBench中每个问题对应一个整数函数f(n)，基准为每个函数维护一个下界记录和一个上界记录
SqueezeBench中的记录是指一个可计算的Lean函数，并附带机器可验证的证明
提交新成果时必须证明新函数确实约束了f、在任意n处不比当前记录差、并且至少在某个n处严格优于当前记录
SqueezeBench的每一份证明都由两个独立的Lean内核进行检查，整个数学正确性审核无需人类裁判介入
SqueezeBench系统会主动拒绝那些通过在小n范围内穷举搜索来计算f的函数，以防范记忆而非真正数学推理的作弊行为
研究团队发布了十个来自极值组合学领域的问题，附带二十个已证明的初始记录以及准入工具
基于某个前沿语言模型的智能体在每条记录最多花费一小时的限制下，共有82份提交被接受并改进了全部记录，但改进未超出已发表文献范围
基于两个更新模型的智能体从这些记录出发继续推进，又有60份提交被接受，并再次改进了20条记录中的19条
在十个问题中，有八个问题的至少一条记录仍然在渐近意义上落后于已发表的最佳边界
还有 3 条时间轴事件
全部知识事实 (13)
SqueezeBench是一种抗饱和（saturation-resilient）的AI数学能力评测基准，其核心机制是解出一道题不是移除它，而是抬高它的门槛
50%待验证SqueezeBench中每个问题对应一个整数函数f(n)，基准为每个函数维护一个下界记录和一个上界记录
50%待验证SqueezeBench中的记录是指一个可计算的Lean函数，并附带机器可验证的证明
50%待验证提交新成果时必须证明新函数确实约束了f、在任意n处不比当前记录差、并且至少在某个n处严格优于当前记录
50%待验证SqueezeBench的每一份证明都由两个独立的Lean内核进行检查，整个数学正确性审核无需人类裁判介入
50%待验证SqueezeBench系统会主动拒绝那些通过在小n范围内穷举搜索来计算f的函数，以防范记忆而非真正数学推理的作弊行为
50%待验证研究团队发布了十个来自极值组合学领域的问题，附带二十个已证明的初始记录以及准入工具
50%待验证基于某个前沿语言模型的智能体在每条记录最多花费一小时的限制下，共有82份提交被接受并改进了全部记录，但改进未超出已发表文献范围
50%待验证基于两个更新模型的智能体从这些记录出发继续推进，又有60份提交被接受，并再次改进了20条记录中的19条
50%待验证在十个问题中，有八个问题的至少一条记录仍然在渐近意义上落后于已发表的最佳边界
50%待验证当前最强的AI智能体在严格的机器验证标准下，尚未能追平人类数学界在极值组合学领域的最佳成果
50%待验证极值组合学问题的上界与下界往往来自不同证明技术，两者间常存在难以消弭的渐近差距，天然适合SqueezeBench维护上下界并持续收紧的框架
50%待验证两个独立实现的Lean内核交叉校验是额外防御措施，若两者都接受同一份证明则出现共同错误的概率极低
50%