近年来，神经网络控制技术在机器人领域展现出令人惊艳的表现。这项基于深度学习的技术，曾驱动各种先进机器人完成了一系列复杂任务。
对于美国麻省理工学院博士生杨麓洁来说，这些先进机器人的名字，她早已能够脱口而出。
图 | 杨麓洁（来源：杨麓洁）
比如：
有既能泡咖啡、又会主动与人对话的 Figure 通用人形机器人；有会系鞋带、会晾衣服的 ALOHA 操作机器人；还有能越过各种地形执行侦查任务的机器狗等。
所有这些智能机器人的背后，都运行着精心设计的神经网络控制器。
尽管神经网络控制展现出卓越的实用性，但是目前仍然缺乏对于安全关键应用的稳定性保证。
而在控制理论领域，已有学者通过规范优化和形式化方法，为线性控制器或多项式控制器提供了严格的稳定性证明。
然而，要想让更加复杂的神经网络控制器拥有同样的稳定性保证，依然存在一些难题。
对于基于神经网络的控制器来说，开展严格的李雅普诺夫稳定性验证具有重要意义，主要原因如下：
其一，要确保系统的安全性和可靠性。
机器人、自动驾驶汽车、工业控制系统等都会涉及到复杂的动态过程，一旦控制系统失稳可能会导致严重的安全事故。
通过李雅普诺夫稳定性验证，可以形式化地证明系统在一定区域内的渐进稳定性，从而保证系统能够安全可靠地运行。
其二，扩大神经网络在关键领域的应用。
由于缺乏稳定性保证，目前的神经网络控制器在安全关键领域的应用依旧受到很大限制。
而一旦可以对其稳定性进行严格验证，神经网络就能大规模用于机器人、航空航天、生命科学等领域，从而发挥强大的控制性能。
其三，弥补神经网络的理论缺陷。
尽管神经网络在实践中表现卓越，但它本身缺乏坚实的理论基础。
通过与李雅普诺夫稳定性理论相结合，可以为神经网络控制器注入理论支撑，弥补其在可解释性和可靠性方面的不足。
其四，促进控制理论与机器学习的融合。
神经网络和李雅普诺夫理论分别代表着机器学习和控制理论两大领域的最新进展。
针对神经网络控制器进行李雅普诺夫验证，正是将这两个领域进行结合的有力尝试，必将推动两个领域的交叉融合，产生新的理论突破。
其五，应对复杂系统的挑战。
随着控制对象的日益复杂，单一的经典控制方法已经难以完全满足需求。
对于神经网络控制器来说，它具有学习复杂映射的能力。如果其稳定性也能得到保证，将为控制复杂非线性系统提供全新的解决方案。
基于此，杨麓洁和所在团队提出一种新型框架，该框架采用快速经验反证和正则化技术等方法，旨在同时学习神经网络控制器和李雅普诺夫稳定性证明，以便能够适用于复杂的非线性动态系统。
（来源：arXiv）
杨麓洁等人所提出的新公式化方法，不仅定义了现有研究中从未涉及的、更大的可稳定区域，而且改进了针对稳定导数的约束条件，让其只聚焦于可被证明的稳定区域范围。
通过这种新颖的方法，课题组突破了现有神经网络控制器在提供稳定性证明上的瓶颈，为更加复杂的神经网络控制系统提供了更大的可验证稳定区域。
对于李雅普诺夫稳定性条件的验证，该团队采用事后严格验证的方式，利用可扩展的、基于线性边界传播的神经网络验证技术，并运用分支定界算法、以及当前最先进的 α,β-CROWN 神经网络验证器，从而让验证方法兼具高效性和灵活性。
整个训练流程和验证流程，都可以在 GPU（graphics processing unit，图形处理器）上加速完成，无需依赖代价高昂的传统求解器。
通过这种新型验证方式，能够避免使用代价高昂的传统求解器，确保了李雅普诺夫稳定性条件的严格验证。
同时，还能兼顾计算效率和灵活性，让针对神经网络控制器的稳定性验证，变得更加高效和更加可行。
通过此，课题组为复杂非线性系统的稳定控制，提供了新的解决方案，在工业、交通、航空航天等领域都具备潜在应用前景。
其一，可用于机器人控制系统。
即本次方法能用于机器人的运动控制。特别是对于具有复杂非线性动力学的机器人系统来说，利用本次所提出的神经网络控制器和李雅普诺夫证明，能够保证机器人运动的稳定性和收敛性。
其二，可用于自动驾驶和无人机的控制。
自动驾驶汽车和无人机等系统，往往具有非线性和高维度的动力学方程。
而通过本次方法可以设计具有稳定性保证的神经网络控制器，提高自动驾驶和无人机的安全性和可靠性。
其三，可用于航天器和航空器的控制。
航天器和航空器通常具有复杂的非线性动力学模型，而本次方法可以为其提供稳定性保证的神经网络控制解决方案。
其四，可用于工业过程的控制。
许多化工、冶金等工业过程，都涉及到复杂的非线性动态系统。本次方法可用于设计具有稳定性保证的神经网络控制器，优化生产过程的控制性能。
其五，可用于生物医学系统建模与控制。
对于一些生物医学系统比如基因调控网络来说，可以使用非线性动力学模型来描述它。因此，本次方法有望用于这些系统的建模和控制。
（来源：arXiv）
另据悉，在相关论文截稿的前两周，该团队重新审视了论文中的数学公式。
在这次讨论之中，他们不仅针对公式加以深度优化，还发现了领域内已有研究中存在的错误和遗漏。
尽管本次研究的初步实验结果已经远远超越目前该领域的最先进成果。但是，上述发现也让他们决定采取一个大胆的举措：推翻所有已有的实验数据，基于优化后的公式全面设计实验。
“这是一个充满挑战的决定，因为重新进行实验意味着巨大的风险和额外的工作量，但我们坚持确保研究成果的严谨性与准确性。”杨麓洁表示。
经过连续奋战，他们终于在论文截稿前 4 小时，完成了所有实验和论文最后修改，确保了本次成果的高质量和创新性。
最终，相关论文以《用于状态和输出反馈的 Lyapunov 稳定神经控制：一种用于高效合成和验证的新形式》（Lyapunov-stable Neural Control for State and Output Feedback：A Novel Formulation for Efficient Synthesis and Verification）为题发在国际机器学习大会（ICML，International Conference on Machine Learning）[1]。
杨麓洁和丰田研究院戴泓楷博士是共同一作。
图 | 相关论文（来源：arXiv）
下一步，课题组将开展以下几方面探索。
首先，提高模型的普适性与适应性。
即开发基于神经网络的方法，来估计或优化系统的可靠性，以及调试和优化价值函数和控制障碍函数等其他控制指标，从而提高处理复杂动态系统时的可扩展性和灵活性。
其次，将理论与实践加以进一步结合。
目前，课题组已经在无人机、以及一些标准控制基准上取得进展。
未来，可以将本次框架用于更多、更复杂的控制系统，比如用于工业机器人和自动驾驶汽车等，以验证和提高其在复杂实际场景下的稳定性和可靠性。
再次，将开展跨学科的合作。
鉴于所研究问题的复杂性和跨学科特质，他们计划与机器学习领域的专家合作，力争发展更好的解决方案。
如前所述，为了合成通用非线性动态系统的、具有李雅普诺夫稳定性的神经网络控制器的目标，课题组还利用了神经网络验证领域的最新的验证工具 α,β-CROWN（https://abcrown.org）。
α,β-CROWN 由杨麓洁的两位合作者——美国伊利诺伊大学张欢教授、以及美国加州大学博士生施舟行共同研发。
在大规模计算机视觉神经网络稳健性验证和神经网络控制器安全性验证上，α,β-CROWN 展现出出色的扩展能力。
它利用了验证问题的网络结构，通过在神经网络中传播线性边界从而加速运算。
同时，α,β-CROWN 的边界传播过程具有较好的“GPU 友好度”，支持大型网络的高效验证，并能借助分支定界技术来快速评估多个子问题。
因此，杨麓洁也希望能进一步利用 α,β-CROWN 的能力，来解决更多的神经网络控制系统验证问题。
参考资料：
1.https://arxiv.org/pdf/2404.07956
排版：朵克斯