|
|
--- |
|
|
license: mit |
|
|
tags: |
|
|
- formal-verification |
|
|
- coq |
|
|
- threshold-logic |
|
|
- neuromorphic |
|
|
- multi-layer |
|
|
- equivalence |
|
|
--- |
|
|
|
|
|
# tiny-BiImplies-verified |
|
|
|
|
|
Formally verified biconditional gate (if and only if). Two-layer threshold network computing logical equivalence with 100% accuracy. |
|
|
|
|
|
## Architecture |
|
|
|
|
|
| Component | Value | |
|
|
|-----------|-------| |
|
|
| Inputs | 2 | |
|
|
| Outputs | 1 | |
|
|
| Neurons | 3 (2 hidden, 1 output) | |
|
|
| Layers | 2 | |
|
|
| Parameters | 9 | |
|
|
| **Layer 1, Neuron 1 (NOR)** | | |
|
|
| Weights | [-1, -1] | |
|
|
| Bias | 0 | |
|
|
| **Layer 1, Neuron 2 (AND)** | | |
|
|
| Weights | [1, 1] | |
|
|
| Bias | -2 | |
|
|
| **Layer 2 (OR)** | | |
|
|
| Weights | [1, 1] | |
|
|
| Bias | -1 | |
|
|
| Activation | Heaviside step (all layers) | |
|
|
|
|
|
## Key Properties |
|
|
|
|
|
- 100% accuracy (4/4 inputs correct) |
|
|
- Coq-proven correctness |
|
|
- Minimal 2-layer architecture |
|
|
- Integer weights |
|
|
- Equivalence relation (reflexive, symmetric, transitive) |
|
|
- Identical to XNOR |
|
|
|
|
|
## Usage |
|
|
|
|
|
```python |
|
|
import torch |
|
|
from safetensors.torch import load_file |
|
|
|
|
|
weights = load_file('biimplies.safetensors') |
|
|
|
|
|
def biimplies_gate(x, y): |
|
|
inputs = torch.tensor([float(x), float(y)]) |
|
|
|
|
|
# Layer 1: NOR and AND |
|
|
nor_sum = (inputs * weights['layer1.neuron1.weight']).sum() + weights['layer1.neuron1.bias'] |
|
|
nor_out = int(nor_sum >= 0) |
|
|
|
|
|
and_sum = (inputs * weights['layer1.neuron2.weight']).sum() + weights['layer1.neuron2.bias'] |
|
|
and_out = int(and_sum >= 0) |
|
|
|
|
|
# Layer 2: OR |
|
|
layer1_outs = torch.tensor([float(nor_out), float(and_out)]) |
|
|
or_sum = (layer1_outs * weights['layer2.weight']).sum() + weights['layer2.bias'] |
|
|
return int(or_sum >= 0) |
|
|
|
|
|
# Test |
|
|
print(biimplies_gate(0, 0)) # 1 (both false, equivalent) |
|
|
print(biimplies_gate(0, 1)) # 0 (different, not equivalent) |
|
|
print(biimplies_gate(1, 0)) # 0 (different, not equivalent) |
|
|
print(biimplies_gate(1, 1)) # 1 (both true, equivalent) |
|
|
``` |
|
|
|
|
|
## Verification |
|
|
|
|
|
**Coq Theorem**: |
|
|
```coq |
|
|
Theorem biimplies_correct : forall x y, biimplies_circuit x y = eqb x y. |
|
|
``` |
|
|
|
|
|
Proven axiom-free with properties: |
|
|
- Reflexivity (x ↔ x) |
|
|
- Symmetry (x ↔ y → y ↔ x) |
|
|
- Transitivity (x ↔ y ∧ y ↔ z → x ↔ z) |
|
|
- Full equivalence relation |
|
|
|
|
|
Full proof: [coq-circuits/Boolean/BiImplies.v](https://github.com/CharlesCNorton/coq-circuits/blob/main/coq/Boolean/BiImplies.v) |
|
|
|
|
|
## Circuit Operation |
|
|
|
|
|
BiImplies outputs true when inputs are equal. |
|
|
|
|
|
BiImplies(x,y) = OR(NOR(x,y), AND(x,y)) = (x ↔ y) |
|
|
|
|
|
## Citation |
|
|
|
|
|
```bibtex |
|
|
@software{tiny_biimplies_prover_2025, |
|
|
title={tiny-BiImplies-verified: Formally Verified Biconditional Gate}, |
|
|
author={Norton, Charles}, |
|
|
url={https://huggingface.co/phanerozoic/tiny-BiImplies-verified}, |
|
|
year={2025} |
|
|
} |
|
|
``` |
|
|
|
