TrainVerify: Equivalence-Based Verification for Distributed LLM Training
This addresses the critical issue of error-prone and costly distributed LLM training for AI researchers and practitioners, representing a novel verification approach rather than an incremental improvement.
The paper tackles the problem of verifying distributed training of large language models (LLMs) to prevent silent errors and wasted GPU hours, introducing TrainVerify, which formally verifies equivalence between distributed execution plans and logical specifications, scaling to models like Llama3 (405B) and DeepSeek-V3 (671B).
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.