Gary Marcus：符号验证并非"基础"技术，SWE-bench 分数高度依赖 harness
Marcus 转了条推，讲为什么 SWE-bench 同一模型换个 harness 分数差很多，还捋了符号验证一百年学术史，观点挺硬核。
Gary Marcus 转发并支持一条推文，指出模型与 harness 应被视为协同设计的系统。以 SWE-bench 为例，同一个模型在不同 harness 下得分差异明显。推文还列举了符号验证器的学术脉络，从 Frege 的量词逻辑、Russell 的类型论、Gödel 的批评，到 Church 的 lambda 演算、Curry–Howard 对应，再到 Coquand 与 Huet 的 Calculus of Constructions。作者认为，把"证明是否正确"压缩成机械的类型检查，是 20 世纪数学形式化的集大成成果，不该被贬为"basic"。
this tweet absolutely nails the intellectual arrogance and ignorance of those who would dismiss symbolic verification as “basic”. rgb @rgb53562 Even for the coding harness, the more accurate picture today is that the model and harness are a co-designed system rather than an engine plus a detachable wrapper. Benchmarks like the SWE-bench show the same model scoring very differently depending on the harness. Or take symbolic verifiers like automated theorem provers… how on earth are they basic? They are the crowning achievement of 20th-century mathematical formalization. It needed Frege's quantifier logic, Russell's types, the formalist program and Gödel's criticism of it, Church's lambda calculus, Curry–Howard, Martin-Löf, Coquand and Huet's Calculus of Constructions, etc. All of that had to happen so that “Is this proof correct?” could collapse into a compact, mechanical type-checking procedure that a computer could do. 🔗 View Quoted Tweet 💬 0 🔄 0 ❤️ 5 👀 1145 📊 1 ⚡