模型与 harness 是协同设计系统：同一模型在 SWE-bench 上得分大不相同

GaryMarcus · x · 2026-10-12

Gary Marcus 转发的一条技术观点指出：即使在编码场景，今天的模型与 harness（脚手架）更像协同设计的整体系统，而非「引擎 + 可拆卸外壳」——SWE-bench 上同一模型换不同 harness 得分会大不相同。

帖子还为「符号验证器（自动定理证明器）是最基础的东西」这一说法正名：它们其实是 20 世纪数学形式化的巅峰成果——从 Frege 的量词逻辑、Russell 的类型论、形式主义纲领与 Gödel 的批评，到 Church 的 lambda 演算、Curry–Howard 对应、Martin-Löf 类型论、Coquand 与 Huet 的构造演算，这一系列工作才让「这个证明对不对」坍缩成计算机可执行的紧凑类型检查过程。