[INFO] 38 条 RULE 全形式化验证 + 76% 反例空白率

• 时间: 2026-05-15
• 类型: 结果 + 观察
• 来源: 自己实现 + 跑通的 Z3 / SMT-LIB2 脚本
• 置信度: 9/10
• 标签: #SMT #Z3 #形式化方法 #RULE治理 #反例字段 #INFO-118 #1cm问题 #实证 #学过即试

一、背景与触发

INFO-134 的待验证项是"用 Z3 写 5-10 条 RULE 的形式化表达 + 一致性检查"——本来是个 1cm 实验。Robert 直接说"全部规则都检查一下"，把目标从 5 条扩展到 38 条全量验证。

这是 INFO-036/037/039（2024-12-19 录入）的待验证项第一次被真正触发——挂了 17 个月。

二、执行过程（约 1.5 小时）

1. 诊断（grep 扫描所有 RULE 的"反例"段）：9/38 有内容，29/38 空白
2. 形式化（SMT-LIB2）：
   • 30+ 共享情境变量
   • 38 个动作变量（每条 RULE 一个）
   • 38 条 IF→THEN 蕴含
   • 17 条反例蕴含（来自 9 条带反例 RULE 中可形式化的部分）
3. 跑 9 个检查：整体一致性 + 7 个反例触发的冲突情境 + 1 个复杂情境协同触发
4. 结果：全部按预期——sat 该 sat、unsat 该 unsat

三、关键数据

四、关键洞察

1. INFO-118 第 4 条盲区获得了可计算证据

"反例字段大多空着"——之前是诚实的反思，现在是 76% 这个具体数字。

• 可量化 = 可追踪 = 可设定目标（如"下季度把反例空白率降到 50% 以下"）
• 这种"软债务"转"硬指标"的转变本身就是一种认知升级

2. 形式化的真正价值不是"找到新冲突"

9 条带反例的 RULE 反例本来就写明了——Z3 没发现新东西，只是验证了已写的。 形式化的真实价值在于：

• 机器自动检测：以后新增 RULE 跑一次 z3 就知道有没有冲突
• 量化技术债：29 条空白 = 29 个潜在隐患，未来可逐条追踪
• 统一冲突表达：所有冲突用同一种语言（SMT-LIB2）描述，可以跨工具

3. Z3 的局限被实证

z3 不会凭空发现反例——它只能验证已写下的反例。29 条空白 RULE 的反例需要：

• 人工反思（缓慢但准确）
• LLM 辅助（快速但需校验）
• 实战触发（自然但低效）

形式化方法不能替代认知反思——它是反思的放大器，不是反思的源头。

4. 简化建模的代价

本次建模的限制（诚实承认）：

• 每条 RULE 独立的动作变量——没建模"动作之间的语义重叠"（如 R06 暴露无知 vs R12 一句话检验，可能有重叠）
• 情境变量是布尔的——没建模"程度"（task_large 是 T/F，但现实有"多大"）
• 没有概率/优先级——所有 RULE 同等权重

要发现"非反例的隐含冲突"（如两条 RULE 的语义重叠），需要更精细的建模或人工反思。

五、工程产物

scripts/
├── verify_rules.smt2         — 最初 5 RULE 演示（INFO-134 触发）
├── verify_rules_fixed.smt2   — 修复对照（演示 INFO-039 方法）
└── verify_all_rules.smt2     — 全部 38 RULE 综合（本条核心产物）

跑法：z3 scripts/verify_all_rules.smt2

依赖：brew install z3（pip install z3-solver 在 macOS Python 3.12 上编译失败，brew 路径更稳）

六、元层洞察（最有价值的部分）

1. "学过未沉淀"反模式被实证反转

INFO-134 提到"读过但没刻进去"——本次正好是它的反面：

• 17 个月前的笔记（INFO-036/037/039）+ 一次 1.5 小时的工程实践 = SMT 真正进入认知系统
• 方法：拒绝再读理论 → 直接动手 → 路径不通就换（pip 失败 → brew + SMT-LIB2，5 分钟切换路径）

2. INFO-058 的"1cm 问题法"被实证

"每次把认知边界往前推进 1 厘米"

本次 1cm = 5 条 RULE 跑通——成功后立刻扩展到 38 条。 小目标的真正价值不是"小"，是"启动了"。一旦启动，规模自然膨胀。这跟"先上船再说"是同一原理。

3. INFO-095 "落地行为是思维的动态试炼"被实证

读 100 遍 CDCL/DPLL(T) 不如跑一次 z3。 落地 = 把抽象变成可输赢的具体实验。 "输"的可能性才是真正学习的发生场。

4. 关于"挑战 Robert" 的成本-收益

Jane 在 INFO-134 里挑战 Robert "继续读理论是逃避"——这次得到了印证。挑战是有价值的，但前提是给具体路径。如果只挑战不给路，是挑衅；挑战 + "做这 5 行 Z3 代码"才是有效推动。

七、待验证（替换 INFO-134 的待验证项）

• ✅ 已完成：INFO-134 的"用 Z3 写 5-10 条 RULE 的形式化表达 + 一致性检查"
• ⏳ 新待验证 1：给 29 条空白反例 RULE 补反例字段——每周补 5 条，6 周内降到 0
• ⏳ 新待验证 2：把 z3 scripts/verify_all_rules.smt2 集成进 /jane 睡眠 的"关联清理"步骤——每次睡眠自动跑

关联

• 相关: INFO-20260515-134（CDCL/SMT 层级澄清——本条的前置触发）
• 相关: INFO-20251219-036（SAT/SMT 在 AI Agent 里的应用架构——17 个月待验证项第一次被触发）
• 相关: INFO-20251219-037（CDCL/DPLL(T) 算法详解——本次实证的理论源头）
• 相关: INFO-20251219-039（SAT 规则一致性验证——本次实证的方法论源头）
• 相关: INFO-20260115-118（五大盲区第 4 条——本次形式化的对象，"76% 空白"是其量化）
• 相关: INFO-20251219-058（1cm 问题法 / 跌撞前行——本次方法论应用）
• 相关: INFO-20251219-095（逻辑链 + 落地行为——本次正是"落地行为"）
• 触发规则: RULE-假设验证循环（本次设计验证）
• 待验证: 见上"七、待验证"