用轻量框架发现大规模分布式训练中的隐性错误。
Verifying Computational Graphs in Production-Grade Distributed Machine Learning Frameworks
- 通过等式饱和与逻辑推理验证计算图语义等价性。
- 可在几分钟内验证4050亿参数的Llama模型。
- 定位到具体代码位置，提供可操作的调试建议。
现代机器学习框架通过并行化和优化技术支持超大规模模型，但这些技术也引入了复杂的隐性错误，严重降低模型性能。现有解决方案或临时应对，或成本过高，难以用于生产。我们提出Scalify，一个轻量级框架，利用等式饱和与类Datalog推理，验证计算图的语义等价性，以暴露隐性错误。为实现可扩展性，Scalify采用并行重写与分层记忆化，复用重写模板，并将等式饱和与关系推理及符号双射推断结合。该方法能精确定位差异位置，将验证结果转化为可操作的调试指导。Scalify可在普通机器上于数分钟内验证高达Llama-3.1-405B规模的模型，并在亚马逊生产级机器学习框架中发现了五个未知缺陷。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。