# TrainVerify: Equivalence-Based Verification for Distributed LLM Training

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 81 references that are in the map.
- First posted on arXiv 19 Jun 2025.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [Llama 2: Open Foundation and Fine-Tuned Chat Models](https://mlsanity.com/paper/2307.09288/) (2023)
- [Scaling Laws for Neural Language Models](https://mlsanity.com/paper/2001.08361/) (2020)
- [Megatron-LM: Training Multi-Billion Parameter Language Models Using Model Parallelism](https://mlsanity.com/paper/1909.08053/) (2019)
- [ZeRO: Memory Optimizations Toward Training Trillion Parameter Models](https://mlsanity.com/paper/1910.02054/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Ring Attention with Blockwise Transformers for Near-Infinite Context](https://mlsanity.com/paper/2310.01889/) (2023)
- [DeepSpeed-MoE: Advancing Mixture-of-Experts Inference and Training to Power Next-Generation AI Scale](https://mlsanity.com/paper/2201.05596/) (2022)
- [Reducing Activation Recomputation in Large Transformer Models](https://mlsanity.com/paper/2205.05198/) (2022)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Ansor: Generating High-Performance Tensor Programs for Deep Learning](https://mlsanity.com/paper/2006.06762/) (2020)
- [The rising costs of training frontier AI models](https://mlsanity.com/paper/2405.21015/) (2024)
- [DeepID3: Face Recognition with Very Deep Neural Networks](https://mlsanity.com/paper/1502.00873/) (2015)
- [Oobleck: Resilient Distributed Training of Large Models Using Pipeline Templates](https://mlsanity.com/paper/2309.08125/) (2023)
- [NNSmith: Generating Diverse and Valid Test Cases for Deep Learning Compilers](https://mlsanity.com/paper/2207.13066/) (2022)
- [Maximizing Parallelism in Distributed Training for Huge Neural Networks](https://mlsanity.com/paper/2105.14450/) (2021)
- [OneFlow: Redesign the Distributed Deep Learning Framework from Scratch](https://mlsanity.com/paper/2110.15032/) (2021)
- [Training with Confidence: Catching Silent Errors in Deep Learning Training with Automated Proactive Checks](https://mlsanity.com/paper/2506.14813/) (2025)
- [Revisiting Differential Verification: Equivalence Verification with Confidence](https://mlsanity.com/paper/2410.20207/) (2024)
- [Revealing Floating-Point Accumulation Orders in Software/Hardware Implementations](https://mlsanity.com/paper/2411.00442/) (2024)

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

- [Role-Based Fault Tolerance System for LLM RL Post-Training](https://mlsanity.com/paper/2512.22492/) (2025)
- [Verifying Computational Graphs in Production-Grade Distributed Machine Learning Frameworks](https://mlsanity.com/paper/2509.10694/) (2025)
- [SCOUT: Symmetric Consensus Outlier Detection for Failure Localization in LLM Pre-Training](https://mlsanity.com/paper/2608.11034/) (2026)

## Abstract (arXiv)

Training large language models (LLMs) at scale requires parallel execution across thousands of devices, incurring enormous computational costs. Yet, these costly distributed trainings are rarely verified, leaving them prone to silent errors and potentially wasting millions of GPU hours. We introduce TrainVerify, a system for verifiable distributed training of LLMs. Given a deep learning model's logical specification as the ground truth, TrainVerify formally verifies that a distributed parallel execution plan is mathematically equivalent to it. Direct verification is notoriously difficult due to the sheer scale of LLMs which often involves billions of variables and highly intricate computation graphs. Therefore, TrainVerify introduces shape-reduction techniques and a stage-wise parallel verification algorithm that significantly reduces complexity while preserving formal correctness. TrainVerify scales to frontier LLMs, including the successful verification of the Llama3 (405B) and DeepSeek-V3 (671B) training plans.