精读笔记
Problem Setting
论文标题：A constrained symbolic regression approach for Lyapunov function discovery（arXiv preprint / 2026）。
这篇论文不是在提出新的 Lyapunov 理论，而是在处理一个自动化 synthesis 问题：给定自治系统的状态轨迹，搜索一个符号形式的 Lyapunov 函数，并希望它最终能被验证为全域有效。任务本质上是“带函数不等式约束的符号函数搜索”，而不是普通回归。
真正困难点有两个。第一，Lyapunov 条件是定义域上的半无限约束，但数据只给出有限轨迹点；在训练点上下降并不意味着全域下降。第二，V 的函数形式未知，搜索变量本身是函数。SOS、LTI Lyapunov 方程这类方法之所以有效，是因为先验函数族强到可以把半无限约束转成代数条件；一旦离开多项式或二次型结构，问题立刻回到无限维和组合搜索。
这篇论文面对的关键矛盾是：研究者想要符号表达式，因为它可解释、可手工验证、可迁移到控制设计；但符号表达式空间离散且巨大，而稳定性约束又不是普通 supervised labels。论文的解法是把“找表达式”和“满足数据上的 Lyapunov 条件”统一写成 constrained symbolic regression，然后再用模型做全域验证。
Motivation
已有路线不够的地方比较明确。基函数/SOS 路线的问题是函数族先验太强：如果 Lyapunov 函数不在预设族里，优化再漂亮也没用。神经网络路线的问题相反：表达力足够，但函数是黑箱，训练通常通过 penalty 软约束实现，连训练点上的严格可行性都不一定保证，更别说全域 certificate。遗传编程式 symbolic regression 可以给解析式，但搜索随机，缺乏全局优化语义，也不自然处理硬约束。
作者的核心观察是：Lyapunov discovery 中没有 V(x) 的标签，所以它不是 classical symbolic regression；唯一有效 supervision 来自 V(x) >= 0 和 Vdot(x) <= 0 这类约束。于是应该把 symbolic regression 从“拟合标签”改造成“寻找满足物理/稳定性约束的表达式”。
关键缺口是 verification 与 search 的割裂。很多 learning-based 方法是先训练出候选 V，再额外做验证；如果候选失败，就进入反例循环或重新训练。本文想利用 MIP/MINLP 求解器在搜索过程中不断产生整数可行表达式这一事实，把验证提前嵌入 branch-and-bound。这个动机是合理的，也是真正区别于普通 symbolic Lyapunov generation 的地方。
Core Idea
核心思想可以概括为：用一个固定深度表达式树定义候选 Lyapunov 函数空间，把节点算子选择编码为整数变量，把每个数据点在每个节点的中间值编码为连续变量，然后通过约束保证表达式结构合法、求值正确、根节点满足数据上的 Lyapunov 条件。这样，原来不可直接优化的函数搜索被离散化为一个有限 superstructure 上的 MINLP。
直觉上它可能有效，是因为 Lyapunov 函数往往存在相对低复杂度的解析表达式，尤其在许多控制例子里是二次型、多项式型或简单组合型。表达式树给了一个比固定基函数更灵活、比神经网络更可解释的 inductive bias：它偏向短表达式、代数组合和可验证结构。这种 bias 在低维稳定系统上很强，甚至比通用函数逼近器更合适。
和 prior 的本质区别不是“也能表达很多函数”，而是把符号函数空间的组合搜索交给 mixed-integer global optimization，并把 Lyapunov constraints 作为硬约束而非 loss penalty。它不是靠 learned representation 泛化，而是靠约束优化筛掉不满足稳定性结构的表达式。scalability 并不天然更好；它更像是用强结构化搜索换取可解释性和中间验证机会。
Method
方法里真正重要的机制如下。
1. 表达式树超结构：固定树深和算子集合，把所有候选符号函数嵌入一个有限组合空间。它解决的是函数形式未知的问题，但代价是上限完全受树深和算子集合限制。所谓“no a priori assumptions about functional form”需要打折理解：没有指定多项式阶数或二次型，但强烈指定了表达式语法、深度、算子集合和常数范围。
2. arity/value constraints：arity constraints 保证表达式合法，value constraints 保证每个节点在每个数据点上的数值与所选算子一致。它们的作用不是提升理论表达力，而是把符号表达式变成优化变量可感知的可行域。big-M 约束是必要工程机制，但也会影响松弛质量和求解性能。
3. 数据点上的 Lyapunov constraints：根节点输出被约束为正，沿轨迹用 finite difference 近似下降。这里把 self-supervised signal 写成硬约束，是论文相对神经 penalty 方法的核心差异。但 finite difference Vdot 是明显折中：它避免符号求导或 derivative tree，却牺牲了与真实 Lie derivative 的一致性。
4. branch-and-bound-and-check：整数可行解一出现，就构造候选 V，并用已知动力学检查全域 min V 和 max Vdot。这个机制解决的是“等全局最优太慢且最优不一定有效”的问题。它带来的核心变化是 verification 从 post-hoc 变为 search-time computation。严格说，这不是新的全局优化理论，而是把 branch-and-check 思想用于 Lyapunov symbolic regression 的一个合适实例。
5. 目标函数设计：可最大化收敛率、惩罚常数大小、最小化表达式复杂度，或设为 feasibility。目标函数主要影响求解路径和返回表达式，不是 Lyapunov 有效性的根本来源。文中也显示目标选择会造成退化或找到不同但等价/近似的函数。
Key Insight / Why It Works
这篇论文真正有效的原因不是 symbolic regression 本身，而是三个因素叠加。
第一，表达式树给了强 inductive bias。对控制系统中的典型 Lyapunov 函数，低阶二次型或简单多项式往往足够；固定深度树加 {+, -, *} 已经能覆盖这些形式。因此在实验里能发现 x1^2 + c x2^2 并不意外。这里的成功很大程度来自 representation alignment：候选空间刚好包含简单真实证书，而且搜索偏向这种短表达式。
第二，硬约束比 penalty 更适合这个问题。Lyapunov discovery 的核心不是拟合精度，而是可行性。把正定性和下降条件作为 constraints，会比神经网络 loss 中的 violation penalty 更直接，至少在训练数据上可以强制排除明显错误候选。这是实质贡献之一。
第三，branch-and-bound-and-check 利用了符号表达式的离散可枚举性。一旦整数变量固定，候选函数是显式解析式，可以立即验证。这个性质在神经网络方法中不成立，因为中间训练 iterate 未必对应有意义的 certificate，验证也更复杂。因此 search-time verification 是本文最值得迁移的 insight。
但需要直接指出：实验中的增益很可能主要来自数据覆盖和简单函数族，而不是方法具备强泛化能力。采样率、时间长度、初始条件数量改变后，返回函数从无效变有效，说明核心瓶颈是 trajectory coverage 与 finite-difference 质量。所谓 self-supervised symbolic discovery 在这里更像“用足够多轨迹点约束一个低复杂度表达式空间”。
哪些部分可能只是 engineering？big-M 建模、Gurobi branching priority、常数惩罚、复杂度约束这些更多是求解工程。真正的思想是 constrained expression-tree search + online verification。finite-difference Vdot 是为了 tractability 的工程选择，不是理论亮点，甚至是主要误差源。
Relation To Prior Work
这篇工作处在三个谱系的交叉处：computational Lyapunov synthesis、mixed-integer symbolic regression、learning-based Lyapunov verification。
相对 SOS，它放弃了多项式/SOS 结构带来的凸性和强证书，换取更开放的表达式语法。这个差异是实质性的，但代价也很大：SOS 的 semi-infinite 约束可通过代数 certificate 处理，而本文仍需 post/search-time global verification。
相对神经 Lyapunov 方法，它的优势是解析表达式和硬约束建模；劣势是表达能力受树深限制且组合爆炸。神经方法的问题是 verification 难，本文把 verification 变得更自然，但没有让 verification 本身消失。
相对遗传编程或 transformer/RL 生成符号 Lyapunov，本文的关键不同是优化语义：它不是局部/随机生成表达式，而是在给定 superstructure 内做系统性 mixed-integer search。这个“全局最优”也要谨慎理解：只是对有限树深、给定算子、给定数据约束和目标函数的全局最优，不是 Lyapunov discovery 问题本身的全局最优。
相对已有 MINLP symbolic regression，新的部分不是表达式树建模本身，相关约束基本沿用该领域已有思想；实质新增在于把 Lyapunov 条件作为 self-supervised constraints，并把 verification 嵌入 B&B 过程。这是已有工具在 Lyapunov discovery 场景下的有效重组，而非全新优化范式。
Dataset / Evaluation
评估覆盖范围偏窄。主要实验是二维自治系统，发现的 Lyapunov 函数基本是简单二次型或近似二次型。论文考察了采样率、时间长度、初始条件数量、目标函数和复杂度约束，这些 ablation 对理解方法很有价值：它们清楚说明数据覆盖和时间离散误差会直接决定是否找到有效函数。
但这些实验并不足以支撑“原则上可用于任意连续动力系统”的强 claim。没有高维系统，没有复杂非多项式 Lyapunov 函数，没有噪声实验，没有真实过程控制数据，也没有与 SOS、神经 Lyapunov、CEGIS neural 方法或 transformer/RL symbolic 方法做系统比较。评估更像 proof-of-concept，而不是性能基准。
benchmark 是否验证核心 claim？它验证了“在简单低维例子中，MINLP 表达式树可以找出符号 Lyapunov，并且数据覆盖影响很大”。它没有验证 scalability，也没有验证相比已有方法的效率优势。branch-and-bound-and-check 的收益也没有被严格隔离：文中展示了可在整数可行解时验证，但缺少与 post-hoc verification 或 counterexample-guided loop 的直接计算对比。
另一个 evaluation limitation 是全域验证子问题的细节不足。论文说检查 min V 和 max Vdot，但这些本身可能是非凸全局优化问题；如果验证只是网格/数值绘图或局部优化，那么 certificate 强度会下降。文中未充分说明这一点。
Limitation
最核心限制是方法成立依赖强前提。
1. 已知模型。虽然称为 data-driven discovery，但全域 certification 依赖 f(x) 已知。若模型未知，方法只能生成候选，不能给证书。这把问题从“学习 Lyapunov”转移到“有模型时用数据辅助搜索”。
2. 数据覆盖。训练约束只在轨迹点上施加，且 Vdot 用 finite difference 近似。实验已经说明短时间、低采样、少初始条件会返回无效函数。核心能力可能主要来自数据覆盖，而不是模型自动推理出稳定结构。
3. 表达式空间上限。树深、算子集合、常数范围决定了能否表示真实 Lyapunov 函数。所谓 generality 是有条件的：如果需要 max/min、分段结构、radial basis、非光滑项、复杂组合或高阶项，树深会迅速膨胀。
4. Scalability。变量和约束随数据点、树节点、状态维度增长；binary 数随树和算子增长，continuous value variables 随数据线性增长。更糟的是乘法/除法导致非凸 MINLP。高维系统下组合爆炸几乎不可避免。文中提出 Benders/active learning，但没有实证。
5. Verification 本身未解决。全域检查 min V >= 0 和 max Vdot <= 0 是另一个非凸问题。论文把验证嵌入 B&B，但没有消除验证难度。对于复杂表达式，验证可能比搜索还难。
6. 目标退化。最小复杂度目标下常数不进入目标，导致参数退化，文中已观察到系数偏差。这说明 objective shaping 会强烈影响返回表达式，且“最简单”不等于“最可靠”。
7. 噪声和真实部署。方法默认无噪数据、单一平衡点、连续自治系统。含噪数据只能靠 slack，这会重新引入 penalty 权重选择问题。离真实实验数据或在线安全控制 deployment 还有明显距离。
Takeaway
- 1. 最值得记住的是：Lyapunov discovery 可以被重新表述为 constrained symbolic regression，而不是 supervised regression。
- 这个视角把稳定性条件从 loss 变成可行域，是比具体 MINLP 公式更重要的贡献。
- 2. 表达式树 + search-time verification 是可迁移 insight。
- 任何“候选对象离散可枚举、验证比训练目标更真实”的问题，都可以考虑在 B&B/枚举过程中嵌入 checker，而不是先求全局最优再验证。
一句话总结
这篇论文把 Lyapunov 函数发现推进为“约束化的符号表达式搜索 + 搜索中验证”的框架，实质贡献在于建模和验证流程重组，而不是新的稳定性理论或可扩展学习机制。