| # Future Work | |
| ## 1. Different function | |
| Apply the train→export→verify pipeline to problems beyond parity: | |
| - **Majority vote**: output 1 if more than half of inputs are 1 | |
| - **Addition carry**: output the carry bit of two 4-bit numbers | |
| - **Threshold-k**: output 1 if at least k inputs are 1 | |
| - **Simple classifiers**: functions where the optimal circuit structure is not obvious | |
| These would test whether the methodology generalizes beyond symmetric Boolean functions. | |
| ## 2. Neuromorphic deployment | |
| Deploy the network on actual neuromorphic hardware (Intel Loihi, IBM TrueNorth, BrainChip Akida) or a cycle-accurate simulator. Measure power consumption, latency, and resource utilization. Validate that the claimed use case—formally verified parity on hardware that cannot implement XOR gates—is practical. | |
| ## 3. Paper | |
| Write up the methodology for publication. Key contributions: | |
| - Evolutionary search for threshold networks on gradient-hostile loss landscapes | |
| - Ternary weight quantization enabling exhaustive Coq verification | |
| - Neuron ablation analysis and principled pruning | |
| - End-to-end pipeline from training to formal proof | |
| Target venues: CAV, ICML, NeurIPS, or a formal methods workshop. | |
| ## 4. Tooling | |
| Package the pipeline into a unified CLI: | |
| ``` | |
| verified-nn --function parity --bits 8 --output model/ | |
| ``` | |
| The tool would: | |
| 1. Train via evolutionary search until 100% accuracy | |
| 2. Export weights to Coq | |
| 3. Compile and verify proofs | |
| 4. Optionally run ablation and pruning | |
| 5. Output SafeTensors + verified Coq proofs | |
| This would lower the barrier to creating new verified networks. | |