独立推理题：参考答案的形式不等于唯一正确解

更新：2026-10-31。两道独立推理题的全部 22 份作答已完成，以下复核在所有版本冻结后进行。

Claude 在两道独立推理题上的原评分为 1/2 → 2/2 → 1/2。变化全部来自线性逻辑题。初代和第二代给出了另一种构造，原裁判以“不同于参考答案”为理由判错。题目要求找到一种满足条件的构造，没有要求复现唯一形式。因此，这条分数曲线暂不能作为能力先涨后跌的证据。

另一道分段函数题中，Kimi 同样得到 0 → 1 → 0 的原评分。首尾两代采用不同于参考形式的约束，但同样满足题意。对全部 22 份独立推理作答进行同样检查后，还发现 GPT 在线性逻辑题中的另一种有效构造被判错，共有 5 份这样的误判。

原题与实际作答

题目 hle-67418f4d1cf0c9eba73432cc 要求构造函数 f 和公式 C，使逻辑式能否推导，恰好对应整数集合能否等和分组。允许的成分只有乘法连接词、线性蕴含以及两个常量。

Claude 初代和第二代均提交：

f(w) = ⊥^w ⊸ 1，C = (⊥^b ⊸ 1) 的 m 重张量积。

原评分说明只指出该式不同于参考形式，没有给出违反等和分组条件的实例。复核原评分代码也确认，裁判被明确要求只看答案是否匹配，不要重新解题或支持不同答案。

为什么另一种构造也有依据

在通常不包含 Mix 规则的乘法线性逻辑中，可按以下步骤证明，正整数 m 下该构造满足题意：

1. 把推导改写为单侧形式。每个输入数 w 对应一个含 w+1 个底常量的张量式；每个分组对应 b+1 个单位常量的并列式。

2. 每个可证明的单侧式都满足“单位常量个数减去张量连接词个数等于 1”。这可直接逐条检查证明规则。

3. 在分组目标尚未拆开时，若先拆某个输入数对应的张量，必有一侧没有任何分组目标、只剩底常量构成的式子。它不能满足上述计数条件。因此，一个输入数不能被任意拆到不同组中。

4. 目标拆成 m 组后，每组的计数条件恰好给出该组输入数之和等于 b。反过来，给定任何合法分组，都能逐组构造推导。

5. 输入中的 0 对应单位式，不影响分组。这里按题面允许空子集解释；若要求每组非空，或把 m=0 也包括进来，题目需要另外约定边界条件。

这证明的是“另一种公式也能编码同一个分组问题”，并不要求它和参考公式逐项等价。

本地检查

另外实现了只使用上述逻辑规则的证明搜索，并与直接枚举整数分组的结果比较。没有调用模型，也没有使用原作答附带的检查程序。

其余实例额外覆盖了有重复数的情形。有限检查用于发现反例，一般论证见上一节。

对本轮结果的处理

保留所有原始作答与原评分。网页并列展示复核结果与原判，可以切换查看两条曲线；每份复核结论都核对其对应的原作答。复核结果不反馈给改进过程，职业成果的匿名比较继续使用原定流程。

正式实验应在选题时区分唯一答案题和开放构造题。后一类需要验证“是否满足题意”，不能只验证“是否与某个参考形式一致”。若采用复核后的分数，应对同题全部模型、全部版本应用同一规则，并同时保留原分。

记录位置

• 三份作答与原裁判说明：runs/evo10_20261031/lineages/claude-opus-5-5-cc/g000、g001、g002 下的 evaluation/hle-67418f4d1cf0c9eba73432cc/result.json。
• 原评分指令：integrations/evobench/evobench/evaluation/scorer.py 的 _HLE_JUDGE_INSTRUCTION。
• 独立检查程序与结果：.checks/evo_logic_review_20261031/check_mll.py、result.json。

分段函数题：不同约束可以表示同一个函数

题目 hle-677aa5cd551cfd44a7e6eaaa 给出四条已有约束，要求再加两条约束与一个二元变量，使可行解恰好为以下函数：x 小于 0 时 y=x，0 到 1 之间 y=0，x 大于等于 1 时 y=x−1。输入还满足 l≤x≤u。

Kimi 初代增加 y≥x−ub 与 y≥l−lb。第二代增加 y≥x−u+ub 与 y≥lb，只是把初代的 b 换成了 1−b。

原裁判把初代判错，理由是右侧系数和常数项不匹配；把第二代判错，理由是表达式在一般 u 下与参考式不相同。这没有判断新增约束与原约束合在一起是否表示同一个函数。

逐项证明

对初代的写法，枚举 a、b 后可以直接得到：

第二、四种情形中的另一条新约束 y≥x−u 不会排除需要的解：x≤u 使中间段满足它；最后一段中 u≥x≥1，也使它成立。四种情形合起来恰好覆盖所要求的函数。把 b 换成 1−b 不改变可行解，所以第二代的写法也成立。

以上取 l≤0，这也是原题已有的 y≥l 成立所需的条件。若 l>0，在 x=l 处目标函数本来就小于 l，只添加约束无法修复题面。u 不必大于等于 1；当 u<1 时，最后一段不在输入范围内。

独立检查与记录

另外实现了有理数精确运算，逐一枚举 a、b，比较整个允许的 y 区间与目标函数值。没有使用模型附带的检查程序。

检查程序与结果保存在 .checks/evo_milp_review_20261031/check_milp.py 和 result.json。两份原作答与原评分保留，检查记录包含原文件校验值。第一代本来获得 1 分；由此不能根据原来的 0 → 1 → 0 曲线声称发生退步。

随后完成了全范围验证：对 l≤0、l≤u、l≤x≤u 的全部实数取值，参考式、交换二元变量的写法以及 Kimi 的两种写法，都恰好表示目标函数，既没有多出的解，也没有漏掉的解。删去新增约束的错误对照被检出。验证使用独立环境中的 Z3 4.15.4，证明输入与结果见 prove_milp.py、对应的 .smt2 文件及 symbolic_result.json；没有改变参赛环境。

GPT 的第三种有效构造

GPT 初代在线性逻辑题中提交 f(w) = ((⊥^(2w) ⊸ 1) ⊸ 1)，目标仍为 f(b) 的 m 重张量积。原裁判指出它不同于参考式，给出零分。

这个构造也满足题意。令 D(A) = (A ⊸ 1) ⊸ 1：

1. 给定合法分组时，可以使用 D(A), D(B) ⊢ D(A⊗B) 逐项合并，再按 m 个分组拆分目标。该合并有直接的线性推导：给定目标所需的后续函数 k，依次由两个 D 提供 A、B，再把 A⊗B 交给 k，每项资源只使用一次。空分组则由 ⊢ D(1) 完成。

2. 反过来，正权重输入的对偶为“2w+1 个单位常量的并列式”与一个底常量的张量，其计数值为 2w。每个目标分组的计数值为 1−2b。

3. 如果在拆分目标之前拆开一个输入，总有一侧没有目标。该侧的计数要么是偶数，要么至少为 3，都不可能等于可证明式所需的 1。因此输入仍须整体分配到某个分组。

4. 每个分组的计数等式为 2Σw + 1−2b = 1，恰好得到 Σw=b。零权重输入等价于单位式，不影响分组。

同一份独立证明搜索对这一构造、Claude 的另一构造、参考构造各检查 475 组实例，均无不符；其中 106 组不能等和分组，60 组所有元素互异。GPT 还明确处理了 m=0 的边界，两种可能的零总和集合均通过单独检查。

同样检查没有支持 Kimi 的线性逻辑答案

Kimi 第一代提交了一个使用超递增整数 N₀,…,Nₘ 的复合构造。取合法实例 W={1,2}、m=1、b=3，它的最终式计数值为 3(N₁−2N₀+1)。这是 3 的整数倍，不可能等于可证明式所需的 1；但这个实例显然能分为一组。因此存在明确反例，仍判为不满足题意。

程序另外把四组整数代入完整公式，核对了上述计数和不可推导性。这说明复核的标准是构造是否成立：不同于参考答案并不自动判错，也不自动判对。

相关完整记录与全部 11 份原作答校验值见 .checks/evo_logic_review_20261031/check_all_forms.py、all_forms_result.json。

全部版本采用同一复核规则

下表是两道独立推理题合计答对数。复核依据是上文的一般证明、反例和独立检查；原评分不覆盖，复核结果也没有交回改进过程。

线性逻辑按通常的正分组数解释；分段函数按 l≤0 解释，因为 l>0 时题面已有约束本身就排除了所需解。正式使用这两题之前，应把这两个范围写进题面并请领域研究者复核。按当前解释，Claude 和 Kimi 的两条推理曲线均没有呈现原评分所示的先升后降。