软件所提出随机微分动态系统的精确矩估计方法

近日，中国科学院软件研究所天基综合信息系统全国重点实验室针对随机微分方程中矩估计难以获得闭式解这一难题，提出了一套基于符号推导与有限维线性常微分方程归约的通用计算框架，为随机动态系统的形式化分析与验证提供了新的理论工具和算法支撑。相关成果论文Exact Moment Estimation of Stochastic Differential Dynamics被形式化领域国际会议FM 2026收录，第一作者为冯胜华副研究员。

随机微分方程是描述连续时间随机动态系统的重要数学模型，分析其统计行为是系统设计、控制优化与安全验证的基础。矩是刻画随机系统统计特征的核心量。例如，一阶矩可反映系统状态的平均演化趋势，二阶矩和高阶矩则能够揭示系统波动、离散程度及稳定性等信息。在随机系统的形式化验证中，矩估计常被用于构造安全边界、评估系统可靠性以及支持风险分析。

然而，随机微分方程的精确矩估计长期以来缺乏系统性的求解方法。即便系统方程形式较为简单，其解通常也难以表示为显式的闭式表达；而对于非线性系统，计算状态变量的期望和高阶矩往往需要引入复杂的高维隐式积分，难以直接求解。

现有方法多依赖超鞅、半定规划或矩闭包近似等技术，能够求解矩的上界、下界或近似结果，但普遍存在结果保守、依赖模板选择、难以获得精确闭式表达等局限。因此，建立一套能够精确计算矩表达式的理论与算法工具，对于提升随机动态系统可验证建模、定量分析和安全性证明能力具有重要意义。

针对上述问题，论文聚焦于多项式随机微分方程，提出了“矩可解随机微分方程”的形式化概念，并设计了一种基于无穷小生成元的符号计算方法。该方法能将目标矩的演化过程自动归约为有限维线性常微分方程系统，从而实现矩的精确闭式计算。具体而言，研究首先形式化定义了矩可解性，用于刻画哪些随机微分系统的多项式矩能够获得显式表达，并利用Dynkin公式递归寻找其依赖的相关矩项。当这些矩项在有限集合中闭合时，即可自动生成线性常微分方程系统，进而精确计算目标矩。研究团队证明了“矩可解随机微分方程”的所有多项式矩均可通过有限维线性常微分方程精确计算。

“矩可解随机微分方程”概念图

研究团队在信息一致性网络、车辆编队系统等多个随机系统基准上进行了实验验证。结果表明，研究团队所提方法能够有效计算线性与非线性系统中的精确矩，并能够有力支撑概率安全性验证和系统行为分析等实际任务，展现出良好的适用性和实用性。

论文链接：

https://link.springer.com/chapter/10.1007/978-3-032-26220-2_4