Formal Verification（形式化验证）

形式化验证通过构建系统的数学模型，使用逻辑推理穷举所有可能状态，以证明其满足规范。在AI领域，它用于验证神经网络鲁棒性、公平性和安全性，例如证明在输入扰动下输出不变。方法包括模型检测、定理证明和抽象解释。挑战在于状态空间爆炸和可扩展性。近年来，可满足性模理论（SMT）和混合整数规划被用于神经网络验证，工具如Marabou和Reluplex。该技术对安全关键系统至关重要。