File size: 2,352 Bytes
25d9c47 |
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 |
---
license: mit
tags:
- pytorch
- safetensors
- formal-verification
- coq
- mod7
- modular-arithmetic
- threshold-network
- neuromorphic
---
# tiny-mod7-prover
Formally verified neural network that computes the MOD-7 function (Hamming weight mod 7) on 8-bit inputs. For Coq source code, see [mod7-verified](https://github.com/CharlesCNorton/mod7-verified).
## Overview
Threshold network computing `mod7(x) = HW(x) mod 7` for 8-bit binary inputs. Outputs 0-6 corresponding to the seven residue classes.
**Key properties:**
- 100% accuracy on all 256 possible inputs
- Correctness proven in Coq (axiom-free)
- Integer weights, Heaviside activation
- Part of the verified MOD-m family
## Architecture
| Layer | Neurons | Function |
|-------|---------|----------|
| Input | 8 | Binary input bits |
| Hidden 1 | 9 | Thermometer encoding |
| Hidden 2 | 6 | MOD-7 detection |
| Output | 7 | Classification |
**Total: 22 neurons, 190 parameters**
## Algebraic Insight
For MOD-m, use weights `(1, 1, ..., 1, 1-m)` with `m-1` ones before the reset.
MOD-7 uses `(1, 1, 1, 1, 1, 1, -6)`:
```
HW=0: cumsum=0, HW=1: cumsum=1, ..., HW=6: cumsum=6
HW=7: cumsum=0 (reset: 1+1+1+1+1+1-6=0)
HW=8: cumsum=1
```
## Formal Verification
```coq
Theorem network_correct_exhaustive : verify_all = true.
Theorem network_correct_constructive : forall x0 x1 x2 x3 x4 x5 x6 x7,
predict [x0; x1; x2; x3; x4; x5; x6; x7] = mod7 [x0; x1; x2; x3; x4; x5; x6; x7].
Theorem cumsum_eq_mod7 : forall k,
(k <= 8)%nat -> cumsum k = Z.of_nat (Nat.modulo k 7).
```
All proofs axiom-free.
## 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) |
| **tiny-mod7-prover** | MOD-7 | 22 | 190 | (1, 1, 1, 1, 1, 1, -6) |
## Related
- [mod7-verified](https://github.com/CharlesCNorton/mod7-verified) — Coq proofs
- [tiny-mod5-prover](https://huggingface.co/phanerozoic/tiny-mod5-prover)
- [tiny-mod3-prover](https://huggingface.co/phanerozoic/tiny-mod3-prover)
- [tiny-parity-prover](https://huggingface.co/phanerozoic/tiny-parity-prover)
## License
MIT
|