diff options
Diffstat (limited to 'xor')
| -rw-r--r-- | xor/xor.py | 40 | ||||
| -rw-r--r-- | xor/xor_a.onnx | bin | 0 -> 4857 bytes | |||
| -rw-r--r-- | xor/xor_a.onnx.data | 0 | ||||
| -rw-r--r-- | xor/xor_argmax.vnnlib | 11 | ||||
| -rw-r--r-- | xor/xor_b.onnx | bin | 0 -> 4987 bytes | |||
| -rw-r--r-- | xor/xor_b.onnx.data | 0 | ||||
| -rw-r--r-- | xor/xor_epsilon.vnnlib | 12 | ||||
| -rw-r--r-- | xor/xor_strict.vnnlib | 11 |
8 files changed, 74 insertions, 0 deletions
diff --git a/xor/xor.py b/xor/xor.py new file mode 100644 index 0000000..ebc5477 --- /dev/null +++ b/xor/xor.py @@ -0,0 +1,40 @@ +import torch +import torch.nn as nn +import torch.onnx + +class xor_mlp(nn.Module): + def __init__(self, hidden_dim): + super().__init__() + self.layers = nn.Sequential( + nn.Linear(2, hidden_dim), + nn.ReLU(), + nn.Linear(hidden_dim, 1) + ) + def forward(self, x): + return self.layers(x) + +def train_model(name: str, dim): + X = torch.tensor([[0,0], [0,1], [1,0], [1,1]], dtype=torch.float32) + Y = torch.tensor([[0], [1], [1], [0]], dtype=torch.float32) + + net = xor_mlp(hidden_dim=dim) + loss_fn = nn.MSELoss() + optimizer = torch.optim.Adam(net.parameters(), lr=0.1) + + print(f"Training {name}...") + for epoch in range(1000): + optimizer.zero_grad() + out = net(X) + loss = loss_fn(out, Y) + 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", 8).eval() + torch_net_b = train_model("Network B", 16).eval() + + torch.onnx.export(torch_net_a, (torch.randn(1, 2),), "xor_a.onnx") + torch.onnx.export(torch_net_b, (torch.randn(1, 2),), "xor_b.onnx") diff --git a/xor/xor_a.onnx b/xor/xor_a.onnx Binary files differnew file mode 100644 index 0000000..9c13609 --- /dev/null +++ b/xor/xor_a.onnx diff --git a/xor/xor_a.onnx.data b/xor/xor_a.onnx.data new file mode 100644 index 0000000..e69de29 --- /dev/null +++ b/xor/xor_a.onnx.data diff --git a/xor/xor_argmax.vnnlib b/xor/xor_argmax.vnnlib new file mode 100644 index 0000000..3043d70 --- /dev/null +++ b/xor/xor_argmax.vnnlib @@ -0,0 +1,11 @@ +(declare-const X_0 Real) +(declare-const X_1 Real) +(declare-const Y_0 Real) +(declare-const Y_1 Real) + +; Discrete inputs: X must be 0 or 1 +(assert (or (= X_0 0) (= X_0 1))) +(assert (or (= X_1 0) (= X_1 1))) + +; Violation of argmax equivalence (threshold 0.5) +(assert (not (= (> Y_0 0.5) (> Y_1 0.5)))) diff --git a/xor/xor_b.onnx b/xor/xor_b.onnx Binary files differnew file mode 100644 index 0000000..fb18840 --- /dev/null +++ b/xor/xor_b.onnx diff --git a/xor/xor_b.onnx.data b/xor/xor_b.onnx.data new file mode 100644 index 0000000..e69de29 --- /dev/null +++ b/xor/xor_b.onnx.data diff --git a/xor/xor_epsilon.vnnlib b/xor/xor_epsilon.vnnlib new file mode 100644 index 0000000..d4e9bb7 --- /dev/null +++ b/xor/xor_epsilon.vnnlib @@ -0,0 +1,12 @@ +(declare-const X_0 Real) +(declare-const X_1 Real) +(declare-const Y_0 Real) +(declare-const Y_1 Real) + +; Discrete inputs: X must be 0 or 1 +(assert (or (= X_0 0) (= X_0 1))) +(assert (or (= X_1 0) (= X_1 1))) + +; Violation of epsilon equivalence (epsilon = 0.1) +(define-fun absolute ((x Real)) Real (if (>= x 0) x (- x))) +(assert (> (absolute (- Y_0 Y_1)) 0.1)) diff --git a/xor/xor_strict.vnnlib b/xor/xor_strict.vnnlib new file mode 100644 index 0000000..fcf364e --- /dev/null +++ b/xor/xor_strict.vnnlib @@ -0,0 +1,11 @@ +(declare-const X_0 Real) +(declare-const X_1 Real) +(declare-const Y_0 Real) +(declare-const Y_1 Real) + +; Discrete inputs: X must be 0 or 1 +(assert (or (= X_0 0) (= X_0 1))) +(assert (or (= X_1 0) (= X_1 1))) + +; Violation of strict equivalence: outputs are different +(assert (not (= Y_0 Y_1))) |