跳到正文
1836 · 开源社区

1836 · 开源社区

AI时代的人本基建

登录/注册
← 返回项目《初焰 • 纳宙 第一赛季 - 风象议题 08 天秤座》

钠衡 · 研究成果与洞见

参与共建发布

robinbg · 发布于 2026/10/16 · 更新于 2026/10/17

RO

robinbg2026/10/16

0. 一句话

钠衡是一套钠离子电池全生命周期运维工作台，它把「状态估计 — 条件寿命 — 事件风险 — 充放电与热管理 — 收益核算 — 主动学习 — 失配撤回 — 模组与更换决策」串成一条可复现的闭环；并且用 Lean 4 机器-checked 的化学与寿命理论去约束运行时行为，而不是把证明当作装饰性徽章。

我们最想请评委注意的，不是"做了多少功能"，而是这套系统在什么地方拒绝给出答案——以及我们在这个过程中得到的、可以推广到别的领域的四个洞见。

1. 实际建成的能力（均可复现）

能力实际状态
形式化理论核心178 条导出声明全部通过 Lean 4.19 内核检查，逐条传递公理审计只依赖 propext、Classical.choice、Quot.sound，无 sorry/admit/自定义结论公理。分布：化学 42、状态归约 72、寿命 30、输出合同 34
数值—理论连接瞬时速率残差预算实际参与每个后验样本的动作准入；模型包绑定精确源码字节，每次执行前复核；理论引用在界面与工件中可逐条回溯
状态估计双位点储钠模型上的粒子滤波（64 个表示样本），联合高斯观察器，未来观测走独立滤波，历史 Run 不被改写
条件寿命（RUL）保存真实协议容量与局部穿越诊断；16 个首次退役时刻如实显示"未知"，不做插值
事件风险5 类原生事件（电压下/上限、温度下/上限、储库耗尽）分别给出后验加权概率；显式标注 population_calibration: not_performed，不称为运营事故概率
控制非线性名义 MPC（SLSQP）+ 全后验场景可行性校验；热管理以 COP 折算电耗入账；九维策略空间（充电双档、放电双档、截止电压、DoD、制冷/制热许可、静置时长）
收益能量账本只记真实执行的能量流；预测能量与终端价值一律不入账；退化损失不重复扣减
主动学习约束贝叶斯优化 + 多保真自回归 GP（ρ 由配对样本最小二乘辨识）+ 成本感知采集；三臂对照（价值查询 / 随机 / 不确定性）各 36 次真实查询
数据公开钠电测量 1,240,278 行冻结，训练/验证/测试角色按电芯与批次锁定，首次冻结后不再用于调参
参考模型固定版本 PyBaMM sodium_ion.BasicDFN / Chayambuka2022 实际运行，作为独立对照而非本项目结论来源
工作台七页 Web（总览/状态/寿命/风险/策略收益/仿真对照/理论证据），真实保存、重载、回放、报告下载；回放显式标注 independent_sample=false
回归1153 项测试通过、23 项子测试（当前 4 项失败已在 §7 定位并修复，验证进行中）

任务账本：45 项任务、18 项需求全部保留，35 项已按原验收条件完成。完整发布门 verify --profile release 仍为退出码 2（受阻/未验收），我们没有把它调成通过。

2. 洞见一：把"未知"当一等公民，系统才真正可用

大多数电池数字孪生的失效方式不是算错，而是在该说"不知道"的地方给了一个数。钠衡在四个层面把 UNKNOWN 做成了一等状态，而且这不是保守姿态，是可用性的来源：

  • 寿命：容量协议只在网格点上被观测。网格观察不能证明网格之间的首次穿越时刻。所以 16 个退役时刻显示"未知"并附原因，而不是用单调性假设外推一个日期。运维方拿到的是一个可以据以安排复检的区间，而不是一个会被追溯为"系统说过 2027 年 3 月"的假精确值。
  • 风险：模型内 5 类事件的越限率，与"起火概率"是不同的东西。系统把它们分开命名，并明确 risk_certificate=false、人群标定未执行。析钠代理、电压越限、退役、火灾从不被合并成一个"失效事件"。
  • 准入：适用性未知不默认放行。模型包超出适用域时返回 unknown，动作被 withheld，而不是回退到一个"看起来安全"的默认策略。
  • 学习：UNKNOWN 的执行消耗预算但绝不获得数值标签。36 次查询里 34 次 UNKNOWN，就如实记 34 次，不插补、不剔除、不当作"负样本"。

可推广的价值：这套"未知语义"是可以直接搬到任何带安全后果的预测系统里的设计规范——它把"模型不知道"从工程负债变成了可审计的输出字段。

3. 洞见二：形式化证明只有在改变运行时行为时才有意义

我们给自己定了一条消融判据：如果把证明徽章从界面上隐藏、而数值行为完全不变，那么系统性能应当一模一样。这条判据逼着我们回答"证明到底用在哪了"，答案是三个真实调用点：

  1. 模型包适用域——定理的条件（共同温度因子、参数范围、物理域、正速率）被写进模型包，运行时逐条核对；
  2. 误差预算——瞬时速率残差界进入每一步的表示后验计算与动作准入；
  3. 状态归约与切换——精确聚合的充要条件决定"组总量"何时足以替代完整位点状态。

绑定是字节级的：4 条 T0 证明绑定精确的状态/参数/源码哈希，每次执行前复核；证据被撤回或过期，严格权限立即失效，不复用旧指针。

理论侧的具体结果（模型内，非新自然规律）

  • ClassSufficiency.lean：给出组总量对真实总储钠导数与俘获速率充分的充要分类——当且仅当同组内 r = a+b+c 与 c 分别相同；允许 a 在组内异质。附四位点到两组的正速率实例，以及"总量不充分"的反例。
  • GivenAmountResidual.lean：由三角不等式与容量加权系数均值导出 |R| ≤ min(δq, δ(C−q))。一个显式物理有理实例把界从 δC = 2δ 收到 δ/2（4 倍收紧）。但更重要的是我们证明了：一般参数下两种预算没有无条件的大小顺序，必须在同一状态与参数下分别比较。这条"不能一般化"的结论本身，就是防止误用的护栏。
  • 反例是成果的一部分：异质双位点组成在显式时间轨迹下不闭合；平/无穿越情形不产生无条件 RUL。这些都实际通过了 Lean 检查，而不是被绕过。

边界：以上是在已声明的合成模型上的形式化，属于既有数学结构（精确/受约束 lumping、CLUE 框架、不变流形）的特例与工程连接。我们没有通过穷尽文献确认其数学新颖性，也不主张发现了新的钠电自然规律。模型内证明不是现实电芯的安全认证。

4. 洞见三：墙钟预算会让算法对比整体失效（本轮新发现）

这是本轮接手后最有推广价值的一个发现，因为它推翻了我们自己的一组实验结论。

现象

主动学习要求对比三种查询策略，每臂 36 次真实查询。结果是：价值查询 2 个有效、随机 2 个有效、不确定性 0 个有效。看起来像是"不确定性采样在这个问题上完全无效"。

真相

三臂共用同一种子和同一 Latin Hypercube 初始设计，所以前 12 个候选逐字节相同。我们检查了其中第 6 个候选在三臂里的执行记录：

臂声明的工作量实际完成的工作量单步墙钟判定
价值查询24 次评估 / 120 s 上限24 次评估、128 次积分0.74 s完成
随机同上24 次评估、128 次积分（完全相同）1.33 s6.02 s 被杀 → UNKNOWN
不确定性同上未及记录—6.04 s 被杀 → UNKNOWN

同一份确定性工作，墙钟耗时从 0.55 秒摆动到超过 6 秒。 三臂是严格串行运行的（时间窗互不重叠），所以不是彼此争抢 CPU，而是宿主背景负载。

问题出在：每次评估的预算里混进了一个 6 秒的内层墙钟守卫，它位于工作循环内部，会在声明的工作量跑完之前就把计算掐断。于是——

训练标签变成了机器负载的函数，而不是候选参数的函数。

而这一个硬币的正反面，恰好决定了该臂能否找到第一个可行点，进而决定整臂的退出码是 0 还是 2。所谓"不确定性采样 0 有效"，测量的其实是那台机器在那 22 分钟里的负载曲线。

修复与验证

把保真度改为只由工作量单位定义（优化器迭代数、候选评估数——这两个数值一个都没改），墙钟降级为宿主资源后备，并在代码里断言它不可能抢先于每查询预算。物理模型、动作准入、预算配置、UNKNOWN 语义全部未动。

修复后重复执行同一候选：

  • 低保真（原分歧点）：5/5 次全部完成，效用值完全一致（3.0302705698157835e-09），工作量计数器一致，单步墙钟 0.91–1.44 s，对 25 s 后备有约 17–27 倍余量；
  • 高保真：3/3 次全部完成，效用与约束裕度一致，四个 MPC 步骤的逐步工作序列完全相同。

为什么这条洞见值得单独讲

它不只属于这个项目。任何仿真在环的优化、硬件在环测试、AutoML 基准、强化学习评测都在用"每次评估限时 N 秒"来保证公平。只要被评估的工作量是确定的、而时限是墙钟的，负载就会渗透进标签，而且它不会报错——它会安静地让某个算法看起来更差。

可操作的结论有三条：

  1. 用工作量单位定义保真度（迭代数、评估数、网格分辨率），墙钟只作为宿主保护，不参与判定；
  2. 算法对比必须做同输入复现测试：同一个候选跑 N 次，断言标签与工作量计数器逐次相同。这比我们最初写的任何统计检验都更早地暴露了问题；
  3. 警惕"一致的 UNKNOWN"——我们的第一版探针因为 5 次重复都返回 UNKNOWN 而判定"可复现"并退出 0。那是空洞通过。现在只要没真正跑到计算内核，一律判为"未测试"。

5. 洞见四：负结果同样是结果，而且我们保留了它们

这个项目里有几处"没有赢"的地方，我们选择如实公开，因为它们比赢更有信息量：

  • 学习效用低于穷举：A01 的实测效用为 学习 5.3994 / 随机 4.4846 / 穷举 5.9590。学习策略明显优于随机，但不及穷举。我们没有把它包装成"学习方法领先"。在 144 个训练点、九维空间、每次评估约 1 秒的预算下，穷举仍然可行——这本身就是关于问题规模的有用结论。
  • 跨体系迁移没有优势：把公开钠电数据做电压迁移计算后，MAE 未显示优势，且冻结 cohort 的实物物性映射仍为 UNKNOWN。这一项（D02）因此保持未完成，而不是用"迁移可行"含糊过去。
  • 相关性 ρ 未被辨识：多保真的核心是低/高保真差异，但真实配对数只有 1，ρ 仍取默认单位值并显式标注 rho_estimation: default_unit_not_identified。我们没有据此声称"已学会保真度差异"。
  • 108 次请求 ≠ 108 个独立样本：同一后验缓存下的重复查询不构成统计独立。科学新增样本数在所有工件中恒为 scientific_N_added: 0。

这些负结果共同说明一件事：当前的合成闭环验证的是工程与方法的正确性，不是收益优势或安全概率。 后者需要真实电芯、独立轨迹和预登记实验，那部分仍是未完成项。

6. 潜在应用价值

以下均标注为潜在——它们描述的是这套方法在补齐真实数据后可以支撑什么，不是已验证的收益承诺。

① 储能电站 / 工商业储能的钠电运营 九维策略空间本身就是运营决策集：充放电双档电流、截止电压、DoD 上限、制冷/制热许可、静置时长。系统按真实执行的能量流和分时电价核算现金流，并把热管理电耗按 COP 计入成本。对钠电尤其相关——它的优势场景正是对成本敏感、对能量密度不敏感的固定式储能。

② 质保、残值与备付决策 一个会说"这 16 个退役时刻未知，原因是只有网格观测"的系统，比一个给出插值日期的系统更适合进入财务与保险流程。显式 UNKNOWN 让复检计划、质保拨备和梯次利用定价有了可审计的依据。

③ 模型治理与认证工件的范式 "模型包 = 数学对象 + 适用条件 + 误差界 + 源码字节哈希，且每次执行前复核"这个模式，可以直接迁移到任何需要论证可信度的场景：安全关键软件的功能安全论证、AI 系统的合规文档、监管提交材料。它的价值在于条件与模型不可分离——超出适用域时系统自动降级为 unknown，而不是继续输出。

④ 模型漂移下的车队管理 失配处理与证据撤回是实际实现的功能：当某个模型映射事后被发现有偏差，依赖它的自动动作会停止，未服务的能量被如实记账，而不是静默回退到默认策略。这对任何"模型上线后才发现问题"的车队/机群运维都是可复用的模式。

⑤ 仿真在环基准的方法学 §4 的工作量预算与同输入复现测试，可以作为任何 sim-in-the-loop / HIL / AutoML 评测的通用检查项。这是本项目外溢性最强的一条。

7. 诚实的边界（本轮修复状态）

未完成、且我们不声称完成的：

  • 真实电芯物性映射与实物身份（D02）——阻塞于冻结 cohort 缺少可接纳的一手物性来源；新论文与仿真不能替代对应测量。
  • 三组独立验收实验 E-T / E-A / E-L（X02/X03/X04）——依赖预登记与强基线协议（X01），后者依赖 A03、P03、D02。
  • 真实运营风险上界与收益领先——risk_certificate=false 恒成立；k=0, N=299 的单次零事件检验尚未在真实轨迹上执行。
  • 完整发布门退出码 2。

本轮已修复、验证进行中的：

  1. A03 标签不可复现（§4）——已修复并用重复执行探针验证；三臂尚未在新源码上重跑，因此 A03 仍为进行中，未升级为完成。
  2. smoke 门 4 项失败——已定性为两个根因：(a) 新增的证明隔离测试把 pytest 临时目录当作证明输出，被项目的授权根守卫正确拒收（该守卫同时禁止 reparse point，因此不能用链接绕过）；(b) 临时目录路径触及 Windows 260 字符边界，换短路径后同一组生命周期测试 5/5 通过。另发现并修复了一个被 (a) 掩盖的真实缺陷：证据回读未声明编码，在中文 Windows 上按 GBK 解码 UTF-8 的 JSON 而失败——这是一个与区域设置相关的可移植性缺陷。全部断言逐字保留，未放宽任何守卫。

8. 可复现性

# 环境体检（Python / Lean 4.19 / Lake / uv / npm）
.venv/Scripts/python.exe -m naheng.cli doctor                       # → exit 0

# 形式核心：178 条声明的内核检查与三公理审计
.venv/Scripts/python.exe -m naheng.cli formal check --suite core    # → status checked, exit 0

# 标签确定性诊断（只读，比对封存工件）
.venv/Scripts/python.exe tools/diagnose_a03_label_determinism_20261016.py \
    --out artifacts/review/a03-label-determinism-20261016-a/diagnosis.json   # → exit 1 = 检出不可复现

# 同输入重复执行探针（可证伪）
.venv/Scripts/python.exe tools/probe_a03_label_determinism_20261016.py \
    --ordinal 6 --fidelity low --repetitions 5 --out artifacts/a03-determinism-probe-20261016-c

# 完整发布门（如实返回受阻）
.venv/Scripts/python.exe -m naheng.cli verify --profile release     # → exit 2

关键工件

内容路径
178 条核心声明的内核检查与公理审计artifacts/formal/core/manifest.json
主张与证据边界（工程通过 / UNKNOWN / 科研未验收分列）docs/CLAIMS.md
理论成果身份与已有文献对照docs/NOVELTY.md
三臂对比的原始账本与图表artifacts/review/a03-new-9593-independent-20261016-c/、artifacts/reports/learning-9593-20261016-d/
标签不可复现的诊断与探针证据artifacts/review/a03-label-determinism-20261016-a/、artifacts/a03-determinism-probe-20261016-*/
实施状态与全部真实命令、退出码docs/STATUS.md

所有首次失败、超时与废弃判据的产物均按原样保留，未由重跑覆盖。

本报告不主张收益领先、概率保证、真实电芯安全认证或新的自然规律。合成计算、参考仿真、公开测量与回放四类证据在全部工件中分开标注。

PE

Peter YU2026/10/16 23:28:15

很强~

登录后可以留言