让大模型分布式训练可验证，防错保效率
TrainVerify: Equivalence-Based Verification for Distributed LLM Training
- 通过形式化等价性验证，确保分布式训练与原模型一致
- 成功验证4050亿和6710亿参数模型的训练计划
- 适合需要高可靠性的大模型训练团队
大规模语言模型（LLM）的训练需在数千设备上并行执行，成本高昂。然而，这些耗资巨大的分布式训练很少被验证，易产生无声错误，浪费数百万GPU小时。我们提出TrainVerify，一种支持可验证分布式训练的系统。给定模型的逻辑规范作为真实基准，TrainVerify可形式化验证分布式并行执行方案是否在数学上等价于该规范。由于LLM规模庞大，常涉及数十亿变量和复杂计算图，直接验证极为困难。为此，TrainVerify引入形状简化技术与分阶段并行验证算法，在保持形式正确性的同时显著降低复杂度。系统可扩展至前沿大模型，成功验证了Llama3（405B）和DeepSeek-V3（671B）的训练计划。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。