# Logic Gate Neural Networks are Good for Verification

arXiv: https://arxiv.org/abs/2505.19932 · HTML: https://mlsanity.com/paper/2505.19932/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 24 of its 41 references that are in the map.
- First posted on arXiv 26 May 2025.

## Builds on (most cited first, 24 of 24)

- [Concrete Problems in AI Safety](https://mlsanity.com/paper/1606.06565/) (2016)
- [A Survey of Quantization Methods for Efficient Neural Network Inference](https://mlsanity.com/paper/2103.13630/) (2021)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Retiring Adult: New Datasets for Fair Machine Learning](https://mlsanity.com/paper/2108.04884/) (2021)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Binary Neural Networks: A Survey](https://mlsanity.com/paper/2004.03333/) (2020)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Strong mixed-integer programming formulations for trained neural networks](https://mlsanity.com/paper/1811.08359/) (2018)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Deep Differentiable Logic Gate Networks](https://mlsanity.com/paper/2210.08277/) (2022)
- [Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming](https://mlsanity.com/paper/2010.11645/) (2020)
- [Convolutional Differentiable Logic Gate Networks](https://mlsanity.com/paper/2411.04732/) (2024)
- [Efficient Exact Verification of Binarized Neural Networks](https://mlsanity.com/paper/2005.03597/) (2020)
- [Scalable Verification of Quantized Neural Networks (Technical Report)](https://mlsanity.com/paper/2012.08185/) (2020)
- [Fairify: Fairness Verification of Neural Networks](https://mlsanity.com/paper/2212.06140/) (2022)
- [CertiFair: A Framework for Certified Global Fairness of Neural Networks](https://mlsanity.com/paper/2205.09927/) (2022)
- [Efficient Global Robustness Certification of Neural Networks via Interleaving Twin-Network Encoding](https://mlsanity.com/paper/2203.14141/) (2022)
- [Verification of Neural Networks' Global Robustness](https://mlsanity.com/paper/2402.19322/) (2024)
- [Verifying Global Two-Safety Properties in Neural Networks with Confidence](https://mlsanity.com/paper/2405.14400/) (2024)
- [Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks](https://mlsanity.com/paper/2211.16187/) (2022)

## Built on by (most cited first, 4 of 4)

- [LILogic Net: Compact Logic Gate Networks with Learnable Connectivity for Efficient Hardware Deployment](https://mlsanity.com/paper/2511.12340/) (2025)
- [Scalable Interconnect Learning in Boolean Networks](https://mlsanity.com/paper/2507.02585/) (2025)
- [Differentiable Weightless Controllers: Learning Logic Circuits for Continuous Control](https://mlsanity.com/paper/2512.01467/) (2025)
- [Self-Organising Digital Circuits](https://mlsanity.com/paper/2608.02606/) (2026)

## Abstract (arXiv)

Learning-based systems are increasingly deployed across various domains, yet the complexity of traditional neural networks poses significant challenges for formal verification. Unlike conventional neural networks, learned Logic Gate Networks (LGNs) replace multiplications with Boolean logic gates, yielding a sparse, netlist-like architecture that is inherently more amenable to symbolic verification, while still delivering promising performance. In this paper, we introduce a SAT encoding for verifying global robustness and fairness in LGNs. We evaluate our method on five benchmark datasets, including a newly constructed 5-class variant, and find that LGNs are both verification-friendly and maintain strong predictive performance.