基于Coq形式化概率库的高维概率编程语言验证框架

标题： 基于Coq形式化概率库的高维概率编程语言验证框架作者： 王宝军，夏挽岚，祖光照，周志农，高雪峰摘要： 概率编程语言（PPL）已成为机器学习和安全攸关系统中的核心建模工具，但其在高维场景下的形式化语义基础与验证手段仍不完善。针对现有PPL验证工具在维度支持、测度论严谨性和自动化程度三方面的局限，本文提出了一个基于 形证概率系统 v4.0 的高维PPL形式化验证框架。我们首先在Coq中系统化地构建了高维概率论的基础设施，包括多维Borel σ-代数、单调类定理及连续映射可测性等核心概念的形式化。基于此，我们设计了一个三层验证架构，支持对高维随机变量、分布及条件概率语义的严格验证。实验表明，该框架能有效验证高维高斯过程与PPO强化学习算法的可测性与语义一致性。所有形式化代码均已通过Coq 8.16+验证，并附有可公开验证的构建来源证明，为构建可靠的高维概率AI系统提供了可复现的理论与工具基础。关键词： 概率编程语言；形式化验证；Coq；高维概率论；Borel可测性；单调类定理；安全AI分类： cs.PL (编程语言), cs.LO (逻辑与验证), cs.AI (人工智能), math.PR (概率论)English DescriptionTitle: A High-Dimensional Probabilistic Programming Language Verification Framework Based on a Formalized Coq Probability LibraryAuthors: Baojun Wang, Wanlan Xia, Guangzhao Zu, Zhinong Zhou, Xuefeng GaoAbstract: Probabilistic Programming Languages (PPLs) have become central to modeling in machine learning and safety-critical systems, yet their formal semantic foundations and verification methods remain underdeveloped for high-dimensional settings. To address three key limitations of existing PPL verification tools—limited dimensional support, weak measure-theoretic rigor, and low automation—this paper presents a high-dimensional PPL verification framework based on FormalCert Probability System v4.0. We first systematically construct a high-dimensional probability theory infrastructure in Coq, formalizing core concepts such as multidimensional Borel σ-algebras, the monotone class theorem, and measurability of continuous mappings. Building on this foundation, we design a three-tier verification architecture that supports rigorous verification of high-dimensional random variables, distributions, and conditional probability semantics. Experiments demonstrate the framework's effectiveness in verifying the measurability and semantic consistency of high-dimensional Gaussian processes and PPO reinforcement learning algorithms. All formalized code has been verified with Coq 8.16+ and is accompanied by publicly verifiable build provenance attestations, providing a reproducible theoretical and practical foundation for building reliable high-dimensional probabilistic AI systems.Keywords: Probabilistic Programming Language; Formal Verification; Coq; High-Dimensional Probability Theory; Borel Measurability; Monotone Class Theorem; Safe AICategories: cs.PL (Programming Languages), cs.LO (Logic in Computer Science), cs.AI (Artificial Intelligence), math.PR (Probability)