ISOIEC 24029-22023 人工智能（AI）-神经网络鲁棒性的评估-第2部分形式方法的使用方法标准立项发展报告

人工智能（AI）——神经网络鲁棒性的评估——第2部分：形式方法的使用方法标准立项发展报告StandardizationDevelopmentReport:ArtificialIntelligence(AI)—AssessmentoftheRobustnessofNeuralNetworks—Part2:MethodologyfortheUseofFormalMethods摘要随着人工智能技术在航空航天、自动驾驶、医疗诊断、工业控制等安全攸关领域的深度应用，神经网络系统的鲁棒性问题日益凸显，已成为制约AI技术规模化落地的关键瓶颈之一。形式方法以其数学上的严格性和完备性，为神经网络鲁棒性评估提供了区别于传统统计测试的确定性验证途径。在此背景下，国际标准化组织（ISO）与国际电工委员会（IEC）联合发布了ISO/IEC24029-2:2023《人工智能（AI）——神经网络鲁棒性的评估——第2部分：形式方法的使用方法》。本报告对该标准的立项背景、编制历程、核心技术内容、应用场景及未来发展方向进行系统阐述。报告指出，该标准填补了神经网络鲁棒性形式化验证领域国际标准的空白，首次系统性地规范了形式方法应用于神经网络鲁棒性评估的总体流程、方法选择准则、前置条件判定及应用约束，为安全攸关领域AI系统的认证与部署提供了权威技术依据。标准的发布对于推动人工智能治理体系建设、促进可信AI产业发展具有重要的里程碑意义。关键词：人工智能；神经网络；鲁棒性评估；形式方法；国际标准；安全攸关系统；可信AIKeywords:ArtificialIntelligence;NeuralNetworks;RobustnessAssessment;FormalMethods;InternationalStandards;Safety-CriticalSystems;TrustworthyAI一、引言1.1研究背景近年来，以深度神经网络为代表的人工智能技术取得了突破性进展，在图像识别、自然语言处理、自主决策等众多任务中展现出接近甚至超越人类专家的性能水平。然而，大量研究表明，神经网络模型普遍存在对抗样本脆弱性问题——即在原始输入上施加人眼难以察觉的微小扰动，即可导致模型产生完全错误的输出。这一缺陷对AI系统的安全性构成了严重威胁，尤其在自动驾驶、民航飞行控制、医疗辅助诊断、核设施监控等安全攸关场景中，可能引发灾难性后果。传统的神经网络性能评估方法主要依赖于测试集上的统计指标计算，如准确率、精确率、召回率等。然而，这类基于采样的评估方法只能保证模型在"已测试"输入上的表现，无法为所有可能的输入提供确定性的性能保证。正如著名的"测试只能证明bug的存在，而不能证明bug的不存在"这一软件工程定律所揭示的，统计测试方法对于安全攸关系统的认证而言存在根本性的局限性。形式方法（FormalMethods）是以数理逻辑为基础的数学化验证技术，通过对系统行为进行严格的数学建模和推理，能够提供具有完备性保证的验证结果。将形式方法应用于神经网络鲁棒性评估，可以在数学上证明"对于一个给定的输入范围，网络输出的变化始终被约束在规定的安全界限之内"，从而为AI系统的安全认证提供坚实的数学基础。1.2标准制定背景尽管形式方法在神经网络验证领域已经积累了丰富的研究成果，但长期以来缺乏统一的国际标准来规范其应用方法和流程。不同研究机构和企业采用各自的技术路线和评价准则，导致验证结果难以横向比较，也使得监管机构和认证部门缺乏可依据的统一技术规范。在此背景下，ISO/IECJTC1（联合技术委员会）下属的SC42（人工智能分技术委员会）启动了ISO/IEC24029系列标准的编制工作。ISO/IEC24029系列标准聚焦于神经网络鲁棒性评估，其中第1部分（ISO/IEC24029-1）概述了鲁棒性评估的总体框架和通用要求，而第2部分（ISO/IEC24029-2）则专门针对形式方法的应用提供方法论指导。2023年8月，ISO/IEC24029-2:2023经国际标准化组织正式发布，标志着神经网络形式化验证领域首项国际标准正式生效。二、标准编制历程与参与单位2.1编制历程ISO/IEC24029-2:2023的编制工作遵循ISO/IEC国际标准制定的标准流程，经历了以下主要阶段：-提案阶段（NWIProposal）：由法国国家标准化机构（AFNOR）提出新工作项目提案，经SC42各成员国投票表决后正式立项；-编制阶段（WorkingDraft,WD）：成立特别工作组（AdHocGroup），汇集各成员国专家起草工作草案；-委员会草案阶段（CommitteeDraft,CD）：草案在SC42内部进行多轮审议和修改；-国际标准草案阶段（DraftInternationalStandard,DIS）：草案分发至各成员国进行为期五个月的投票和意见征集；-最终国际标准草案阶段（FinalDraftInternationalStandard,FDIS）：根据DIS阶段反馈进行最终修订；-正式发布阶段（Publication）：2023年8月1日，经各成员国最终投票通过后正式发布。整个编制过程历时约三年，期间经历了多轮技术讨论和意见协调，反映了国际社会在神经网络形式化验证方法论上的广泛共识。2.2主要参与单位介绍法国国家信息与自动化研究所（INRIA）作为该标准编制的核心技术支撑单位之一，法国国家信息与自动化研究所（InstitutNationaldeRechercheenInformatiqueetenAutomatique,INRIA）在标准的制定过程中发挥了关键性作用。INRIA是法国国家级的信息科学与自动化研究机构，成立于1967年，隶属于法国高等教育、研究与创新部，在形式化验证、程序分析、嵌入式系统安全等领域拥有超过五十年的深厚积累。INRIA旗下多个研究团队长期从事神经网络形式化验证的基础理论研究，在抽象解释（AbstractInterpretation）、可达性分析（ReachabilityAnalysis）、可满足性模理论（SatisfiabilityModuloTheory,SMT）求解等核心技术方向上处于国际领先水平。INRIA的研究人员率先提出了基于抽象解释理论的神经网络鲁棒性验证框架，该框架通过将神经网络的连续状态空间抽象为有限个几何区域，实现了对网络行为的近似精确分析，同时控制了计算复杂度。这一原创性方法论为ISO/IEC24029-2的技术框架构建提供了重要的理论基础。在标准编制过程中，INRIA的专家团队牵头起草了标准中"形式方法的分类与选择"及"形式方法应用的前置条件分析"等核心技术章节，并组织了多轮国际间的实验比对研究（Round-RobinTesting），验证了标准中所述方法在不同类型神经网络架构上的适用性和效果。INRIA的深度参与确保了该标准不仅在理论层面具有严谨的数学基础，而且在实际工程应用中具有良好的可操作性。除INRIA外，德国联邦材料研究与测试研究所（BAM）、日本产业技术综合研究所（AIST）以及多家国际知名企业和学术机构也参与了标准的起草工作，共同推动了这一国际标准的最终发布。三、标准主要内容概述3.1标准定位与适用范围ISO/IEC24029-2:2023是ISO/IEC24029系列标准的第2部分，聚焦于形式方法在神经网络鲁棒性评估中的应用。该标准适用于以下范围的神经网络系统：-采用深度神经网络（DeepNeuralNetwork,DNN）、卷积神经网络（ConvolutionalNeuralNetwork,CNN）、循环神经网络（RecurrentNeuralNetwork,RNN）等主流架构的AI系统；-应用于安全攸关领域、需要提供可靠性保证的AI系统；-需要在部署前或运行过程中进行形式化验证的AI系统；-需要接受监管审查或安全认证的AI系统。标准不限定具体的神经网络框架或硬件平台，具有较好的技术中立性和普适性。3.2核心技术内容3.2.1形式方法的总体应用流程标准规定了对神经网络鲁棒性进行形式化评估的系统性流程，主要包括以下关键步骤：-鲁棒性属性定义：明确需要验证的鲁棒性属性，如局部鲁棒性（在某一输入点周围的安全半径内，网络输出保持稳定）、全局鲁棒性（在整个输入空间中，网络输出的变化满足给定的界限）或特定语义属性（如对某种特定扰动的抵抗能力）；-神经网络模型形式化建模：将训练完成的神经网络模型（包括网络结构、激活函数、权重参数、偏置等）转化为形式方法工具可处理的数学表示，如线性不等式系统、多面体约束或逻辑表达式；-输入空间约束设定：定义输入扰动的可行域，明确对抗扰动的范数约束（如L∞范数、L2范数）和语义约束（如亮度变化范围、几何变换范围等）；-验证属性形式化表达：将鲁棒性需求转化为形式化的验证目标，通常表达为可达性判定问题或优化问题的数学形式；-验证引擎执行：调用选定的形式验证工具（如基于SMT求解器、抽象解释引擎或混合整数线性规划求解器等）执行验证过程；-结果分析与反馈：对验证输出进行系统解释，对于验证失败的情形，分析反例（Counterexample）产生的根源，并反馈至模型修正或再训练环节。3.2.2形式方法的分类与选择标准系统性地对适用于神经网络鲁棒性评估的形式方法进行了分类，主要包括以下类别，并针对每类方法给出了适用场景和应用建议：-完备验证方法（CompleteVerificationMethods）：包括基于可满足性模理论（SMT）的编码方法、混合整数线性规划（MILP）方法、确定性完备搜索算法等。这类方法能够在数学上给出"是/否"的确定性判定结果，但其计算复杂度通常较高，适用于网络规模较小或鲁棒性属性结构相对简单的场景；-不完备验证方法（IncompleteVerificationMethods）：包括基于抽象解释的方法、区间传播分析方法、基于凸松弛的线性近似方法等。这类方法通过牺牲一定的完备性换取更高的计算效率，能够处理更大规模的网络，但在某些情况下可能产生"不确定"的验证结果；-对抗样本生成方法（AdversarialExampleGenerationMethods）：包括基于梯度优化的快速梯度符号法（FGSM）、投影梯度下降（PGD）、基于优化的C&W方法等。这类方法虽然不能提供完备性保证，但能够有效发现有价值的反例，为鲁棒性改进提供线索。标准特别指出，上述各类方法之间存在互补关系。在实际应用中，应当根据验证目标、可用计算资源、所需保证强度等因素，综合考虑选择单一方法或组合使用多种方法。这一分类框架不仅考虑了验证能力的技术维度，还兼顾了计算效率与可扩展性的工程维度，体现了标准在理论完备性与工程可实施性之间的精心平衡。3.2.3形式方法应用的前置条件与约束标准对形式方法在实际应用中所需满足的前置条件和使用约束做出了明确规定，主要包括：-网络结构的约束：某些形式验证方法要求神经网络的激活函数为特定的分段线性形式（如ReLU），对于使用Sigmoid、Tanh等非线性激活函数的网络，需要进行适当的近似处理或采用专门针对非线性激活的验证方法；-数值精度要求：由于浮点数运算存在舍入误差，形式验证过程中需要对数值精度进行控制。标准建议在验证过程中使用高精度运算或多精度混合运算策略，以确保验证结果的可靠性；-输入空间的有界性假设：大多数形式验证方法要求输入空间为一个紧致集合（有界闭集），因此需要将实际应用中的输入范围进行合理界定；-计算资源的约束：标准要求验证工作的实施方应根据网络规模、验证属性和可用计算资源进行可行性和成本预评估，必要时可采用模型简化、抽象精化（Counterexample-GuidedAbstractionRefinement,CEGAR）等策略在保证率与计算效率之间寻求平衡；-与相关标准的协调兼容：标准要求形式方法的应用应与ISO/IEC24029-1中规定的鲁棒性评估总体框架保持一致，并参照ISO/IEC22989（人工智能概念与术语）及ISO/IEC23053（机器学习框架）中的相关定义和要求。四、标准的意义与应用价值4.1填补国际标准空白ISO/IEC24029-2:2023是全球首项专门针对神经网络鲁棒性形式化验证方法进行系统规范的国际标准。在以往的国际标准化体系中，形式方法主要应用于传统软件和硬件系统的验证领域，如航空电子系统中的DO-178C标准及铁路信号系统中的EN50128标准。虽然这些标准中提到了形式方法的应用可能性，但并未涉及神经网络这一新型计算范式。本标准的发布，首次将形式方法的应用范畴正式拓展至神经网络验证领域，填补了该方向国际标准体系的空白。4.2促进AI安全认证体系建设随着欧盟《人工智能法案》（EUArtificialIntelligenceAct）等全球性AI监管法规的逐步落地，AI系统的安全认证（ConformityAssessment）成为亟需解决的关键问题。ISO/IEC24029-2:2023为监管部门和认证机构提供了可操作的技术依据。依据本标准，认证机构可以明确要求高风险AI系统的开发者在特定场景下使用形式方法对神经网络鲁棒性进行验证，并以标准化的格式提交验证结果，实现不同系统间验证结果的横向比较和累积互认。4.3推动产业实践与技术进步对于AI系统的开发者和部署者而言，本标准的发布提供了明确的技术指引，有助于在AI研发流程中系统性地嵌入形式化验证环节，将鲁棒性保障从"事后修补"转变为"前置设计"。同时，标准的实施也将推动形式验证工具链的发展和完善，促进学术界与工业界在神经网络验证领域的深度合作，加速新方法、新工具从实验室走向实际工程应用。五、结论与展望ISO/IEC24029-2:2023的发布，是人工智能标准化进程中具有里程碑意义的重要事件。该标准通过系统性地规范形式方法在神经网络鲁棒性评估中的应用方法论，为安全攸关领域AI系统的研发、验证和认证提供了权威的技术框架，也为全球AI治理体系的建设贡献了实质性的技术支撑。展望未来，随着神经网络的规模不断扩大、应用场景持续深化，形式验证方法将面临可扩展性与验证效率的持续挑战。我们预期，未来的标准化工作将重点关注以下方向：一是面向更大规模深度网络的高效验证方法的标准化；二是涵盖学习过程本身的正式验证方法体系（形式化机器学习的验证）；三是与测试、运行时监控等其它保证手段的综合集成方法论；四是多模态AI系统、大语言模型等新型AI范式鲁棒性评估的标准化需求；五是面向行业应用的标准细化与延伸（如ISO26262道路车辆功能安全、ISO/SAE21434道路车辆网络安全等标准的衔接与协调）。同时，本标准在实际应用中的效果反馈和经验积累，也将为标准的后续修订和完善提供宝贵的实践依据。我们有理由相信，以ISO/IEC24029-2:2023为代表的人工智能鲁棒性评估系列标准，将持续推动人工智能向更加安全、可靠、可信的方向发展，为人工智能技术造福人类社会提供坚实的技术保障。参考文献[1]ISO/IEC24029-2:2023,Artificialintelligence(AI)—Assessmentoftherobustnessofneuralnetworks—Part2:Methodologyfortheuseofformalmethods[2]ISO/IEC24029-1,Artificialintelligence