罗盘 / 神经网络形式化验证
暗星档案 · 未点亮的星神经网络形式化验证
本条为初评草案（AI 辅助编目）：T 阶为三问初评（撬动面 × 停滞度 × 临界性），双评过 σ 门并红蓝复核后才升"已建档"。查不到的字段留空不编。点亮者会进入亮星候选流程，其贡献与星阶按 HCF 独立重评，不从暗星自动继承。
神经网络形式化验证T5 量级 · 新星
给AI的行为提供数学级别的安全保证，而非事后测试
暗星编号DS-1084
轴R · 风险与文明安全
领域ai-computing
状态初评草案 · 待双评与红蓝复核
这是什么 · 为什么难
现有AI安全评估几乎全靠经验性测试，无法穷尽输入空间；形式化验证试图用可达性分析、抽象解释、证明证书等数学工具，为神经网络的输出范围提供可证明的边界保证。VNN-COMP国际神经网络验证竞赛已连续举办六届，PyRAT等工具已能对特定规模网络给出可靠性证明。攻破意味着关键场景（自动驾驶、医疗诊断、AI Agent自主行动）下的AI系统能像传统安全关键软件一样获得数学级别的行为保证，而不只是统计意义上"大概率没问题"。
卡在哪 · 机制级卡点
形式化验证方法在网络规模、非线性激活函数复杂度上有严重的可扩展性瓶颈，目前仅能验证相对小型的网络或非常局部的性质；大语言模型级别的验证在理论和算力上都远未可行。
谁在攻
VNN-COMP国际神经网络验证竞赛（SAIV国际AI验证研讨会主办）；CEA List（PyRAT工具研发团队，法国）
怎么参与
从形式化方法、可达性分析或AI安全理论方向进入相关学术团队或竞赛