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