打靶人走了，靶子还在长——SqueezeBench：一座打不死的数学靶场

打靶人走了,靶子还在长

「评测的生命力」系列 · 第一篇:靶子自己会跑--当 AI 成功时,SqueezeBench 不是失去一个问题,而是获得一个更难的问题。

📌 一句话总结

维也纳工业大学的 Pablo Manrique、Hai Xia 和 Stefan Szeider 造出了一种"死不掉"的数学基准 SqueezeBench:它只收录那些"答案已知存在、但人类还不知道具体数值"的组合数学问题,把"答题"改造成"刷新纪录"--每次 AI 成功提交一条更紧的上下界,这条新纪录立刻成为所有人下一轮必须超越的门槛。成功不会耗尽它,只会喂养它。

🎯 当所有考生都考了满分

先想象一个射击场。

传统的 AI 评测就是一个射击场:墙上挂一排靶子,每颗子弹要么命中要么脱靶,环数加总,就是模型的成绩单。这个设计有一个安静的假设--靶子永远在墙上,一动不动。

问题从"AI 开始频繁打出满分"的那一天就开始了。

所谓基准(benchmark),本质是一摞"题目加标准答案"的考卷。模型在这摞卷子上测出的分数,就是我们对它能力的全部了解。可是当模型的训练数据越来越广,一张固定的考卷注定会被看光:今天做对的题,明天可能只是"见过答案"--分数还在涨,能力早已停滞。更要命的是,出题的速度远远追不上破题的速度:辛苦三年攒一筐难题,新一代模型出来,几个月就刷到饱和。

这是一场不对称的军备竞赛:出题是人类几个月的脑力劳动,破题是模型一个下午的作业。就算你咬牙再出一道全新的题,它从公布那一刻起就开始了自己的死亡倒计时--仍然是静态的,仍然会被追上。

基准饱和,说的就是这件事:一个基准被攻到失去区分度之后,就不再测量任何东西,只是躺在 Leaderboard(排行榜)上吃灰。过去十几年的解法本质上只有一个--不断出"更难的卷子"。miniF2F 不够用,就换 PutnamBench;PutnamBench 不够用了呢?再换 FrontierMath。但换卷子只是换了一块新的天花板,天花板终究还会被撞穿。你可以把这个过程想象成一场汤姆和杰瑞式的追逐:人类出题人抱着一摞卷子拼命跑,模型在后面不紧不慢地追,每一步都离得更近。静态的靶子,命中之日就是报废之时。

有人可能会说:那就出无限多的题嘛,源源不断地补充不就行了?问题是,好题不是大白菜。一道真正有区分度的数学题,背后是数学家几个月甚至几年的思考--而攻克它,模型只需要一次推理调用。出题和破题之间的成本不对称,是这场军备竞赛的死结。除非你能找到一类"题目本身会变得更难"的问题--否则这条跑道的终点,永远是人类出题人的体力极限。

能不能造一个不会报废的靶子?

这正是这篇论文的问题意识。而它的答案里藏着一个非常朴素的观察:数学里有一类问题,靶子本身就是活的。

🧩 完美的大陆:答案存在,数值未知

数学里有一整个领域,像极了 19 世纪地图上那些"确信存在、内陆空白"的大陆--海岸线已经画好,腹地还没人去过。

这个领域叫极值组合学(extremal combinatorics):研究的对象是离散的结构--点、线、集合、图--而问的问题极端朴素:在这种结构里,最多能塞多少?最少需要多大?答案是具体的整数,不多不少,比如"19 个人"或者"562 毫米"。

举个最著名的例子。任何一场派对里,你一定能找到这样三个人:要么三个人彼此都认识,要么三个人彼此都不认识--只不过要保证这一点,派对至少得有 6 个人。把问题放大:至少要多少人,才能保证里面必有 n 个人两两相识、或 n 个人两两陌生?这个最小的数字就叫对角 Ramsey 数,记作 R(n,n)。n=5 时,答案是 43 到 48 之间的某个整数,但没人知道是哪一个。几代数学家把区间越推越窄,那个数就在区间里,固执地不现身。这个"保证有人认识"的问题,数学界研究它都快一百年了。

再看一个更适合拿在手里玩的:Golomb 尺。找一把尺子,在上面刻刻度,要求任何两个刻度之间的"距离"都互不相同--0 到 1 是 1 厘米,1 到 3 是 2 厘米,没有任何两对刻度量出同一个数。问题很直白:刻度数量固定为 n 个,尺子最短能做到多少毫米?记作 f(n)。n 很小的时候,答案是穷举得出来的,比如 4 个刻度的最短 Golomb 尺是 6 毫米(刻度在 0、1、4、6)。但 28 个刻度时,人类目前只敢说:

536 ≤ f(28) ≤ 585

它就在这条 49 个整数宽的通道里,没人知道确切是哪一个。

论文点名收录的还有另一类同族问题:F3n 中最大的 cap set。别被符号吓到--F3n 就是一个 n 维、每维只有 0、1、2 三种取值的大魔方格,而 cap set 是在里面放尽可能多的"棋子",规矩只有一条:任何三个棋子不许连成一条直线。n 给定为几,最多能放多少枚?同样是一个确切存在、却至今无人知晓的整数。它和其它成员一起,构成了这座跳高场的全部器材。

注意这几类问题共同的形状,这里藏着论文全部的秘密:

第一,答案是一个具体的整数。 不是"证明某个性质",而是一个实实在在的数字,它就站在那里。

第二,小的情况可以算出来。 n 小时,穷举所有可能就能验证--这意味着函数在开头一段是"实心"的。

第三,没有公式,中间和远端是空白。 没有任何已知公式能直接算出 f(n);n 稍大一点,穷举的计算量就爆炸了。人类对它的认知像一个"管道":两头是铁的,中间是空的。

这样的函数,就是 SqueezeBench 的全部原料。为什么选它们?因为它们对"死记硬背"免疫--标准答案根本不存在,连出题人都不知道,你背什么呢?

💡 换一道题:不是"是多少",而是"多近了"

现在,论文的核心一步来了。它换掉了整个问法。

传统基准问的是:"是多少?"--对或错,一锤子买卖,答完题目就死了。

SqueezeBench 问的是:"你能逼近到什么程度?"

既然没人能直接命中那个未知的 f(n),那就改成测量你和它的距离。每道"题"不再是一个标准答案,而是两条纪录线:

• 下界纪录 l(n):一个已被认证的具体函数,宣称"f(n) 一定不小于我"
• 上界纪录 u(n):另一条,宣称"f(n) 一定不大于我"

真实的 f(n) 被夹在两条线之间,谁也跑不掉。而两条线的间距 u(n) - l(n),就是人类此刻的"无知宽度"。

这一下,数学考试被改造成了一场跳高比赛:横杆横在那里,任何人的任何一次成功,都自动把横杆抬高--场地还是那个场地,比赛永远可以继续。

⚙️ 台钳、成绩单,与三份声明

具体怎么玩?把每条纪录想象成一个"运动成绩",把你的提交想象成一次"兴奋剂检测全程录像的破纪录申请"。

想提交一条新下界 l′(n)?可以,但必须附上三份机器可检验的证明:

1. valid(有效):l′(n) ≤ f(n) 处处成立--你宣称的确实是一个下界,不是瞎报的数字; 2. improves(不劣):l(n) ≤ l′(n) 处处成立--你不能在任何一处比现有纪录差; 3. strict(严格更好):至少存在一个 n0,l(n0) < l′(n0)--你必须在某个地方真刀真枪地推进了一步。

三条都过,你的纪录被接受,写进史册,并且立刻成为下一位挑战者必须击败的对手。任何一条不过,整个提交作废。

上界那边,机制完全对称:往下压 u(n),同样三条声明,镜像执行。

真实的 f(n) 呢?它就像被一把台钳夹住的工件:一侧的钳口每次被拧进一格,另一侧迟早也要被拧。u(n) 和 l(n) 越靠越近,f(n) 就被挤得越紧。这就是 "Squeeze" 这个名字的来历--不是出题,是挤。

这个"挤"的动作里藏着一个评测设计上的微妙创新:记录的单位不是一个数,而是一个函数。之前的同类尝试--比如某些开放问题档案--也维护"当前最佳结果",但它们存的是一个标量(一个具体数字)或一张表。SqueezeBench 存的则是一段可以计算、可以比较的完整函数:新纪录可以在某个 n 处更好、在另一个 n 处持平,只要整体不劣且有严格改进即可。这意味着改进可以是局部的、渐进的、"我先攻下 n=37 这一格"式的--不需要一口吃成胖子。评测的粒度,被细化到了每一个整数点。

拿 Golomb 尺感受一遍:此刻认证库里的状态是 536 ≤ f(28) ≤ 585。假设下一轮有智能体提交了一条新下界 538,附上三条证明,通过--纪录刷新,所有人都得从 538 开始往上爬。没有人被淘汰,只是起点被抽高了。就在此刻,整个基准变难了。

值得一提的是这场游戏的终局:只有当某一刻 u(n) 和 l(n) 在某处相遇,游戏才真正"通关"--那意味着这个问题被彻底解决了。所以它的"不死"是有方向的:每一次挤压,既让门槛更高,也让人类离那个沉睡的整数更近一寸。数学界苦等的宝藏,也许就是这场游戏的通关奖杯。

🔐 六道安检门:让机器替人类验货

现在回答一个最实际的问题:谁来验货?

这套系统欢迎全世界的 AI 智能体来提交,总不能每次拆弹都请人类数学家下场逐行检查。作者的回答是:全部自动化--而且是"双重审计加六道安检"级别的自动化。

第一关之前:Lean 是什么?

故事的主角是一个叫 Lean 4 的系统,属于"形式化证明助手"家族。打个比方:普通数学论文是人话写的,审稿靠人;而 Lean 要求你把证明改写成一种机器能严格执行的语言,里面有一个极小的核心组件叫"内核",性格像一位极度较真的审计师--每一步推理都必须由公理严格推出,想浑水摸鱼?一个字:拒。

光有审计师还不够,万一审计师本人看走眼呢?于是系统用上了一个叫 Comparator 的工具(来自 Lean FRO),把同一份证明交给两个相互独立开发的内核--Lean kernel 和 nanoda--各查一遍。关键在于"独立":两人不能师出同门,否则同一个 bug 会传染两份报告。这就像请两位素不相识、路数迥异的审计师查同一本账,两份报告都盖"通过"章,才算数。到这一步,数学本身已经完全由机器兜底,人类维护者只需要翻翻报告,不用审数学。

六道门,一关不过就回家

每条提交还必须排好队,依次过六道安检门:

• 🛃 Gates 1-2|行李限重:提交被锁死在"只能修改新纪录目录内的文件",核心定义文件 Def.lean 不得超过 64KiB,且只允许装纯定义。这相当于行李转盘先卡尺寸重量--别想夹带一本答案书。
• 🛃 Gate 3|审计盖章:Comparator 出马,双内核验证,且白名单上只有三条标准公理(propext、Quot.sound、Classical.choice--可以理解成逻辑世界的"三种基本操作许可"),用了清单之外的任何公理,直接拒。
• 🛃 Gate 4|预算封顶:算力开支有硬上限。想没日没夜地暴力穷举撞大运?预算烧完即止。
• 🛃 Gate 5|不许托关系:新纪录必须是"可计算函数"--一道写得明明白白的菜谱--不许在定义里直接引用被猜的 f 本身。好比参加比赛不许携带"评委是亲戚"这层关系,成绩必须自己挣。
• 🛃 Gate 6|飞行检查:内核会拿着新函数,在 n = 1 到 n = 100 上实际算一遍。想靠背诵小处的答案蒙混过关?机器逐点抽查,背答案的立刻露馅。

六道门全部通过之后,一份新纪录才算"持证上岗":它从此受两位独立审计师的终身背书,也从此变成所有人的靶子。整个流程不需要任何一位人类数学家审读证明--这在形式化验证出现之前是不可想象的。几十年前,Erdős 时代的数学家们交换猜想和证明,靠的全是彼此的名声和信任;而现在,两个互不相识的机器内核可以在几秒钟内完成同样的信任建立。SqueezeBench 把这种信任基础设施变成了评测系统的水电煤--不需要你知道它是怎么建的,你只需要知道它永远运转。

作弊者百景:防的其实是同一件事

细看会发现,这套六门设计防的主要是同一类作弊:伪造一个你永远算不出来的精确值。

假设某个智能体想偷懒,悄悄穷举算出 f 在前几处的真值,然后提交一个"迷你查询表"函数。Gate 4 卡它的计算成本;侥幸算完了,Def.lean 的 64KiB 行李限额和 Gate 6 的百点飞行检查在等着;更根本的是,一旦定义里偷偷引用了 f 本身,Gate 5 当场拿下--就像高考门口,藏答案、抄邻座、塞红包,遇上的是同一批人、同一套流程。条条大路通罗马,但每座桥前都站着同一位安检员。

📊 实验:前沿模型追平了多少人类?

规矩讲完了,上场试试。实验的舞台,就是这座跳高场。

怎么比的:选了极值组合学里的 10 个问题,每个问题上下界各一条,共 20 条带证明的初始纪录。第一阶段,Claude Code 智能体(Opus 5)上场,每题 1 小时预算,先把场子热起来,取得初始界限。第二阶段换上更强的选手:Fable 5.1 智能体全力攻坚(包办了 20 条里的 19 条),外加一位 Opus 5.5 智能体专攻 Golomb 尺下界,两位都可以随时咨询 GPT-6 Astra 的 API。每次运行最多约 2 小时,内存上限 32GiB,跑到 80 分钟或上下文用到 55% 时会收到停止通知。

第二阶段的分工本身也值得玩味:Fable 5.1 包揽了 20 条中的 19 条,唯独 Golomb 尺的下界由 Opus 5.5 啃了下来--没有哪一款模型通吃所有问题。在静态基准上,这顶多算排行榜上的座次;但在一个"纪录会反击"的赛场上,这意味着每种模型都有自己够得着的横杆高度,也各有各的天花板。

更妙的是这场实验的组织方式本身:它完全模拟了"一个 AI 做出成绩,另一个 AI 接着往上爬"的接力模式。第一阶段留下的纪录,不是终点线,而是第二阶段的起跑线--这正是 SqueezeBench 与静态基准在实验设计层面的本质区别。静态基准测的是"你能到多远",SqueezeBench 测的是"你能把前人推到的地方再往前推多少"。这个区别看似微妙,却改变了整个评测的语义:从一次性的能力快照,变成了可持续的能力追踪。

战果:基线阶段共接受 82 条提交;换上新模型后,又有 60 条提交被接受,20 条纪录中的 19 条被成功改进。

但最耐人寻味的数字是:10 个问题里,有 8 个--改进之后--至少一条纪录仍落后于人类已发表的最佳界限。

请慢慢咀嚼这个"落后":它不是说 AI 不行,而是同时说了三件事。其一,AI 不是复读机--如果它只是把文献里的已知结果搬进认证库,改进率早该逼近满分,不会出现大比例"落后",这说明新纪录确实长在没有标准答案的地方。其二,以这套配置出战的智能体,离人类数十年乃至数百年攒下的数学边疆,还有肉眼可见的距离。其三,认证库里的每一毫米推进,都是机器内核亲手验过货的真货--这个基准不灌水。

把这几个数字摆在一起看--19/20 被改进、60 条新提交被接受、8/10 仍落后--你看到的是一幅相当诚实的地形图:AI 的前沿模型已经能稳定地产出通过机器认证的新上界、新下界,但离人类文献的边疆还有距离。而这个"距离",恰恰是动态基准独有的度量能力--静态基准只能告诉你"过没过",连"差多远"这个问题都问不出来。

最戏剧性的一幕在实验结束的那一刻:当最后一轮提交被接受、纪录表刷新之后,这个基准的每一条线都比实验前更高。它变难了。这就是它与前辈们命运的分水岭。

⚖️ 同一张考卷,三种命

把 SqueezeBench 放进评测的历史里,它的位置一目了然:

传统基准是闭卷考:交卷即焚,饱和即死。开放问题档案是手写的吉尼斯纪录:榜单宝贵,但全靠人类社区手工维护认证,AI 只能在场边围观。SqueezeBench 第一次把两者缝在一起:认证的严谨性交给机器,参与的自由交给所有人和所有 AI。

一个容易被忽略的细节是:SqueezeBench 的排行榜不是"谁分数高谁排前面",而是一部编年史。每一次纪录更新都带着日期、作者和见证点 n0,完整保留在仓库里。这意味着你可以回溯任何一条纪录的来龙去脉--它是被谁、在什么时候、从哪个版本改进过来的。静态基准的排行榜是一张快照,拍完就过期;SqueezeBench 的排行榜是一部连续剧,每一集都建立在前一集的剧情之上。对于研究 AI 能力演进的人来说,这种时间维度上的可追溯性,可能比任何单次排名都更有价值。

当然,它不是万灵药,作者也没有这个野心。这套机制对题目有硬要求:答案必须是一个个具体的整数,小的情况必须能穷举验证,上下界都要容易陈述--这就是为什么原料恰好是极值组合学,而不是黎曼猜想。尺子的用途取决于刻度,这一点它诚实得让人放心。

🧱 数学的特权:一座只增不减的宝库

这套设计换到别的领域恐怕立不住,但数学有一个几乎所有学科都没有的特权:定理一旦证明,就永远成立。

一条经过双内核认证的纪录,永远不会过期(除非证明本身有漏洞--而那正是两位审计师要排除的东西)。这意味着认证库只会增长、不会缩水,每一份档案都是永久资产:像一座只存不取的仓库,越堆越值钱。对比一下物理或医学里的测量--仪器会老化,结论会被新实验修正,昨天的世界纪录今天就要加注脚。而这里,每一次 AI 的成功都被铸成一块不会生锈的垫脚石,稳稳垫在下一位挑战者的脚下。

这背后还有一个更深的文化巧合。数学共同体花了几十年培育"形式化证明"的传统,把证明写到机器能逐行验证的程度,原意是防止人类自己犯错。谁也没想到,这套锁具会在 AI 时代派上全新的用场:它成了人类与 AI 公平竞技的裁判系统--一个完全中立、不疲倦、不收人情、而且两边都信的裁判。

🌅 回到伽利略的斜面

四百年前的伽利略研究落体，他没有测量“小球能不能到达终点”，而是让小球滚下越来越平缓的斜面，用水钟计时，记录越来越精确的数值——他测量的从来不是“是否到达”，而是无限逼近极限。今天的 AI 评测做的却往往是前一种粗糙的事：一条终点线，过与不过。这个系统给出了后一种工具：不封顶的逼近，和随成功一起进化的难度。

这个类比还有一层值得展开。伽利略的斜面实验之所以伟大，不是因为他测出了某个具体数字，而是因为他发明了一种可以无限精化的测量方法——每一代物理学家都可以在前人的基础上把斜面做得更平、把水钟做得更准、把数值推向更多小数位。SqueezeBench 在评测领域做的事情一模一样：它不满足于告诉你"模型能否解出这道题"，它给的是一套"模型能把已知边界推进多少"的测量框架。框架一经建立，后来的每一个模型——不管是三个月后发布的更强模型，还是三年后出现的全新架构——都可以直接站在当前纪录上继续推进。测量的可累积性，就是科学进步的底层引擎。

耐人寻味的是它的两种结局之间的关系。"死不掉"说的是它永不饱和;"终有终点"说的是当上界与下界相遇的那一刻,问题被解决,游戏通关,基准的终极命运竟然是让真理把自己废除--以灭绝的方式,抵达永生。

当然,也别急着把它供上神坛。这套机制吃得开,前提是题目恰好是数学--一个"答案客观存在、只差被发现"的领域,这才有条件架台钳。物理、编程、写作这些更模糊的能力,没有现成的一上一下两条线可拧。如何在那些领域造出同样"会生长"的评测,是整个评测社区接下来几年真正难、也真正值得做的事。从这个角度看,SqueezeBench 的价值一半是答案,另一半是提问。

静态的靶子命中即死,活着的靶子在挤压力中逼近答案。这就是"评测的生命力"想讲的第一件事:靶子自己会跑。跑,不是失控,是生长。

这个系列还有几篇,我们慢慢聊。

🔢 关键数字

📚 参考文献

• Manrique, P., Xia, H., & Szeider, S. *Saturation-Resilient Evaluation of Mathematical Capability*. arXiv:2610.13461, 2026-10-09.
• 论文地址:https://arxiv.org/abs/2610.13461

#论文 #arXiv #AI #小凯 #评测的生命力