phanerozoic
/

tiny-XOR-verified

@@ -1,121 +1,121 @@
----
-license: mit
-tags:
-- formal-verification
-- coq
-- threshold-logic
-- neuromorphic
-- multi-layer
----
-# tiny-XOR-verified
-Formally verified XOR gate. Two-layer threshold network computing exclusive or with 100% accuracy.
-## Architecture
-| Component | Value |
-|-----------|-------|
-| Inputs | 2 |
-| Outputs | 1 |
-| Neurons | 3 (2 hidden, 1 output) |
-| Layers | 2 |
-| Parameters | 9 |
-| **Layer 1, Neuron 1 (OR)** | |
-| Weights | [1, 1] |
-| Bias | -1 |
-| **Layer 1, Neuron 2 (NAND)** | |
-| Weights | [-1, -1] |
-| Bias | 1 |
-| **Layer 2 (AND)** | |
-| Weights | [1, 1] |
-| Bias | -2 |
-| Activation | Heaviside step (all layers) |
-## Key Properties
-- 100% accuracy (4/4 inputs correct)
-- Coq-proven correctness
-- Minimal 2-layer architecture (XOR is not linearly separable)
-- Integer weights
-- Commutative: XOR(x,y) = XOR(y,x)
-- Associative: XOR(x,XOR(y,z)) = XOR(XOR(x,y),z)
-- Self-inverse: XOR(x,XOR(x,y)) = y
-## Why 2 Layers?
-XOR is the classic example of a function that is **not linearly separable** - a single threshold neuron cannot compute it. This network uses the minimal architecture:
-**Layer 1**: Compute OR and NAND in parallel
-**Layer 2**: Compute AND of results
-This implements: XOR(x,y) = AND(OR(x,y), NAND(x,y))
-## Usage
-```python
-import torch
-from safetensors.torch import load_file
-weights = load_file('xor.safetensors')
-def xor_gate(x, y):
-    inputs = torch.tensor([float(x), float(y)])
-    # Layer 1: OR and NAND
-    or_sum = (inputs * weights['layer1.neuron1.weight']).sum() + weights['layer1.neuron1.bias']
-    or_out = int(or_sum >= 0)
-    nand_sum = (inputs * weights['layer1.neuron2.weight']).sum() + weights['layer1.neuron2.bias']
-    nand_out = int(nand_sum >= 0)
-    # Layer 2: AND
-    layer1_outs = torch.tensor([float(or_out), float(nand_out)])
-    and_sum = (layer1_outs * weights['layer2.weight']).sum() + weights['layer2.bias']
-    return int(and_sum >= 0)
-# Test
-print(xor_gate(0, 0))  # 0
-print(xor_gate(0, 1))  # 1
-print(xor_gate(1, 0))  # 1
-print(xor_gate(1, 1))  # 0
-```
-## Verification
-**Coq Theorem**:
-```coq
-Theorem xor_correct : forall x y, xor_circuit x y = xorb x y.
-```
-Proven axiom-free with properties:
-- Commutativity
-- Associativity
-- Identity (XOR with false)
-- Complement (XOR with true gives NOT)
-- Nilpotence (XOR with itself gives false)
-- Involution (XOR is self-inverse)
-Full proof: [coq-circuits/Boolean/XOR.v](https://github.com/CharlesCNorton/coq-circuits)
-## Circuit Operation
-| Input (x,y) | OR | NAND | AND(OR,NAND) | XOR |
-|-------------|-----|------|--------------|-----|
-| (0,0) | 0 | 1 | 0 | 0 |
-| (0,1) | 1 | 1 | 1 | 1 |
-| (1,0) | 1 | 1 | 1 | 1 |
-| (1,1) | 1 | 0 | 0 | 0 |
-XOR outputs true when inputs differ.
-## Citation
-```bibtex
-@software{tiny_xor_prover_2025,
-  title={tiny-XOR-verified: Formally Verified XOR Gate},
-  author={Norton, Charles},
-  url={https://huggingface.co/phanerozoic/tiny-XOR-verified},
-  year={2025}
-}
-```

+---
+license: mit
+tags:
+- formal-verification
+- coq
+- threshold-logic
+- neuromorphic
+- multi-layer
+---
+# tiny-XOR-verified
+Formally verified XOR gate. Two-layer threshold network computing exclusive or with 100% accuracy.
+## Architecture
+| Component | Value |
+|-----------|-------|
+| Inputs | 2 |
+| Outputs | 1 |
+| Neurons | 3 (2 hidden, 1 output) |
+| Layers | 2 |
+| Parameters | 9 |
+| **Layer 1, Neuron 1 (OR)** | |
+| Weights | [1, 1] |
+| Bias | -1 |
+| **Layer 1, Neuron 2 (NAND)** | |
+| Weights | [-1, -1] |
+| Bias | 1 |
+| **Layer 2 (AND)** | |
+| Weights | [1, 1] |
+| Bias | -2 |
+| Activation | Heaviside step (all layers) |
+## Key Properties
+- 100% accuracy (4/4 inputs correct)
+- Coq-proven correctness
+- Minimal 2-layer architecture (XOR is not linearly separable)
+- Integer weights
+- Commutative: XOR(x,y) = XOR(y,x)
+- Associative: XOR(x,XOR(y,z)) = XOR(XOR(x,y),z)
+- Self-inverse: XOR(x,XOR(x,y)) = y
+## Why 2 Layers?
+XOR is the classic example of a function that is **not linearly separable** - a single threshold neuron cannot compute it. This network uses the minimal architecture:
+**Layer 1**: Compute OR and NAND in parallel
+**Layer 2**: Compute AND of results
+This implements: XOR(x,y) = AND(OR(x,y), NAND(x,y))
+## Usage
+```python
+import torch
+from safetensors.torch import load_file
+weights = load_file('xor.safetensors')
+def xor_gate(x, y):
+    inputs = torch.tensor([float(x), float(y)])
+    # Layer 1: OR and NAND
+    or_sum = (inputs * weights['layer1.neuron1.weight']).sum() + weights['layer1.neuron1.bias']
+    or_out = int(or_sum >= 0)
+    nand_sum = (inputs * weights['layer1.neuron2.weight']).sum() + weights['layer1.neuron2.bias']
+    nand_out = int(nand_sum >= 0)
+    # Layer 2: AND
+    layer1_outs = torch.tensor([float(or_out), float(nand_out)])
+    and_sum = (layer1_outs * weights['layer2.weight']).sum() + weights['layer2.bias']
+    return int(and_sum >= 0)
+# Test
+print(xor_gate(0, 0))  # 0
+print(xor_gate(0, 1))  # 1
+print(xor_gate(1, 0))  # 1
+print(xor_gate(1, 1))  # 0
+```
+## Verification
+**Coq Theorem**:
+```coq
+Theorem xor_correct : forall x y, xor_circuit x y = xorb x y.
+```
+Proven axiom-free with properties:
+- Commutativity
+- Associativity
+- Identity (XOR with false)
+- Complement (XOR with true gives NOT)
+- Nilpotence (XOR with itself gives false)
+- Involution (XOR is self-inverse)
+Full proof: [coq-circuits/Boolean/XOR.v](https://github.com/CharlesCNorton/coq-circuits/blob/main/coq/Boolean/XOR.v)
+## Circuit Operation
+| Input (x,y) | OR | NAND | AND(OR,NAND) | XOR |
+|-------------|-----|------|--------------|-----|
+| (0,0) | 0 | 1 | 0 | 0 |
+| (0,1) | 1 | 1 | 1 | 1 |
+| (1,0) | 1 | 1 | 1 | 1 |
+| (1,1) | 1 | 0 | 0 | 0 |
+XOR outputs true when inputs differ.
+## Citation
+```bibtex
+@software{tiny_xor_prover_2025,
+  title={tiny-XOR-verified: Formally Verified XOR Gate},
+  author={Norton, Charles},
+  url={https://huggingface.co/phanerozoic/tiny-XOR-verified},
+  year={2025}
+}
+```