File size: 5,457 Bytes
278368f |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 |
---
license: mit
tags:
- pytorch
- safetensors
- formal-verification
- coq
- mod5
- modular-arithmetic
- threshold-network
- neuromorphic
---
# tiny-mod5-prover
Formally verified neural network that computes the MOD-5 function (Hamming weight mod 5) on 8-bit inputs. This repository contains the model artifacts; for proof development and Coq source code, see [mod5-verified](https://github.com/CharlesCNorton/mod5-verified).
## Overview
This is a threshold network that computes `mod5(x) = HW(x) mod 5` for 8-bit binary inputs, where HW denotes Hamming weight (number of set bits). The network outputs 0, 1, 2, 3, or 4 corresponding to the five residue classes.
**Key properties:**
- 100% accuracy on all 256 possible inputs
- Correctness proven in Coq via constructive algebraic proof
- Weights constrained to integers
- Heaviside step activation (x >= 0 -> 1, else 0)
- Part of the verified MOD-m family: {MOD-2, MOD-3, MOD-5, ...}
## Architecture
| Layer | Neurons | Function |
|-------|---------|----------|
| Input | 8 | Binary input bits |
| Hidden 1 | 9 | Thermometer encoding (HW >= k) |
| Hidden 2 | 4 | MOD-5 detection |
| Output | 5 | Classification (one-hot) |
**Total: 18 neurons, 146 parameters**
## Quick Start
```python
import torch
from safetensors.torch import load_file
weights = load_file('model.safetensors')
def forward(x, weights):
x = x.float()
x = (x @ weights['layer1.weight'].T + weights['layer1.bias'] >= 0).float()
x = (x @ weights['layer2.weight'].T + weights['layer2.bias'] >= 0).float()
out = x @ weights['output.weight'].T + weights['output.bias']
return out.argmax(dim=-1)
inputs = torch.tensor([[1, 0, 1, 1, 1, 0, 0, 0]], dtype=torch.float32)
output = forward(inputs, weights)
print(f"MOD-5 of [1,0,1,1,1,0,0,0]: {output.item()}") # 4 (4 bits set, 4 mod 5 = 4)
```
## Weight Structure
| Tensor | Shape | Values | Description |
|--------|-------|--------|-------------|
| `layer1.weight` | [9, 8] | All 1s | Thermometer encoding |
| `layer1.bias` | [9] | [0, -1, ..., -8] | Threshold at HW >= k |
| `layer2.weight` | [4, 9] | [0,1,1,1,1,-4,1,1,1] | MOD-5 detection |
| `layer2.bias` | [4] | [-1, -2, -3, -4] | Class thresholds |
| `output.weight` | [5, 4] | Various | Classification |
| `output.bias` | [5] | [0, -1, -1, -1, -1] | Output thresholds |
## Algebraic Insight
The MOD-m construction uses weights `(1, 1, ..., 1, 1-m)` with `m-1` ones before the reset term.
For MOD-5, the pattern `(1, 1, 1, 1, -4)` produces cumulative sums that cycle through `(0, 1, 2, 3, 4, 0, 1, 2, 3, 4, ...)`:
```
HW=0: cumsum = 0 -> 0 mod 5
HW=1: cumsum = 1 -> 1 mod 5
HW=2: cumsum = 2 -> 2 mod 5
HW=3: cumsum = 3 -> 3 mod 5
HW=4: cumsum = 4 -> 4 mod 5
HW=5: cumsum = 0 -> 0 mod 5 (reset: 1+1+1+1-4=0)
HW=6: cumsum = 1 -> 1 mod 5
HW=7: cumsum = 2 -> 2 mod 5
HW=8: cumsum = 3 -> 3 mod 5
```
## Formal Verification
The network is proven correct in the Coq proof assistant with three independent proofs:
**1. Exhaustive verification:**
```coq
Theorem network_correct_exhaustive : verify_all = true.
Proof. vm_compute. reflexivity. Qed.
```
**2. Constructive verification (case analysis):**
```coq
Theorem network_correct_constructive : forall x0 x1 x2 x3 x4 x5 x6 x7,
predict [x0; x1; x2; x3; x4; x5; x6; x7] =
mod5 [x0; x1; x2; x3; x4; x5; x6; x7].
```
**3. Algebraic verification:**
```coq
Theorem cumsum_eq_mod5 : forall k,
(k <= 8)%nat -> cumsum k = Z.of_nat (Nat.modulo k 5).
Theorem network_algebraic_correct : forall h,
(h <= 8)%nat ->
classify ... = Nat.modulo h 5.
```
All proofs are axiom-free ("Closed under the global context").
## MOD-5 Distribution
For 8-bit inputs (256 total):
| Class | Count | Hamming Weights |
|-------|-------|-----------------|
| 0 | 57 | 0, 5 |
| 1 | 36 | 1, 6 |
| 2 | 36 | 2, 7 |
| 3 | 57 | 3, 8 |
| 4 | 70 | 4 |
## The MOD-m Family
| Model | Function | Neurons | Params | Weight Pattern |
|-------|----------|---------|--------|----------------|
| tiny-parity-prover | MOD-2 | 14 | 139 | (1, -1) |
| tiny-mod3-prover | MOD-3 | 14 | 110 | (1, 1, -2) |
| **tiny-mod5-prover** | MOD-5 | 18 | 146 | (1, 1, 1, 1, -4) |
## Limitations
- **Fixed input size**: 8 bits only (algebraic construction extends to any n)
- **Binary inputs**: Expects {0, 1}, not continuous values
- **No noise margin**: Heaviside threshold at exactly 0
- **Not differentiable**: Cannot be fine-tuned with gradient descent
## Files
```
tiny-mod5-prover/
├── model.safetensors # Network weights (146 params)
├── model.py # Inference code
├── config.json # Model metadata
└── README.md # This file
```
## Citation
```bibtex
@software{tiny_mod5_prover_2026,
title={tiny-mod5-prover: Formally Verified Threshold Network for MOD-5},
author={Norton, Charles},
url={https://huggingface.co/phanerozoic/tiny-mod5-prover},
year={2026},
note={Part of the verified MOD-m threshold circuit family}
}
```
## Related
- **Proof repository**: [mod5-verified](https://github.com/CharlesCNorton/mod5-verified)
- **MOD-3 network**: [tiny-mod3-prover](https://huggingface.co/phanerozoic/tiny-mod3-prover)
- **Parity network**: [tiny-parity-prover](https://huggingface.co/phanerozoic/tiny-parity-prover)
## License
MIT
|