phanerozoic/tiny-mod5-verified

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.

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

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:

Theorem network_correct_exhaustive : verify_all = true.
Proof. vm_compute. reflexivity. Qed.

2. Constructive verification (case analysis):

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:

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

@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
• MOD-3 network: tiny-mod3-prover
• Parity network: tiny-parity-prover

License

MIT