phanerozoic/tiny-mod7-verified

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.

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

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 — Coq proofs
• tiny-mod5-prover
• tiny-mod3-prover
• tiny-parity-prover

License

MIT