Rename from tiny-Majority-verified
Browse files- README.md +84 -0
- config.json +22 -0
- model.py +71 -0
- model.safetensors +3 -0
README.md
ADDED
|
@@ -0,0 +1,84 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
---
|
| 2 |
+
license: mit
|
| 3 |
+
tags:
|
| 4 |
+
- pytorch
|
| 5 |
+
- safetensors
|
| 6 |
+
- threshold-logic
|
| 7 |
+
- neuromorphic
|
| 8 |
+
---
|
| 9 |
+
|
| 10 |
+
# threshold-majority
|
| 11 |
+
|
| 12 |
+
Strict majority detector for 8 inputs. Fires when more than half are active.
|
| 13 |
+
|
| 14 |
+
## Circuit
|
| 15 |
+
|
| 16 |
+
```
|
| 17 |
+
x₀ x₁ x₂ x₃ x₄ x₅ x₆ x₇
|
| 18 |
+
│ │ │ │ │ │ │ │
|
| 19 |
+
└──┴──┴──┴──┼──┴──┴──┴──┘
|
| 20 |
+
▼
|
| 21 |
+
┌─────────┐
|
| 22 |
+
│ w: all 1│
|
| 23 |
+
│ b: -5 │
|
| 24 |
+
└─────────┘
|
| 25 |
+
│
|
| 26 |
+
▼
|
| 27 |
+
HW ≥ 5?
|
| 28 |
+
```
|
| 29 |
+
|
| 30 |
+
## Mechanism
|
| 31 |
+
|
| 32 |
+
- Sum = (number of 1s) - 5
|
| 33 |
+
- Fires when Hamming weight ≥ 5 (more 1s than 0s)
|
| 34 |
+
|
| 35 |
+
A tie (4-4) doesn't count as majority. You need strictly more than half.
|
| 36 |
+
|
| 37 |
+
Functionally identical to threshold-5outof8.
|
| 38 |
+
|
| 39 |
+
## Duality with Minority
|
| 40 |
+
|
| 41 |
+
| Circuit | Weights | Bias | Fires when |
|
| 42 |
+
|---------|---------|------|------------|
|
| 43 |
+
| **Majority** | all +1 | -5 | HW ≥ 5 |
|
| 44 |
+
| Minority | all -1 | +3 | HW ≤ 3 |
|
| 45 |
+
|
| 46 |
+
Majority: "enough votes to pass"
|
| 47 |
+
Minority: "not enough votes to block"
|
| 48 |
+
|
| 49 |
+
These are not complements (they don't sum to 1). The gap at HW=4 belongs to neither.
|
| 50 |
+
|
| 51 |
+
## Parameters
|
| 52 |
+
|
| 53 |
+
| | |
|
| 54 |
+
|---|---|
|
| 55 |
+
| Weights | [1, 1, 1, 1, 1, 1, 1, 1] |
|
| 56 |
+
| Bias | -5 |
|
| 57 |
+
| Total | 9 parameters |
|
| 58 |
+
|
| 59 |
+
## Usage
|
| 60 |
+
|
| 61 |
+
```python
|
| 62 |
+
from safetensors.torch import load_file
|
| 63 |
+
import torch
|
| 64 |
+
|
| 65 |
+
w = load_file('model.safetensors')
|
| 66 |
+
|
| 67 |
+
def majority(bits):
|
| 68 |
+
inputs = torch.tensor([float(b) for b in bits])
|
| 69 |
+
return int((inputs * w['weight']).sum() + w['bias'] >= 0)
|
| 70 |
+
```
|
| 71 |
+
|
| 72 |
+
## Files
|
| 73 |
+
|
| 74 |
+
```
|
| 75 |
+
threshold-majority/
|
| 76 |
+
├── model.safetensors
|
| 77 |
+
├── model.py
|
| 78 |
+
├── config.json
|
| 79 |
+
└── README.md
|
| 80 |
+
```
|
| 81 |
+
|
| 82 |
+
## License
|
| 83 |
+
|
| 84 |
+
MIT
|
config.json
ADDED
|
@@ -0,0 +1,22 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
{
|
| 2 |
+
"model_type": "threshold_network",
|
| 3 |
+
"task": "majority_gate",
|
| 4 |
+
"architecture": "8 -> 1",
|
| 5 |
+
"input_size": 8,
|
| 6 |
+
"output_size": 1,
|
| 7 |
+
"num_neurons": 1,
|
| 8 |
+
"num_parameters": 9,
|
| 9 |
+
"threshold": 5,
|
| 10 |
+
"activation": "heaviside",
|
| 11 |
+
"weight_constraints": "integer",
|
| 12 |
+
"verification": {
|
| 13 |
+
"method": "coq_proof",
|
| 14 |
+
"exhaustive": true,
|
| 15 |
+
"inputs_tested": 256
|
| 16 |
+
},
|
| 17 |
+
"accuracy": {
|
| 18 |
+
"all_inputs": "256/256",
|
| 19 |
+
"percentage": 100.0
|
| 20 |
+
},
|
| 21 |
+
"github": "https://github.com/CharlesCNorton/coq-circuits"
|
| 22 |
+
}
|
model.py
ADDED
|
@@ -0,0 +1,71 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
"""
|
| 2 |
+
Threshold Network for Majority Gate
|
| 3 |
+
|
| 4 |
+
A formally verified single-neuron threshold network computing 8-bit majority.
|
| 5 |
+
Outputs 1 when 5 or more of the 8 inputs are true (strict majority).
|
| 6 |
+
"""
|
| 7 |
+
|
| 8 |
+
import torch
|
| 9 |
+
from safetensors.torch import load_file
|
| 10 |
+
|
| 11 |
+
|
| 12 |
+
class ThresholdMajority:
|
| 13 |
+
"""
|
| 14 |
+
Majority gate implemented as a threshold neuron.
|
| 15 |
+
|
| 16 |
+
Circuit: output = (sum of inputs + bias >= 0)
|
| 17 |
+
With all weights=1, bias=-5: fires when hamming weight >= 5.
|
| 18 |
+
"""
|
| 19 |
+
|
| 20 |
+
def __init__(self, weights_dict):
|
| 21 |
+
self.weight = weights_dict['weight']
|
| 22 |
+
self.bias = weights_dict['bias']
|
| 23 |
+
|
| 24 |
+
def __call__(self, bits):
|
| 25 |
+
inputs = torch.tensor([float(b) for b in bits])
|
| 26 |
+
weighted_sum = (inputs * self.weight).sum() + self.bias
|
| 27 |
+
return (weighted_sum >= 0).float()
|
| 28 |
+
|
| 29 |
+
@classmethod
|
| 30 |
+
def from_safetensors(cls, path="model.safetensors"):
|
| 31 |
+
return cls(load_file(path))
|
| 32 |
+
|
| 33 |
+
|
| 34 |
+
def forward(x, weights):
|
| 35 |
+
"""
|
| 36 |
+
Forward pass with Heaviside activation.
|
| 37 |
+
|
| 38 |
+
Args:
|
| 39 |
+
x: Input tensor of shape [..., 8]
|
| 40 |
+
weights: Dict with 'weight' and 'bias' tensors
|
| 41 |
+
|
| 42 |
+
Returns:
|
| 43 |
+
1 if majority (5+ of 8) are true, else 0
|
| 44 |
+
"""
|
| 45 |
+
x = torch.as_tensor(x, dtype=torch.float32)
|
| 46 |
+
weighted_sum = (x * weights['weight']).sum(dim=-1) + weights['bias']
|
| 47 |
+
return (weighted_sum >= 0).float()
|
| 48 |
+
|
| 49 |
+
|
| 50 |
+
if __name__ == "__main__":
|
| 51 |
+
weights = load_file("model.safetensors")
|
| 52 |
+
model = ThresholdMajority(weights)
|
| 53 |
+
|
| 54 |
+
print("Majority Gate Tests:")
|
| 55 |
+
print("-" * 40)
|
| 56 |
+
|
| 57 |
+
test_cases = [
|
| 58 |
+
[0,0,0,0,0,0,0,0],
|
| 59 |
+
[1,0,0,0,0,0,0,0],
|
| 60 |
+
[1,1,1,1,0,0,0,0],
|
| 61 |
+
[1,1,1,1,1,0,0,0],
|
| 62 |
+
[1,1,1,1,1,1,0,0],
|
| 63 |
+
[1,1,1,1,1,1,1,1],
|
| 64 |
+
]
|
| 65 |
+
|
| 66 |
+
for bits in test_cases:
|
| 67 |
+
hw = sum(bits)
|
| 68 |
+
out = int(model(bits).item())
|
| 69 |
+
expected = 1 if hw >= 5 else 0
|
| 70 |
+
status = "OK" if out == expected else "FAIL"
|
| 71 |
+
print(f"HW={hw}: Majority({bits}) = {out} [{status}]")
|
model.safetensors
ADDED
|
@@ -0,0 +1,3 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
version https://git-lfs.github.com/spec/v1
|
| 2 |
+
oid sha256:7d01848d8d9961c12dac0b923a1f92f6d03ac7395cc8957bbc1b24c5aa37094c
|
| 3 |
+
size 164
|