Page 32 - 《软件学报》2025年第8期
P. 32
刘宗鑫 等: 神经网络的增量验证 3455
10 4 3 10 4 3 10 4 3 10 4 3
10
10
10
DeepInc (s) 10 2 10 2 10 2 10 2
10
10 10 10 10
0 10 10 2 10 3 10 4 0 10 10 2 10 3 10 4 0 10 10 2 10 3 10 4 0 10 10 2 10 3 10 4
Marabou (s) Marabou (s) Marabou (s) Marabou (s)
(a) γ = 0.001时安全性质的 (b) γ = 0.01时安全性质的 (c) γ = 0.03时安全性质的 (d) γ = 0.05时安全性质的
验证时间对比 验证时间对比 验证时间对比 验证时间对比
10 3 10 3 10 3 10 3
DeepInc (s) 10 2 10 2 10 2 10 2
10
10
10
10
0 10 10 2 10 3 0 10 10 2 10 3 0 10 10 2 10 3 0 10 10 2 10 3
Marabou (s) Marabou (s) Marabou (s) Marabou (s)
(e) γ = 0.001时局部鲁棒性 (f) γ = 0.01时局部鲁棒性 (g) γ = 0.03时局部鲁棒性 (h) γ = 0.05时局部鲁棒性
性质的验证时间对比 性质的验证时间对比 性质的验证时间对比 性质的验证时间对比
图 7 DeepInc 与 Marabou 在所有权重都变化的 ACAS Xu 网络上验证安全性质和局部鲁棒性的
运行时间比较
10 4 10 4 10 4
DeepInc (s) 10 3 2 DeepInc (s) 10 3 2 DeepInc (s) 10 3 2
10
10
10
10 10 10
0 10 10 2 10 3 10 4 0 10 10 2 10 3 10 4 0 10 10 2 10 3 10 4
Marabou (s) Marabou (s) Marabou (s)
(a) γ = 0.01 (b) γ = 0.03 (c) γ = 0.05
变化权重占比 10% 30% 50%
图 8 DeepInc 与 Marabou 在部分权重变化的 ACAS Xu 网络上验证安全性质的运行时间比较
6 000 6 000 6 000 6 000
DeepInc (s) 4 000 4 000 4 000 4 000
2 000
2 000
2 000
2 000
0 2 000 4 000 6 000 0 2 000 4 000 6 000 0 2 000 4 000 6 000 0 2 000 4 000 6 000
Marabou (s) Marabou (s) Marabou (s) Marabou (s)
(a) γ = 0.001 (b) γ = 0.01 (c) γ = 0.03 (d) γ = 0.05
变化权重占比 10% 30% 50% 100%
图 9 DeepInc 与 Marabou 在部分权重变化的 MNIST 神经网络上验证局部鲁棒性性质的运行时间
