Verifying Computational Graphs in Production-Grade Distributed Machine Learning Frameworks
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909786012909568 |
|---|---|
| author | Zulkifli, Kahfi S. Qian, Wenbo Zhu, Shaowei Zhou, Yuan Zhang, Zhen Lou, Chang |
| author_facet | Zulkifli, Kahfi S. Qian, Wenbo Zhu, Shaowei Zhou, Yuan Zhang, Zhen Lou, Chang |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_10694 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Verifying Computational Graphs in Production-Grade Distributed Machine Learning Frameworks Zulkifli, Kahfi S. Qian, Wenbo Zhu, Shaowei Zhou, Yuan Zhang, Zhen Lou, Chang Machine Learning Programming Languages 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. |
| title | Verifying Computational Graphs in Production-Grade Distributed Machine Learning Frameworks |
| topic | Machine Learning Programming Languages |
| url | https://arxiv.org/abs/2509.10694 |