钠衡——可验证电化学模型驱动的钠电全生命周期 AI 运维
robinbg · 发布于 2026/10/9 · 更新于 2026/10/9
robinbg2026/10/9
让每一次钠电运维决策，都有状态依据、化学依据和收益依据。
项目摘要
钠衡面向钠离子电池的电芯与模组级运维，拟构建一套集状态评估、寿命预测、风险预警、充放电策略和全生命周期收益优化于一体的 AI 系统。项目以机理约束的概率状态模型为共同基础，让不同功能使用一致的状态解释、参数不确定性与运行记录，在同一验收口径下比较安全和经济性。
项目同时开展电化学模型的形式化研究：以储钠位点和副反应为明确对象，利用 AI 搜索状态归约、有效近似及适用条件，并通过反例和证明检查形成可复用的化学知识。相关结论将进入可执行模型包，直接服务状态估计、寿命计算、模型切换和动作准入，而不只是作为系统外部的理论说明。
验证以计算机仿真为主，结合公开真实钠电数据校验。拟交付可运行的 Web 工作台、完整仿真闭环、形式模型与证明工件，以及可复现的对照实验。软件功能、理论成果及二者的实际连接将分别接受检验。
对赛题的回应
| 赛题要求 | 项目回应 |
|---|---|
| 用 AI 研究钠电的状态、寿命与风险 | 从统一状态模型输出健康与内部状态估计、条件化寿命分布及事件级风险。 |
| 将安全预警、充放电策略和收益优化纳入同一套管理方案 | 贯通观测、预测、决策、仿真执行、收益核算与反馈修正。 |
| 让安全与经济性共同接受检验 | 在统一风险定义、独立测试与完整成本核算下，比较风险—收益前沿。 |
**项目范围：**电芯与模组级的预测性运维和决策支持。当前为研究与实现提案；软件、证明和效果指标均以实际交付与验证结果为准。真实设备阶段不替代电池管理系统（BMS）的实时保护。
一、项目目标与完整应用能力
运维者需要同时回答三个问题：电池当前状态如何，继续运行会怎样，以及接下来应当采取什么策略。钠衡拟把这些问题放入同一条计算链，使收益计算能够反映退化代价，使风险判断能够反映状态不确定性，也使模型不适用时的限制能够传递到实际建议。
应用目标是交付完整工作台；研究目标是形成有化学含义的形式模型与推导；连接目标是让这些理论结果实际参与运维。 三项成果共同构成项目，而非相互替代。
1.1 面向用户的功能与输出
| 功能 | 用户获得的结果 | 关键计算要求 |
|---|---|---|
| 状态与健康评估 | 荷电状态（SOC）、健康状态（SOH）、可用容量、内阻、极化及热状态与区间 | 使用电压、电流、温度历史；对无法充分识别的隐状态保留不确定性。 |
| 寿命预测 | 不同未来策略下的剩余寿命（RUL）分布、容量与内阻轨迹、退役时间区间 | 绑定环境、测试协议与退役定义，不把寿命当作与策略无关的常数。 |
| 风险评估与安全预警 | 电压、温度、功率等事件风险；析钠相关代理事件；预警原因和建议 | 区分运行越限、模型失配、证据不足和未覆盖的故障机制。 |
| 充放电与热管理 | 分 SOC 段倍率、截止电压、放电深度、预热／冷却及时序建议 | 在硬保护边界、模型适用条件和经检验的风险要求内决策。 |
| 全生命周期收益 | 净收益及其区间、成本明细、策略对比和风险—收益前沿 | 统一计入购售电、热管理、维护、更换与残值，避免重复计算退化损失。 |
| 主动学习与失配处理 | 高价值仿真查询、边界修订、证据撤回、模型升级与重新验收 | 数据异常时允许扩大不确定性、收缩动作范围，而非始终增加信心。 |
| 模组与生命周期管理 | 单体差异、共同功率约束、退化反馈策略、退役／更换情景 | 持续模拟“策略影响退化、退化改变策略”的反馈，考虑共同环境及耦合。 |
| 运行与结果追溯 | 场景配置、交互仿真、批量实验、固定回放、证据卡和报告导出 | 画面、指标和结论关联同一运行编号、模型标识和实际计算记录。 |
1.2 从单次建议走向完整生命周期
系统不仅比较某一时刻的充电动作，还将跟踪策略如何改变容量、内阻和后续可用功率，并据此更新寿命、风险与未来收益。模组层保留单体差异和共同约束，不把多个单体的结论未经组合分析直接当作模组保证。
二、总体架构：化学模型贯通运维决策
项目采用三层协同架构。化学理论与发现层产生模型和证据，可信模型与决策层执行估计和优化，运维交付层把结果变成可使用、可追溯的软件。三层共享模型定义和记录接口，但控制模型、参考模型与外部校验保持必要独立。
2.1 三层架构
| 层级 | 主要工作 | 输出及去向 |
|---|---|---|
| 化学理论与发现层 | 定义物种、反应、储钠位点及外部驱动；搜索归约条件；寻找反例；检查推导 | 形式模型、定理或候选命题、适用域、误差结论与依赖说明，组成模型包。 |
| 可信模型与决策层 | 状态推断、模型有效性检查、寿命与风险预测、滚动优化、主动查询 | 后验状态、事件风险、策略、准入结果和收益预测，供运行服务调用。 |
| 运维交付层 | 场景配置、交互计算、批量仿真、回放、审计与解释 | Web 工作台、数据接口、策略证据卡、对照报告及可运行交付包。 |
2.2 统一概率状态模型
系统拟将电压、电流、温度和允许的历史信息作为基础观测，并保留增量容量分析（ICA）与阻抗诊断接口及其使用条件。通过机理约束状态空间模型和贝叶斯推断，表示当前状态及参数的不确定性；寿命、风险和收益基于同一状态快照与模型包计算。
推断方法将根据状态维数和计算预算选择粒子滤波等合适方案。参考仿真的内部状态可用于训练与评价，所有控制方法使用同等可见观测；隐状态难以识别时，输出分布、集合或需要追加诊断的说明。
2.3 两条相互连接的闭环
**运行闭环：**持续观测 → 状态推断 → 模型有效性检查 → 寿命与风险预测 → 经济优化 → 动作准入 → 仿真执行或影子建议 → 新观测与审计。
**研究闭环：**运行残差或参考模型暴露问题 → AI 提出新状态、归约或条件 → 反例搜索与证明检查 → 模型包更新 → 独立回归测试 → 进入运行闭环。
研究闭环主要离线执行；在线系统调用已经生成的模型与证据，避免把昂贵的定理搜索放入每一个快速控制周期。模型更新通过适用条件检查和验收后，再进入运行链。
同一套状态解释服务全部运维功能；独立的参考与测试负责检验它是否值得使用。
三、研究核心：从电化学机制到可检查的有效规律
钠衡拟在明确的电化学模型族内推进化学形式化与局部公理化：把物种、反应、物质与电荷收支、适用假设及模型间推导组织为计算机可检查的知识体系。研究对象是化学模型本身，而不只是在给定模型上验证控制器。[1–4]
首批实例选择两类可逆储钠位点与一个显式副反应通道，再向明确的一族模型扩展。它是用于研究的有效模型，不被视为对所有真实硬碳微观机制的完整描述；应用仍覆盖单体、热、老化和模组功能，不同组件分别标明证据范围。
3.1 基础对象与假设体系
拟形式化物种的元素组成、电荷、相与单位，反应的计量和边界交换，位点总量与占据范围，以及外界输入的电功和热交换。一般数学结构、物理建模原则、材料本构假设与数据识别参数分别登记。
拟采用 Lean 表达化学对象与目标命题，并开展库存与电荷收支、位点约束和所选框架下热力学一致性的基础证明。充电涉及外部功输入；变温系统还需要独立的热收支描述，不能直接沿用封闭等温系统的自由能递减结论。[2] 已知关系的形式化与新发现的命题分开报告。
3.2 研究问题一：哪些储钠状态可以合并？
拟研究在位点异质性、外部驱动和副反应耦合下，哪些聚合变量能保留总库存、可观测响应及指定反应量；何时仅能近似，误差又有多大。状态不足时，反例应能指出需要补充的变量或历史信息。
例如，两组内部位点分布可能具有相同总储量，却在所选动力学中产生不同的后续变化。本项目将以这类模型检验归约条件，而非仅训练更大的预测器。研究也区分“一个状态对预测必需”和“该状态能否由现有传感器识别”。
3.3 研究问题二：副反应怎样导出寿命规律？
拟从声明的反应—传输假设出发，推导库存、膜层或阻抗相关量的变化，进一步研究常用近似的适用域。目标是让寿命模型说明“何时可以使用”，而不是永久固定一条衰减曲线。
可用容量需绑定截止电压、温度和倍率等测试协议；从容量轨迹误差推导退役时间误差，还需明确阈值穿越条件。相关结果将直接服务寿命预测、寿命感知策略和经济核算。
3.4 研究问题三：归约误差怎样影响运维结论？
拟研究详细模型与有效模型在相同允许动作或声明的闭环条件下，电压、反应裕量及累计副反应量等输出的误差关系。误差边界用于调整动作准入、预测区间及模型选取，并显式处理时间范围、数值求解和切换条件。
**预期研究成果：**可复用的形式定义与证明、条件化归约或误差结果、候选与反例集合。新的理论贡献以文献对照和实际证明为依据，不预先宣称发现新自然规律。
四、带条件与证据的可执行模型包
理论与软件的连接点，是能够被计算服务调用的模型包。它不仅包含预测方程，还包含方程适用的化学对象、观测条件、误差说明和验证依据。运行系统据此决定：使用简化模型、保留更多内部状态、追加诊断，还是采用备用策略。
4.1 模型包的组成
| 组成 | 记录内容 | 对运维的作用 |
|---|---|---|
| 化学与状态定义 | 化学体系、反应集、位点、状态单位及可用观测 | 防止混用电芯参数，构造一致的状态估计。 |
| 有效模型与映射 | 动力学、观测关系、归约与重建规则 | 支持快速预测，并保留模型切换所需的初始状态信息。 |
| 适用条件 | 参数域、温度、驱动方式、电位参考与时间范围 | 判断当前工况能否使用相应结论。 |
| 误差说明 | 目标量误差、数值误差和明确的概率条件 | 确定有适用范围的预测区间和约束余量。 |
| 证据与监测 | 证明工件、数值证书、统计验收、有效性检查 | 区分已证明、统计支持、经验支持及未知，条件变化时撤回旧证据。 |
| 替代与追溯 | 替代模型、备用策略、代码与数据标识、运行编号 | 在证据不足时有序切换，支持复核与问题定位。 |
4.2 一个模型证据进入决策的例子
设详细模型的约束为 ，有效模型输出为 。若在明确适用域内建立 ，则有：
这一标准逻辑关系说明了理论进入决策的方式。研究重点是从化学归约得到可用的误差 ，并把状态估计、数值求解及时间范围正确纳入条件。模型内证据也不自动覆盖模型与真实电芯之间的偏差。
当条件依赖不可直接观测的状态时，需要对可信状态集合进行判断；仅检查后验均值不足以代表整个集合适用。从低维切换到高维模型时，也保留隐藏状态重建的不确定性。
4.3 AI 如何生产可用的模型知识
AI 拟参与候选状态与公式搜索、条件修订、反例定位和证明尝试。高保真查询按预期运维价值、证据增益及计算成本分配，而不只追求更小的平均预测误差。危险反例在模拟环境中探索，真实装置上的诊断另行评估。
模型更新需经过独立检查后才进入运行服务。形式化表达与执行代码建立一致性测试；只有覆盖转换、数值算法和实现关系的部分，才声称具有相应范围的端到端保证。语言模型的解释必须引用实际记录。
五、安全、寿命与收益的联合决策
项目的经济目标是：在硬保护边界、可接受风险要求和模型适用条件内，提高全生命周期净收益。安全边界不因收益增加而放宽；经济偏好仅用于比较已经满足准入要求的候选策略。
同一风险验收水平下比较收益，同一收益目标下比较风险；不以短期盈利掩盖长期退化。
5.1 多时间尺度策略优化
慢时间尺度拟采用约束贝叶斯优化与多保真评估，选择分 SOC 段倍率、截止电压、放电深度、热管理及时序等策略参数；快时间尺度采用滚动优化提出动作，再检查模型条件、风险与裕量。
贝叶斯优化、电池模型预测控制及形式验证已有相关研究。[5–6] 本项目重点在于把化学归约证据、有效域和误差传递加入同一决策流程，并检验这些连接是否改善可靠性、计算效率或可用收益。
5.2 运行边界的主动学习与模型失配处理
离线主动学习优先检查高价值但证据不足的动作区域，以及可能导致错误放行的边界区域。反馈不仅更新参数，也可触发增加化学状态、修改近似条件或切换模型。
在线监测将区分越限风险、观测残差异常和证据失效。信息不足时允许扩大区间、收缩运行域或使用已检查其适用条件的备用策略；增加数据不被视为模型必然更准的保证。
5.3 一套完整的生命周期经济账
| 收益或成本 | 核算方式 |
|---|---|
| 购售电与能量转换 | 按同一电价情景和实际能量流计算，统一初始及终端状态。 |
| 热管理与执行 | 计入预热、冷却等耗电及对应执行条件。 |
| 退化、维护与更换 | 体现可用容量、剩余寿命、维护和更换影响；避免重复扣除同一损失。 |
| 残值与提前退出 | 统一处理终端容量、剩余寿命、提前退役与残值。 |
| 需求响应与辅助服务 | 保留情景配置；仅在适用规则、资格和数据明确时计入相应收入。 |
在线退化价格可用于近似未来损失，最终验收则按统一现金流与残值口径核算。合成电价、长周期外推及尚未确认的服务收入将明确标注，不作为既有商业业绩。
5.4 风险—收益前沿
系统拟输出不同允许风险要求下的可用策略集合与前沿，并同时给出事件定义、测试范围和统计依据。规则策略、固定裕度及鲁棒方法也充分调参形成对照前沿，以公平比较不同方法的安全与经济表现。
六、仿真与验证设计
项目以计算机模拟为主要实验环境，结合公开真实钠电数据进行可观测量校验。形式理论、数值仿真和真实数据各自回答不同问题，分别报告证据范围，不用其中一类替代其余两类。
6.1 三类相互补充的验证资源
| 资源 | 作用 | 使用边界 |
|---|---|---|
| 形式理论测试模型族 | 检验一般命题、归约条件、反例和证明工件 | 不直接等同于某一款真实电芯。 |
| 快速模型与独立参考仿真 | 运行完整闭环，评估内部状态、退化和模型失配 | 参考与控制模型保持独立，并单独评估现实适用性。 |
| 公开真实钠电数据 | 校验电压、容量、阻抗及数据实际包含的老化现象 | 故障验证限于数据实际提供的标签与观测。 |
电化学、热与副反应模块将分别检查和标定。不同正负极体系的数据与参数分开管理；仿真工具按具体模型和实现逐项核查其能力。数据与代码将记录来源、许可、字段和校验标识。
6.2 三组共同验收的实验
**理论与 AI 发现实验。**评价形式定义的完整性、已知结论恢复、必要条件反例、模型族泛化及证据成本；比较人工构造、传统聚合、纯拟合、无反例反馈及带证明反馈的方法。
**完整应用实验。**比较充分调参的规则策略、名义及鲁棒／场景模型预测控制、概率建模与主动学习方法。统一可见观测、初末状态、任务、计算预算和经济口径。
**理论到应用的连接实验。**分别移除有效域判断、归约误差传递、必要状态增补和失配后的证据撤回，检验其实际作用。仅隐藏证明标签而不改变数值模型，不应产生性能差异；可信依据与性能增益分别评价。
6.3 核心指标
| 维度 | 拟报告的指标 |
|---|---|
| 状态与寿命 | 状态误差、区间覆盖、条件 RUL 误差、退化与退役时间偏差。 |
| 风险与预警 | 预定义事件的轨迹级风险及上界、提前量、误报和召回。 |
| 收益与生命周期 | 净收益分布、尾部损失、单位容量收益、维护与更换成本。 |
| 计算与理论连接 | 决策时延、高保真调用量、证据成本、错误准入及模型切换代价。 |
运营分布测试、极端压力测试和外部数据校验分别统计。策略冻结后采用独立完整轨迹验收，不把相关时间点当作独立样本；同时报告失败、无优势和数值异常，以实际结果说明改进及适用边界。
七、参赛作品形态与完整演示
拟交付真实计算服务驱动的 Web 工作台，并提供离线运行包、CSV／API 数据接口、报告导出和可复现实验回放。用户无需理解证明器，即可查看状态、寿命、风险、建议及收益；每条关键结论又能进一步追溯到模型与证据。
7.1 工作台页面
| 页面 | 主要能力 |
|---|---|
| 电芯／模组总览 | 设置化学体系、环境和经济情景，查看当前状态、告警与策略。 |
| 状态与健康 | 查看 SOC、SOH、容量、内阻及区间，检查历史残差和识别不足。 |
| 寿命实验室 | 比较未来策略下的 RUL、退化路径、退役情景及近似有效条件。 |
| 风险与预警 | 查看事件风险、运行边界、预警原因，以及模型或证据失效提醒。 |
| 策略与收益 | 生成充放电与热管理建议，查看完整成本、收益区间和风险—收益前沿。 |
| 仿真对照 | 在冻结场景中运行基线与候选方法，比较全部结果并查看失败案例。 |
| 理论与证据 | 查看反应模型、适用域、证明工件、反例和模型更新依据。 |
7.2 一次演示贯通全部功能
**配置与评估。**用户选择电芯或模组、工况与经济情景；系统读取观测，形成当前状态、未来寿命和风险预测。
**机会与判断。**在预先定义的测试场景中出现调度机会；系统计算候选策略，检查简化模型是否仍然适用，必要时增补状态、调整误差或切换模型。
**动作与反馈。**系统更新充放电建议和收益预测，在模拟环境中执行，显示新观测、预测偏差与策略调整。
**对照与追溯。**用户比较不同方法的收益和风险，打开策略证据卡，查看某条化学条件如何影响模型与建议。展示案例来自实际完成的实验，并同时提供失败或无优势情形。
7.3 三种运行模式，来源清晰
工作台拟提供快速交互仿真、长周期批量计算和固定实验回放。回放将明确标记；图表关联原始轨迹与生成脚本，实时计算与固定实验结果清楚区分。
策略证据卡记录电芯与模型标识、状态范围、候选动作、有效时域、事件定义、验证方式、失效条件和替代策略。解释性文字与对应计算结果关联，支持逐项复核。
八、实施里程碑与交付成果
工程与理论并行推进：完整功能逐步贯通，形式模型与证据同步进入实际计算服务。里程碑以可运行功能、可检查证据和独立实验为验收依据。
8.1 实施里程碑
| 里程碑 | 应用与工程成果 | 理论及连接成果 |
|---|---|---|
| 研究对象与接口确定 | 明确电芯体系、观测、风险事件、收益账和全部模块接口 | 确定形式对象、首批命题、参数与单位约定，完成已有工作对照。 |
| 端到端闭环贯通 | 状态、寿命、风险、策略、仿真、收益与报告实际运行 | 建立基础反应模型、收支证明和归约反例；至少一项已检查的化学性质进入模型服务。 |
| 完整联合系统 | 加入主动边界学习、失配管理、全周期与模组功能 | 完成非平凡归约或有效域研究；让条件与误差实际影响模型选取和动作。 |
| 联合验收与交付 | 冻结策略，完成强基线实验、工作台、部署／离线包和回放 | 交付可复用形式库、证明与反例，完成理论、应用及连接三组实验。 |
8.2 四类最终交付物
**运维作品包。**可运行工作台与后端、完整仿真闭环、数据导入、固定实验回放、状态与寿命服务、安全预警、策略与收益优化、证据卡及报告。
**化学形式化与 AI 研究包。**形式模型库、证明器环境与假设依赖、归约条件和误差结果、候选与反例、AI 搜索和验证流程，并说明已知结果与新增贡献的区别。
**可复现实验证据包。**模型、数据和代码标识，冻结划分、基线配置、随机种子、风险验收、经济账、连接消融以及失败记录。
**研究报告与论文材料。**沿“化学机制—有效模型—运行决策—生命周期结果”组织方法、证明与实验，报告适用范围与局限。
8.3 预期价值
对运维者，项目提供从状态到策略的一致判断和透明收益账；对研发者，提供能够检查、修订和复用的电化学模型与证据；对主办方及后续合作方，提供可以独立运行、回放和复核的作品与实验基础。
研究价值通过可复用的化学形式化成果体现，应用价值通过完整系统与公平实验体现，二者的连接通过模型实际调用和消融实验体现。三项成果共同接受验收。
九、适用边界与研究基础
9.1 适用范围与证据说明
**仿真与现实分开。**本提案以计算机模拟为主要验证环境，公开数据只支持其实际包含的观测范围。多年情景外推不等同于多年真实运行；仿真内部状态不称为实验真值。
**概率与故障分开。**电压或温度越限、析钠相关代理事件、容量退役与真实故障具有不同定义，分别报告。未标定的代理事件概率不作为起火概率或产品安全认证。
**证明与物理适用性分开。**形式证明保证指定假设下的命题成立，不单独证明假设适用于真实电芯。基础理论形式化、新候选命题和经检验的新理论成果分别登记；部分模型的证明不代表整个软件已经完成形式验证。
**预测建议与实时保护分开。**在仿真中闭环执行策略；接入真实设备时先采用建议与影子运行模式，保留 BMS 和硬件保护职责。备用策略同样需要明确适用范围。
**模型更新保留不确定性。**参数或机制改变后，旧证据可能失效；系统允许输出未知、撤回结论或收缩动作域。新数据与更窄后验本身不构成更安全或更准确的证明。
9.2 参考研究
以下文献分别提供化学形式化、模型归约和可信控制的研究基础；本项目成果将由实际证明与实验另行支持。
[1] Bobbin M, Sharlin S, Feyzishendi P, et al. Formalizing chemical physics using the Lean theorem prover. Digital Discovery, 2024, 3: 264–280. DOI: 10.1039/D3DD00077J.
[2] Rao R, Esposito M. Nonequilibrium Thermodynamics of Chemical Reaction Networks: Wisdom from Stochastic Thermodynamics. Physical Review X, 2016, 6: 041064. DOI: 10.1103/PhysRevX.6.041064.
[3] Cardelli L, Tribastone M, Tschaikowski M, Vandin A. Forward and Backward Bisimulations for Chemical Reaction Networks. CONCUR 2015, LIPIcs 42: 226–239. DOI: 10.4230/LIPIcs.CONCUR.2015.226.
[4] Wachtel A, Rao R, Esposito M. Thermodynamically Consistent Coarse Graining of Biocatalysts beyond Michaelis–Menten. arXiv:1709.06045.
[5] Hirt S, Höhl A, Pohlodek J, et al. Safe Learning-Based Optimization of Model Predictive Control: Application to Battery Fast-Charging. arXiv:2410.04982.
[6] Coppola R, Touloujian H, Ombrini P, Mazo M Jr. Reinforcement Learning for Robust Ageing-Aware Control of Li-ion Battery Systems with Data-Driven Formal Verification. arXiv:2509.04288.
让化学知识进入实际决策，让安全与经济性在同一套证据下接受检验。
登录后可以留言