Rename from tiny-mod5-verified

README.md

@@ -0,0 +1,107 @@
+---
+license: mit
+tags:
+- pytorch
+- safetensors
+- threshold-logic
+- neuromorphic
+- modular-arithmetic
+---
+
+# threshold-mod5
+
+Computes Hamming weight mod 5 for 8-bit inputs. Multi-layer network with thermometer encoding.
+
+## Circuit
+
+```
+  x₀ x₁ x₂ x₃ x₄ x₅ x₆ x₇
+   │  │  │  │  │  │  │  │
+   └──┴──┴──┴──┼──┴──┴──┴──┘
+               ▼
+       ┌─────────────┐
+       │ Thermometer │  Layer 1: 9 neurons
+       │  Encoding   │
+       └─────────────┘
+               │
+               ▼
+       ┌─────────────┐
+       │  MOD-5      │  Layer 2: 4 neurons
+       │  Detection  │  Pattern (1,1,1,1,-4)
+       └─────────────┘
+               │
+               ▼
+       ┌─────────────┐
+       │  Classify   │  Output: 5 classes
+       └─────────────┘
+               │
+               ▼
+        {0, 1, 2, 3, 4}
+```
+
+## Algebraic Insight
+
+Pattern `(1, 1, 1, 1, -4)` causes cumulative sums to cycle mod 5:
+
+```
+HW=0: sum=0 → 0 mod 5
+HW=1: sum=1 → 1 mod 5
+HW=2: sum=2 → 2 mod 5
+HW=3: sum=3 → 3 mod 5
+HW=4: sum=4 → 4 mod 5
+HW=5: sum=0 → 0 mod 5  (reset: 1+1+1+1-4=0)
+HW=6: sum=1 → 1 mod 5
+HW=7: sum=2 → 2 mod 5
+HW=8: sum=3 → 3 mod 5
+```
+
+## Architecture
+
+| Layer | Neurons | Function |
+|-------|---------|----------|
+| Input | 8 | Binary bits |
+| Hidden 1 | 9 | Thermometer encoding |
+| Hidden 2 | 4 | MOD-5 detection |
+| Output | 5 | One-hot classification |
+
+**Total: 18 neurons, 146 parameters**
+
+## Output Distribution
+
+| Class | HW values | Count/256 |
+|-------|-----------|-----------|
+| 0 | 0, 5 | 57 |
+| 1 | 1, 6 | 36 |
+| 2 | 2, 7 | 36 |
+| 3 | 3, 8 | 57 |
+| 4 | 4 | 70 |
+
+## Usage
+
+```python
+from safetensors.torch import load_file
+import torch
+
+w = load_file('model.safetensors')
+
+def forward(x):
+    x = x.float()
+    x = (x @ w['layer1.weight'].T + w['layer1.bias'] >= 0).float()
+    x = (x @ w['layer2.weight'].T + w['layer2.bias'] >= 0).float()
+    out = x @ w['output.weight'].T + w['output.bias']
+    return out.argmax(dim=-1)
+```
+
+## Files
+
+```
+threshold-mod5/
+├── model.safetensors
+├── model.py
+├── config.json
+└── README.md
+```
+
+## License
+
+MIT

config.json

@@ -0,0 +1,30 @@
+{
+  "model_type": "threshold_network",
+  "task": "mod5_classification",
+  "architecture": "8 -> 9 -> 4 -> 5",
+  "input_size": 8,
+  "hidden1_size": 9,
+  "hidden2_size": 4,
+  "output_size": 5,
+  "num_parameters": 146,
+  "num_neurons": 18,
+  "activation": "heaviside",
+  "weight_constraints": "integer",
+  "verification": {
+    "method": "coq_proof",
+    "exhaustive": true,
+    "constructive": true,
+    "algebraic": true,
+    "axiom_free": true
+  },
+  "accuracy": {
+    "all_inputs": "256/256",
+    "percentage": 100.0
+  },
+  "algebraic_insight": "Weights (1,1,1,1,-4) on thermometer encoding produce cumsum = HW mod 5",
+  "github": "https://github.com/CharlesCNorton/mod5-verified",
+  "related": {
+    "mod3_model": "https://huggingface.co/phanerozoic/tiny-mod3-prover",
+    "parity_model": "https://huggingface.co/phanerozoic/tiny-parity-prover"
+  }
+}

model.py

@@ -0,0 +1,119 @@
+"""
+Inference code for mod5-verified threshold network.
+
+This network computes MOD-5 (Hamming weight mod 5) on 8-bit binary inputs.
+"""
+
+import torch
+import torch.nn as nn
+from safetensors.torch import load_file
+
+
+def heaviside(x):
+    """Heaviside step function: 1 if x >= 0, else 0."""
+    return (x >= 0).float()
+
+
+class Mod5Network(nn.Module):
+    """
+    Verified threshold network for MOD-5 computation.
+
+    Architecture: 8 -> 9 -> 4 -> 5
+    - Layer 1: Thermometer encoding (9 neurons detect HW >= k)
+    - Layer 2: MOD-5 detection using (1,1,1,1,-4) weight pattern
+    - Output: 5-class classification
+    """
+
+    def __init__(self):
+        super().__init__()
+        self.layer1 = nn.Linear(8, 9)
+        self.layer2 = nn.Linear(9, 4)
+        self.output = nn.Linear(4, 5)
+
+    def forward(self, x):
+        """Forward pass with Heaviside activation."""
+        x = x.float()
+        x = heaviside(self.layer1(x))
+        x = heaviside(self.layer2(x))
+        x = self.output(x)
+        return x
+
+    def predict(self, x):
+        """Get predicted class (0, 1, 2, 3, or 4)."""
+        return self.forward(x).argmax(dim=-1)
+
+    @classmethod
+    def from_safetensors(cls, path):
+        """Load model from safetensors file."""
+        model = cls()
+        weights = load_file(path)
+
+        model.layer1.weight.data = weights['layer1.weight']
+        model.layer1.bias.data = weights['layer1.bias']
+        model.layer2.weight.data = weights['layer2.weight']
+        model.layer2.bias.data = weights['layer2.bias']
+        model.output.weight.data = weights['output.weight']
+        model.output.bias.data = weights['output.bias']
+
+        return model
+
+
+def mod5_reference(x):
+    """Reference implementation: Hamming weight mod 5."""
+    return (x.sum(dim=-1) % 5).long()
+
+
+def verify(model, verbose=True):
+    """Verify model on all 256 inputs."""
+    inputs = torch.zeros(256, 8)
+    for i in range(256):
+        for j in range(8):
+            inputs[i, j] = (i >> j) & 1
+
+    targets = mod5_reference(inputs)
+    predictions = model.predict(inputs)
+
+    correct = (predictions == targets).sum().item()
+
+    if verbose:
+        print(f"Verification: {correct}/256 ({100*correct/256:.1f}%)")
+
+        if correct < 256:
+            errors = (predictions != targets).nonzero(as_tuple=True)[0]
+            print(f"Errors at indices: {errors[:10].tolist()}")
+
+    return correct == 256
+
+
+def demo():
+    """Demonstration of MOD-5 computation."""
+    print("Loading mod5-verified model...")
+    model = Mod5Network.from_safetensors('model.safetensors')
+
+    print("\nVerifying on all 256 inputs...")
+    verify(model)
+
+    print("\nExample predictions:")
+    test_cases = [
+        [0, 0, 0, 0, 0, 0, 0, 0],
+        [1, 0, 0, 0, 0, 0, 0, 0],
+        [1, 1, 0, 0, 0, 0, 0, 0],
+        [1, 1, 1, 0, 0, 0, 0, 0],
+        [1, 1, 1, 1, 0, 0, 0, 0],
+        [1, 1, 1, 1, 1, 0, 0, 0],
+        [1, 1, 1, 1, 1, 1, 0, 0],
+        [1, 1, 1, 1, 1, 1, 1, 0],
+        [1, 1, 1, 1, 1, 1, 1, 1],
+    ]
+
+    for bits in test_cases:
+        x = torch.tensor([bits], dtype=torch.float32)
+        hw = sum(bits)
+        pred = model.predict(x).item()
+        expected = hw % 5
+        status = "OK" if pred == expected else "ERROR"
+        print(f"  {bits} -> HW={hw}, pred={pred}, expected={expected} [{status}]")
+
+
+if __name__ == '__main__':
+    demo()

model.safetensors

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:56840ae01951fd606bfc6aadb521629c1860752d8886efaad1ecd6bd2583707d
+size 1008