phanerozoic commited on
Commit
e38a17f
·
verified ·
1 Parent(s): a0ae7d0

Upload README.md with huggingface_hub

Browse files
Files changed (1) hide show
  1. README.md +87 -0
README.md ADDED
@@ -0,0 +1,87 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ ---
2
+ license: mit
3
+ tags:
4
+ - formal-verification
5
+ - coq
6
+ - threshold-logic
7
+ - neuromorphic
8
+ ---
9
+
10
+ # tiny-7OutOf8-prover
11
+
12
+ Formally verified 7-out-of-8 threshold gate. Single threshold neuron with 100% accuracy.
13
+
14
+ ## Architecture
15
+
16
+ | Component | Value |
17
+ |-----------|-------|
18
+ | Inputs | 8 |
19
+ | Outputs | 1 |
20
+ | Neurons | 1 |
21
+ | Parameters | 9 |
22
+ | Weights | [1, 1, 1, 1, 1, 1, 1, 1] |
23
+ | Bias | -7 |
24
+ | Activation | Heaviside step |
25
+
26
+ ## Key Properties
27
+
28
+ - 100% accuracy (256/256 inputs correct)
29
+ - Coq-proven correctness
30
+ - Single threshold neuron
31
+ - Integer weights
32
+ - Fires when at least 7 of 8 inputs are true
33
+
34
+
35
+ ## Usage
36
+
37
+ ```python
38
+ import torch
39
+ from safetensors.torch import load_file
40
+
41
+ weights = load_file('sevenoutof8.safetensors')
42
+
43
+ def sevenoutof8_gate(bits):
44
+ # bits: list of 8 binary values
45
+ inputs = torch.tensor([float(b) for b in bits])
46
+ weighted_sum = (inputs * weights['weight']).sum() + weights['bias']
47
+ return int(weighted_sum >= 0)
48
+
49
+ # Test
50
+ print({func}_gate([0,0,0,0,0,0,0,0])) # 0 (0/7, below threshold)
51
+ print({func}_gate([1,1,1,1,1,1,0,0])) # 0 (6/8, below threshold)
52
+ print({func}_gate([1,1,1,1,1,1,1,0])) # 1 (7/8, at threshold)
53
+ print(sevenoutof8_gate([1,1,1,1,1,1,1,1])) # 1 (8/8, above threshold)
54
+ ```
55
+
56
+ ## Verification
57
+
58
+ **Coq Theorem**:
59
+ ```coq
60
+ Theorem sevenout_eight_correct : forall x0 x1 x2 x3 x4 x5 x6 x7,
61
+ sevenout_eight_circuit [x0; x1; x2; x3; x4; x5; x6; x7] =
62
+ sevenout_eight_spec [x0; x1; x2; x3; x4; x5; x6; x7].
63
+ ```
64
+
65
+ Proven axiom-free via:
66
+ 1. **Exhaustive**: All 256 inputs verified
67
+ 2. **Universal**: Quantified proof over boolean combinations
68
+ 3. **Algebraic**: Hamming weight ≥ 7
69
+
70
+ Full proof: [coq-circuits/Threshold/SevenOutOfEight.v](https://github.com/CharlesCNorton/coq-circuits)
71
+
72
+ ## Circuit Operation
73
+
74
+ Input with h true bits (Hamming weight h):
75
+ - Weighted sum: h - 7
76
+ - Output: 1 if h ≥ 7, else 0
77
+
78
+ ## Citation
79
+
80
+ ```bibtex
81
+ @software{tiny_7outof8_prover_2025,
82
+ title={tiny-7OutOf8-prover: Formally Verified 7-out-of-8 threshold gate},
83
+ author={Norton, Charles},
84
+ url={https://huggingface.co/phanerozoic/tiny-7OutOf8-prover},
85
+ year={2025}
86
+ }
87
+ ```