|
|
---
|
|
|
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
|
|
|
|
