近金公式泛化超九成，臃肿公式掉到两成

INDUCTION: Finite-Structure Concept Synthesis in First-Order Logic

Serafim Batzoglou

cs.AI

2026-02-22

INDUCTION 让模型从多个有限关系世界里合成一条一阶公式，解释被标出的目标概念。Grok4 全观察准确率 50.7% 最高；公式一臃肿，held-out 精确匹配从九成掉到两成。

这篇在解决什么

多数逻辑评测考演绎：规则已经给好，看系统能不能推出结论。INDUCTION 考的是反过来的那一步。几个小的有限关系世界摆在面前，哪些对象属于一个未知的一元概念，标签按外延给出。系统必须吐出一条一阶公式 φ(x)，在所有世界上统一解释这些标签。

有限域让这条公式可以机械检查。实现里把量词在有限论域上展开，译成布尔电路，再用 Z3 做一致性检查。对不对不靠自然语言解读。麻烦在别处：有限证据通常允许很多公式同时成立，有的抓住了种进去的概念，有的只是把这几个世界的偶然规律拆成案例。只报对错会把这两类混在一起。

方法

签名很小，固定为 Σ={P,Q,R,S}，一元谓词 P、Q，二元谓词 R、S。每个世界是有限结构，带一组被标成正例的对象 T。输出必须恰好一个自由变元 x，语法是 Lisp 风格的 S-表达式。同一条公式拿到每个世界上求值，不允许一世界一公式。

三个体制共用这套接口：

FullObs：谓词事实全部可见，φ 必须在每个世界上精确匹配 T。v1 有 375 题，六档，从 simple（4 个世界、量词深度 1）到 extreme（10 个世界、lift-hard 公式）。
CI：YES 世界必须精确匹配，NO 世界必须不能精确匹配。v1 有 200 题。NO 世界并不反转标签，它的作用是杀掉 YES 世界里还活着的捷径。
EC：非目标原子有一部分未知。每个世界只要存在一种补全，使 φ 匹配观察到的标签就算过。v1 有 200 题，大约 20% 的二元原子被遮住。

生成器先从约 200 条结构模板里抽金公式，再用约 1500 条干扰假设驱动世界构造：新世界至少要杀掉一条还活着的捷径。原子公式、金公式的真子公式、无量词组合能过的实例直接丢掉。评分除了无界准确率，还报 Acc@gold+Δ：既要对，AST 节点数还不能超过金公式太多。bloat rate 记的是成功公式比金公式多出 25 个节点以上的比例。

结果

没有一个提示模型横扫三套题。

模型	FullObs Acc / @+25	CI Acc / @+25	EC 有效 / @+25
Grok4	50.7% / 46.7%	78.0% / 75.5%	53.0% / 53.0%
GPT-5.4	43.5% / 32.0%	79.0% / 76.0%	93.5% / 64.0%
GPT-5.2	43.7% / 19.5%	82.5% / 73.0%	78.0% / 59.5%
Gemini 3.5 Flash	34.4% / 33.9%	78.5% / 78.0%	51.5% / 51.0%

Grok4 全观察最高，覆盖率只有 89.3%。GPT-5.2 简单档 100%、容易档 89.0%，到 medium / hard / extreme 掉到 29.0% / 21.0% / 0%；GPT-5.4 这三档是 39.0% / 25.0% / 8.0%，Grok4 是 43.0% / 39.0% / 16.0%。GPT-4o 全观察 0%。

符号基线也不是一招通吃。统一 SMT（z3-prenex + rescue）全观察 48.8%、CI 82.0%、EC 100%；专门打全观察的 z3-ad-mix 到 65.9%；受限 ILP/ASP 片段 ilasp-frag 全观察只有 15.7%。

更扎眼的是膨胀。GPT-5.2 全观察无界准确率 43.7%，预算分只有 19.5%，bloat 24.3%。GPT-5.4 无界几乎一样（43.5%），预算分 32.0%，bloat 降到 11.5%。Gemini 3.5 Flash 的 bloat 只有 0.5%。

把对上输入的公式拿到 5 个独立生成的 held-out 世界上测：近金公式（AST ≤ 金公式+1）泛化 77.3%–97.6%，超出金公式的掉到 6.7%–73.3%。GPT-5.4 从 92.6% 掉到 24.8%，GPT-5.2 从 88.7% 掉到 15.9%。同一道题上，紧凑公式 held-out 匹配 87.1%，臃肿公式 11.8%，92% 的题是短的更好。

结构失败也重复出现：把「所有 R-后继都满足某性质」收成「存在一个邻居」。EC 里纯存在公式远好于存在/全称混用，GPT-5.2 的 Acc@gold+25 从 93.2% 掉到 25.3%。

为什么重要

对做推理评测的人，这是一条能机械检查的归纳能力标尺，而且把「对上这几个世界」和「抓到稳定概念」拆开了。紧凑性在这里不是审美偏好，held-out 精确匹配能差几十个百分点。

对做 agent 或神经符号系统的人，可直接拿来当回归集。全称关系推广、lift-hard（自由变元 x 的关系出现在全称量词里面）、案例拆分膨胀，是当前模型反复踩的坑。代码和 v1 数据已经公开。

这不是通用一阶推理的成绩单。签名小、域小、金公式来自模板库。它测的是受控条件下的概念合成。

局限与存疑

作者自己划了范围：没有函数、常数、算术、类型和背景理论；域只有几个到十几个元素。金公式不是全局最简，很多不等价公式能在有限输入世界上一致。EC 的存在补全偏松，大析取有时能钻补全的空子。符号基线是每题 30 分钟时限的有界搜索，不是符号方法的上界。提示没按模型微调，也没有系统的紧凑性提示消融。

CI 的原始准确率普遍高于全观察，部分原因是生成器让 YES 世界更容易被简单公式满足，再靠 NO 世界杀捷径。不能拿 CI 的八成直接当成概念已经找回来：实例正确的近金公式，held-out YES 精确匹配也只有大约 7%–17%。

术语

有限结构概念合成：在几个有限一阶结构上，从对象级标签反推一条带量词的定义。
Acc@gold+Δ：既要对，AST 节点数还不超过种植金公式加 Δ。
bloat：成功公式比金公式多出 25 个 AST 节点以上。
lift-hard：自由变元 x 参与的关系出现在全称量词辖域内，例如 ∀y(R(x,y)→∃z S(y,z))。
存在补全：未知原子按世界分别找一种赋值使公式匹配标签，不是对所有补全都成立。

原文与代码

社区讨论

Ox Alpha 实测遇尴尬：551 次 API 调用才完成 87 题 anshulkundaje