From 689c34076d08e59b1382864f9efcd983c8665ae5 Mon Sep 17 00:00:00 2001 From: ericmarin Date: Mon, 23 Mar 2026 17:53:21 +0100 Subject: added FashionMNIST xd --- verify_fashion_mnist.py | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 verify_fashion_mnist.py (limited to 'verify_fashion_mnist.py') diff --git a/verify_fashion_mnist.py b/verify_fashion_mnist.py new file mode 100644 index 0000000..48c8bc1 --- /dev/null +++ b/verify_fashion_mnist.py @@ -0,0 +1,32 @@ +import z3 +import nneq + +def check_property(onnx_a, onnx_b, vnnlib): + solver = nneq.Solver() + + print(f"--- Checking {vnnlib} ---") + + solver.load_onnx(onnx_a) + solver.load_onnx(onnx_b) + solver.load_vnnlib(vnnlib) + + result = solver.check() + + if result == z3.unsat: + print("VERIFIED (UNSAT): The networks are equivalent under this property.") + elif result == z3.sat: + print("FAILED (SAT): The networks are NOT equivalent.") + print("Counter-example input:") + print(solver.model()) + # m = solver.model() + # sorted_symbols = sorted([s for s in m.decls() if s.name().startswith("X_")], key=lambda s: s.name()) + # for s in sorted_symbols: + # print(f" {s.name()} = {m[s]}") + else: + print("UNKNOWN") + print("") + +if __name__ == "__main__": + check_property("./fashion_mnist/fashion_mnist_a.onnx", "./fashion_mnist/fashion_mnist_b.onnx", "./fashion_mnist/fashion_mnist_strict.vnnlib") + check_property("./fashion_mnist/fashion_mnist_a.onnx", "./fashion_mnist/fashion_mnist_b.onnx", "./fashion_mnist/fashion_mnist_epsilon.vnnlib") + check_property("./fashion_mnist/fashion_mnist_a.onnx", "./fashion_mnist/fashion_mnist_b.onnx", "./fashion_mnist/fashion_mnist_argmax.vnnlib") -- cgit v1.2.3