使用Rocq证明器对倾斜估计的形式化验证

中文摘要 AI 辅助

人形机器人的安全运行关键依赖于对其垂直方向（即“倾斜”）的准确估计。这需要多种数学工具，包括三维几何和微分方程。为了形式化验证倾斜估计，我们在Rocq证明器中开发了一个用于稳定性分析的库。我们首先形式化常微分方程的理论。我们提供了（局部）Cauchy-Lipschitz（又称Picard-Lindelof）定理的存在性和唯一性的形式化，利用了Mathematical Components库对商的支持。我们将此形式化扩展为全局存在性和对初始条件的连续依赖的变体。在这些基础上，我们发展了Lyapunov稳定性的理论，该理论与现有的LaSalle不变性原理的形式化兼容。我们还扩展了一个现有的机器人操纵器静力学库以支持动态系统。最后，我们将这些库应用于为一个人形机器人开发的最先进的倾斜估计的验证。

英文摘要

The safe operation of a humanoid robot critically relies on accurate estimation of its vertical orientation, or ``tilt''. This requires a variety of mathematical tools, including three-dimensional geometry and differential equations. To formally verify tilt estimation, we develop a library for stability analysis in the Rocq prover. We start by formalizing a theory of ordinary differential equations. We provide a formalization of the (local) Cauchy-Lipschitz (a.k.a. Picard-Lindelof) theorem for existence and uniqueness, taking advantage of the library support for quotients provided by the Mathematical Components library. We extend this formalization with a variant for global existence and continuous dependence on initial conditions. Building on these foundations, we develop a theory of Lyapunov stability that is compatible with an existing formalization of LaSalle's invariance principle. We also extend an existing library for the statics of robot manipulators to support dynamical systems. Finally, we apply these libraries to the verification of a state-of-the-art tilt estimation developed for a humanoid robot.

发表机构

• National Institute of Advanced Industrial Science and Technology (AIST)（先进产业科学技术研究所）
• Université Paris Cité（巴黎西岱大学）
• Nagoya University/National Institute of Advanced Industrial Science and Technology (AIST)（名古屋大学/先进产业科学技术研究所）
• Kyoto University（京都大学）

机构由 AI 辅助整理，请以论文原文为准。