⚡ electrical engineering

Bernstein-based polynomial approach to study the stability of switched systems and formal verification using HOL Light

本文提出了一种研究切换系统稳定性的初步方法，该方法通过利用伯恩斯坦插值将切换系统转化为多项式表达式以构建李雅普诺夫函数，随后使用 HOL Light 证明助手对其进行形式化验证。

原作者： Loïc Michel

发布于 2026-06-04

📖 1 分钟阅读☕ 轻松阅读

原作者： Loïc Michel

原始论文采用 CC BY 3.0 许可（http://creativecommons.org/licenses/by/3.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在驾驶一辆拥有两种不同引擎的汽车：一种是用于赛车的运动引擎（Sport Engine），另一种是用于节省燃油的节能引擎（Eco Engine）。所谓的“切换系统（switched system）”，就像是一辆会根据规则（例如“如果路面陡峭，使用运动模式；如果路面平坦，使用节能模式”）在两种引擎之间瞬间切换的汽车。

工程师们面临的核心问题是：无论切换引擎的频率有多高，这辆车是否都能保持在路面上行驶而不发生碰撞？

这篇论文提出了一种巧妙的新方法来回答这个问题，即使用一种被称为**伯恩斯坦插值法（Bernstein Interpolation）**的数学方法。以下是作者对该方法的拆解：

1. 问题所在：规则太多

通常，为了检查汽车是否安全，你必须分别查看运动引擎的规则和节能引擎的规则，然后试图弄清楚在来回切换时会发生什么。这就像是通过观察两个不同的天气预报模型，并试图猜测它们如何混合，来预测天气一样。这会让过程变得混乱且复杂。

2. 解决方案：将引擎融合为一个平滑的配方

作者提出了一个技巧：与其将“切换”视为一次突然的跳变，不如使用一种特殊的数学工具——伯恩斯坦多项式（Bernstein polynomials），将其描述为一个平滑、连续的曲线。

你可以把它想象成灯光的调光开关（dimmer switch），而不是普通的开关（on/off button）。

数学不再说“引擎 A 开启，引擎 B 关闭”，而是创建一个单一的、平滑的公式，将两种引擎融合在一起。
如果开关处于 30% 运动模式和 70% 节能模式的状态，该公式会创造出一个正好是 30% 运动性能和 70% 节能性能的“混合”引擎。
这把一个复杂的、跳跃的系统变成了一个单一的、平滑的多项式方程（一个高级的代数配方）。

3. 安全检查：“李雅普诺夫（Lyapunov）”测试

一旦汽车被描述为这样一个单一的平滑配方，作者就要证明它是安全的。在工程学中，有一个著名的安全测试叫做李雅普诺夫函数（Lyapunov function）。

比喻： 想象汽车是一个在碗里滚动的球。如果球总是向着碗底（中心）滚动，那么系统就是稳定的；如果球向边缘滚动并掉出碗外，那么系统就是不稳定的。
李雅普诺夫函数就像是一张数学地图，它能证明这个球必须向碗底滚动。

4. “HOL Light”计算机律师

这是论文中最独特的部分。通常，人类负责检查这些安全地图，而人类可能会犯错。

作者使用了一个名为 HOL Light 的计算机工具。
你可以把 HOL Light 想象成一位极其严苛的计算机律师。它不仅仅是在猜测，它会逐步阅读数学证明，并以 1 亿% 的确定性验证每一个逻辑步骤。
如果这位计算机律师说：“是的，这个李雅普诺夫函数证明了球会留在碗里”，那么你就确信该系统是稳定的。这里没有任何人为错误的余地。

这篇论文实际做了什么

作者并没有发明一种新的汽车或引擎。他们通过两个案例展示了这种方法：

稳定系统： 他们展示了一辆天生安全的汽车。他们的方法成功地融合了引擎，并且计算机律师确认了其安全性。
不稳定系统： 他们展示了一辆天生会发生碰撞的汽车。他们的方法融合了引擎，而计算机律师正确地识别出安全地图失效了（球会滚出碗外）。

核心结论

这篇论文是一项“初步研究”，意味着它是一个概念验证。作者是在说：
“我们找到了一种方法，利用伯恩斯坦多项式，将一个复杂的跳跃系统转化为一个单一的平滑数学公式。然后，我们使用一位计算机律师（HOL Light）来正式证明这个公式代表的是一个安全系统还是一个危险系统。”

其目标是使检查这些切换系统是否安全的过程，变得更加可靠，并更易于使用计算机进行验证。

技术摘要：基于 Bernstein 多项式的切换系统稳定性与形式化验证方法

问题陈述
由多个受切换信号控制的子系统组成的切换系统，在稳定性分析方面提出了显著挑战。传统方法往往难以对系统的完整行为提供统一的数学描述，特别是当切换信号较为复杂（例如状态相关或时间相关）时。虽然存在多种分析此类系统的方法，但目前需要一种能够将离散切换逻辑转化为连续多项式表达式的表述方式，从而促进 Lyapunov 函数的构建并实现严谨的形式化验证。

方法论
本文提出了一种利用 Bernstein 插值 对切换系统进行重构的策略。其核心方法包括以下步骤：

多项式重构： 使用 Bernstein 多项式对决定子系统 $f_i$ 激活状态的切换信号 $\sigma$ 进行近似。通过将切换信号表示为 Bernstein 基函数的线性组合，原本由分段微分方程定义的整个切换系统被转化为一个统一的多项式表达式。
- 系统最初被描述为子系统的凸组合： $\dot{x} = \sum f_i(x)\sigma_i$ ，其中 $\sum \sigma_i = 1$ 且 $\sigma_i \geq 0$ 。
- 切换信号 $\sigma_i$ 被替换为其 Bernstein 级数近似 $B_{i,m}^\sigma(\sigma(\nu), \nu)$ ，从而得到一个由单个多项式微分方程描述的“B-切换系统”（B-switched system）。
处理切换类型： 该方法可以容纳不同的切换行为：
- 状态相关切换： 使用符号函数（例如 $\sigma \equiv \text{sign}(\delta x_1 x_2)$ ）进行建模，并通过特定阶数 $m$ 的 Bernstein 多项式进行近似。
- 时间相关切换： 使用脉冲函数来表示周期性激活。
- 灵活性： 可以通过调整 Bernstein 多项式的阶数 $m$ 来精细化近似，或者应用组合规则以提高精度，尽管这会增加所得表达式的复杂度。
形式化验证： 一旦系统被表示为多项式，作者建议使用 HOL Light 证明助手 来形式化验证其稳定性属性。
- 为该多项式系统确定一个候选 Lyapunov 函数 $V(x)$ 。
- 验证任务被简化为在定义域 $D$ 内证明不等式 $\dot{V}(x) < \epsilon$ （其中 $\epsilon$ 是一个微小的正数）。
- 这是通过使用带有 Taylor 近似的区间算术实现的，该方法此前已在 Flyspeck 项目中得到验证。这使得能够严谨地证明 Lyapunov 导数在指定边界内是负的（或足够接近于零）。

关键结果
作者通过两个源自现有文献的数值示例来展示所提方法，并将“B-切换”多项式表示与“标准”切换系统进行了对比：

示例 1（稳定系统）： 分析了一个包含两个稳定子系统的线性切换系统。Bernstein 近似成功模拟了标准系统的稳定行为。
示例 2（不稳定系统）： 分析了一个包含不稳定子系统的线性切换系统。该方法正确捕捉到了发散行为，并指出随着状态乘积 $x_1 x_2$ 增长超出区间 $[0, 1]$ ，Bernstein 级数会自然发散，反映了系统的这种不稳定性。
形式化验证： 使用了一个基础的线性稳定系统来演示 HOL Light 的验证过程。作者成功生成了一个形式化证明证书，确认了二次 Lyapunov 函数的导数在区间 $[0, 1]$ 内保持在阈值（ $\epsilon = 0.01$ ）之下。

意义与主张
作者将这项工作视为一项初步研究，并提出了以下具体贡献与局限性：

统一性： 主要贡献在于能够通过 Bernstein 插值将多个切换子系统“统一”为一个单一的多项式表达式。这简化了寻找 Lyapunov 候选函数的过程。
形式化认证： 该方法弥合了数值模拟与形式化证明之间的鸿沟，允许 HOL Light 助手验证所推导出的 Lyapunov 函数的稳定性属性。
规模有限： 本文明确指出，其假设 B-切换系统的稳定性属性与标准切换系统是等价的（至少在 Lyapunov 稳定性方面），但尚未声称已对其等价性进行了严谨的数学证明。
未来工作： 作者确定了几个有待进一步研究的方向，包括：
- 证明标准表示与 B-切换表示在稳定性方面的完全数学等价性。
- 将该方法扩展到非线性及非多项式系统。
- 利用平方和（SOS）工具来计算“最优”Lyapunov 函数，而非仅仅验证已识别的候选函数。

总之，本文提出了一种创新的框架，利用 Bernstein 多项式将切换系统的分析转化为多项式问题，从而可以通过形式化验证工具进行求解，为严谨的稳定性认证提供了一条潜在路径。