# Verifying Computational Graphs in Production-Grade Distributed Machine Learning Frameworks

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 15 of its 82 references that are in the map.
- First posted on arXiv 12 Sep 2025.

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

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Megatron-LM: Training Multi-Billion Parameter Language Models Using Model Parallelism](https://mlsanity.com/paper/1909.08053/) (2019)
- [DeepTest: Automated Testing of Deep-Neural-Network-driven Autonomous Cars](https://mlsanity.com/paper/1708.08559/) (2017)
- [Mirage: A Multi-Level Superoptimizer for Tensor Programs](https://mlsanity.com/paper/2405.05751/) (2024)
- [Hidet: Task-Mapping Programming Paradigm for Deep Learning Tensor Programs](https://mlsanity.com/paper/2210.09603/) (2022)
- [Equality Saturation for Tensor Graph Superoptimization](https://mlsanity.com/paper/2101.01332/) (2021)
- [Silent Bugs in Deep Learning Frameworks: An Empirical Study of Keras and TensorFlow](https://mlsanity.com/paper/2112.13314/) (2021)
- [Rewrite Rule Inference Using Equality Saturation](https://mlsanity.com/paper/2108.10436/) (2021)
- [Coverage-Guided Tensor Compiler Fuzzing with Joint IR-Pass Mutation](https://mlsanity.com/paper/2202.09947/) (2022)
- [BagPipe: Accelerating Deep Recommendation Model Training](https://mlsanity.com/paper/2202.12429/) (2022)
- [On Neural Network Equivalence Checking using SMT Solvers](https://mlsanity.com/paper/2203.11629/) (2022)
- [Training with Confidence: Catching Silent Errors in Deep Learning Training with Automated Proactive Checks](https://mlsanity.com/paper/2506.14813/) (2025)
- [MCTS-GEB: Monte Carlo Tree Search is a Good E-graph Builder](https://mlsanity.com/paper/2303.04651/) (2023)
- [Better Together: Unifying Datalog and Equality Saturation](https://mlsanity.com/paper/2304.04332/) (2023)
- [TrainVerify: Equivalence-Based Verification for Distributed LLM Training](https://mlsanity.com/paper/2506.15961/) (2025)

## Abstract (arXiv)

Modern machine learning frameworks support very large models by incorporating parallelism and optimization techniques. Yet, these very techniques add new layers of complexity, introducing silent errors that severely degrade model performance. Existing solutions are either ad hoc or too costly for production. We present Scalify, a lightweight framework that exposes silent errors by verifying semantic equivalence of computational graphs using equality saturation and Datalog-style reasoning. To scale, Scalify partitions graphs with parallel rewriting and layer memoization, reuses rewrite templates, and augments equality saturation with relational reasoning and symbolic bijection inference. It further localizes discrepancies to precise code sites, turning verification results into actionable debugging guidance. Scalify verifies models as large as Llama-3.1-405B within minutes on a commodity machine and exposed five unknown bugs in Amazon production machine learning frameworks.
