# ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 37 references that are in the map.
- First posted on arXiv 24 Dec 2025.

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

- [Optuna: A Next-generation Hyperparameter Optimization Framework](https://mlsanity.com/paper/1907.10902/) (2019)
- [Deeper Insights into Graph Convolutional Networks for Semi-Supervised Learning](https://mlsanity.com/paper/1801.07606/) (2018)
- [On the Bottleneck of Graph Neural Networks and its Practical Implications](https://mlsanity.com/paper/2006.05205/) (2020)
- [Masked Label Prediction: Unified Message Passing Model for Semi-Supervised Classification](https://mlsanity.com/paper/2009.03509/) (2020)
- [Understanding Attention and Generalization in Graph Neural Networks](https://mlsanity.com/paper/1905.02850/) (2019)
- [Gamora: Graph Learning based Symbolic Reasoning for Large-Scale Boolean Networks](https://mlsanity.com/paper/2303.08256/) (2023)
- [DeepGate3: Towards Scalable Circuit Representation Learning](https://mlsanity.com/paper/2407.11095/) (2024)

## Abstract (arXiv)

We present ReVEAL, a graph-learning-based method for reverse engineering of multiplier architectures to improve algebraic circuit verification techniques. Our framework leverages structural graph features and learning-driven inference to identify architecture patterns at scale, enabling robust handling of large optimized multipliers. We demonstrate applicability across diverse multiplier benchmarks and show improvements in scalability and accuracy compared to traditional rule-based approaches. The method integrates smoothly with existing verification flows and supports downstream algebraic proof strategies.
