refactored examples

4 files changed, 175 insertions, 0 deletions

diff --git a/examples/iris/iris.py b/examples/iris/iris.py
new file mode 100644
index 0000000..db631c0
--- /dev/null
+++ b/examples/iris/iris.py
@@ -0,0 +1,63 @@
+import torch
+import torch.nn as nn
+from sklearn.datasets import load_iris
+from sklearn.preprocessing import StandardScaler
+from torch.utils.data import DataLoader, TensorDataset
+
+class Iris_MLP(nn.Module):
+    def __init__(self, hidden_dim):
+        super().__init__()
+        self.layers = nn.Sequential(
+            nn.Linear(4, hidden_dim),
+            nn.ReLU(),
+            nn.Linear(hidden_dim, 3),
+        )
+    def forward(self, x):
+        return self.layers(x)
+
+iris = load_iris()
+scaler = StandardScaler()
+X = scaler.fit_transform(iris.data).astype('float32') # pyright: ignore
+y = iris.target.astype('int64') # pyright: ignore
+
+dataset = TensorDataset(torch.from_numpy(X), torch.from_numpy(y))
+trainloader = DataLoader(dataset, batch_size=16, shuffle=True)
+
+def train_model(name: str, dim):
+    net = Iris_MLP(hidden_dim=dim)
+    loss_fn = nn.CrossEntropyLoss()
+    optimizer = torch.optim.Adam(net.parameters(), lr=1e-2)
+
+    print(f"Training {name} ({dim} neurons)...")
+    for epoch in range(200):
+        global loss
+        for data in trainloader:
+            inputs, targets = data
+            optimizer.zero_grad()
+            outputs = net(inputs)
+            loss = loss_fn(outputs, targets)
+            loss.backward()
+            optimizer.step()
+        if (epoch + 1) % 100 == 0:
+            print(f"  Epoch {epoch+1}, Loss: {loss.item():.4f}")
+    return net
+
+if __name__ == "__main__":
+    torch_net_a = train_model("Network A", 10).eval()
+    torch_net_b = Iris_MLP(hidden_dim=20).eval()
+
+    with torch.no_grad():
+        torch_net_b.layers[0].weight[:10].copy_(torch_net_a.layers[0].weight) # pyright: ignore
+        torch_net_b.layers[0].bias[:10].copy_(torch_net_a.layers[0].bias) # pyright: ignore
+        torch_net_b.layers[0].weight[10:].copy_(torch_net_a.layers[0].weight) # pyright: ignore
+        torch_net_b.layers[0].bias[10:].copy_(torch_net_a.layers[0].bias) # pyright: ignore
+
+        half_weights = torch_net_a.layers[2].weight / 2.0 # pyright: ignore
+        
+        torch_net_b.layers[2].weight[:, :10].copy_(half_weights) # pyright: ignore
+        torch_net_b.layers[2].weight[:, 10:].copy_(half_weights) # pyright: ignore
+        
+        torch_net_b.layers[2].bias.copy_(torch_net_a.layers[2].bias) # pyright: ignore
+
+    torch.onnx.export(torch_net_a, (torch.randn(1, 4),), "iris_a.onnx")
+    torch.onnx.export(torch_net_b, (torch.randn(1, 4),), "iris_b.onnx")
diff --git a/examples/iris/iris_argmax.vnnlib b/examples/iris/iris_argmax.vnnlib
new file mode 100644
index 0000000..ec72109
--- /dev/null
+++ b/examples/iris/iris_argmax.vnnlib
@@ -0,0 +1,51 @@
+; Argmax Equivalence for Iris
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const X_2 Real)
+(declare-const X_3 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+(declare-const Y_4 Real)
+(declare-const Y_5 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+(assert (>= X_2 0.0))
+(assert (<= X_2 1.0))
+(assert (>= X_3 0.0))
+(assert (<= X_3 1.0))
+
+; Violation of argmax equivalence
+(assert (or
+  (and 
+    (> Y_0 Y_1)
+    (> Y_0 Y_2)
+    (or
+      (> Y_4 Y_3)
+      (> Y_5 Y_3)
+    )
+  )
+  (and 
+    (> Y_1 Y_0)
+    (> Y_1 Y_2)
+    (or
+      (> Y_3 Y_4)
+      (> Y_5 Y_4)
+    )
+  )
+  (and 
+    (> Y_2 Y_0)
+    (> Y_2 Y_1)
+    (or
+      (> Y_3 Y_5)
+      (> Y_4 Y_5)
+    )
+  )
+))
diff --git a/examples/iris/iris_epsilon.vnnlib b/examples/iris/iris_epsilon.vnnlib
new file mode 100644
index 0000000..9c8e825
--- /dev/null
+++ b/examples/iris/iris_epsilon.vnnlib
@@ -0,0 +1,31 @@
+; Strict Equivalence for Iris
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const X_2 Real)
+(declare-const X_3 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+(declare-const Y_4 Real)
+(declare-const Y_5 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+(assert (>= X_2 0.0))
+(assert (<= X_2 1.0))
+(assert (>= X_3 0.0))
+(assert (<= X_3 1.0))
+
+; Violation of epsilon equivalence (epsilon = 0.1)
+(define-fun absolute ((x Real)) Real (if (>= x 0) x (- x)))
+(assert (or
+	(> (absolute (- Y_0 Y_3)) 0.1)
+	(> (absolute (- Y_1 Y_4)) 0.1)
+	(> (absolute (- Y_2 Y_5)) 0.1)
+))
diff --git a/examples/iris/iris_strict.vnnlib b/examples/iris/iris_strict.vnnlib
new file mode 100644
index 0000000..78d01fe
--- /dev/null
+++ b/examples/iris/iris_strict.vnnlib
@@ -0,0 +1,30 @@
+; Strict Equivalence for Iris
+
+; Constant declaration
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const X_2 Real)
+(declare-const X_3 Real)
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+(declare-const Y_4 Real)
+(declare-const Y_5 Real)
+
+; Bounded inputs: X must be within [0, 1]
+(assert (>= X_0 0.0))
+(assert (<= X_0 1.0))
+(assert (>= X_1 0.0))
+(assert (<= X_1 1.0))
+(assert (>= X_2 0.0))
+(assert (<= X_2 1.0))
+(assert (>= X_3 0.0))
+(assert (<= X_3 1.0))
+
+; Violation of strict equivalence
+(assert (or
+	(not (= Y_0 Y_3))
+	(not (= Y_1 Y_4))
+	(not (= Y_2 Y_5))
+))