Pith. sign in

REVIEW 3 major objections 5 minor 94 references

Verifying Computational Graphs in Production-Grade Distributed Machine Learning Frameworks

T0 review · 3 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Equality saturation can verify semantic equivalence of large ML computational graphs, making silent distributed-framework errors detectable at graph level.

desk verdict Solid systems paper: equality-saturation graph equivalence checking that actually scales to 400B-param models and found five real Amazon bugs; main gap is the asserted soundness of its hand-written rules. read the letter →

arxiv 2509.10694 v1 pith:XQRJ4IR2 submitted 2025-09-12 cs.LG cs.PL

Kahfi S. Zulkifli , Wenbo Qian , Shaowei Zhu , Yuan Zhou , Zhen Zhang , Chang Lou This is my paper · ORCID
classification cs.LGcs.PL
keywords equalitysaturatione-graphcomputationalgraphverificationsilenterrorsdistributedmachinelearningDatalogreasoninglayoutoptimizationbuglocalization
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper claims that semantic equivalence of large machine-learning computational graphs can be verified quickly and cheaply by treating the problem as an equality-saturation search. It presents Scalify, a tool that merges a single-device baseline graph and a distributed or optimized graph into one e-graph, applies rewrite rules plus relational reasoning about sharding and layout, and declares the graphs equivalent if their output nodes land in the same equivalence class. The authors report that this approach verifies models up to Llama-3.1-405B in minutes on a commodity machine, detects 17 of 19 reproduced historical bugs, and uncovered five previously unknown bugs in two Amazon production ML frameworks. A sympathetic reader takes this as evidence that semantic, not numeric, verification is practical at production scale and can expose silent errors that numerical comparison misses.

What carries the argument

The load-bearing machinery is the e-graph (equality graph), a data structure that groups structurally different but semantically equivalent expressions into e-classes; the tool builds one e-graph containing both the baseline and the distributed graph and iteratively applies rewrite rules until saturation. Around this core, Scalify layers a Datalog-style relational analysis that tracks sharded, duplicate, layout, partial, and slice relations across tensors, and a symbolic bijection inference that synthesizes a reshape-transpose-reshape sequence aligning two different layout paths. Layer-boundary partitioning, parallel rewriting threads, and layer memoization keep the e-graph from exploding on deep models.

What would settle it

Construct a pair of graphs whose only difference is a reshape-transpose sequence that the symbolic bijection inference treats as structurally equal but that reorders tensor elements for some concrete shape; run Scalify on random tensors and check whether it reports equivalence while the numeric outputs differ. A single such false-positive case would show the bijection or layout rules are unsound.

Watch

Extended reading notes

Core claim

Scalify's central claim is that verifying semantic equivalence between an original computational graph and its distributed/optimized counterpart reduces to checking whether the two graphs' output tensors can be rewritten into the same e-class via a small set of generic rewrite rules augmented with Datalog-style relation propagation. The tool handles layout heterogeneity by inferring a symbolic bijection between differently structured reshape-transpose sequences, handles scale by partitioning graphs along layer boundaries and memoizing rewritten layer fingerprints, and turns failures into debugging guidance by mapping unverified nodes back to source lines. The paper reports end-to-end verification of Llama-3.1-8B/70B/405B and Mixtral-8x7B/8x22B under tensor, sequence, and expert parallelism within minutes on a 6-core CPU with 16 GB RAM, plus detection of five unknown bugs in Amazon's Transformers NeuronX and NeuronX Distributed frameworks and 17 out of 19 reproduced bugs from prior studies.

Load-bearing premise

The verifier's guarantee rests on the soundness of the 25 manually written rewrite rules and the Datalog-style relation rules in Table 1: if any rule licenses a transformation that does not actually preserve tensor semantics, the tool could certify a buggy graph as verified.

Editorial extensions

If this is right

  • If the claim holds, silent errors in distributed ML frameworks can be caught before training or inference, instead of surfacing only after severe performance degradation.
  • Verification time being independent of tensor shape and parallelization degree makes the check predictable enough to run as a routine pre-flight step in model development pipelines.
  • A verified result eliminates software bugs as a cause of observed degradation, narrowing the search to numerical instability or hardware faults.
  • Since localization points to exact source lines, unverified results directly assist debugging rather than requiring a separate root-cause hunt.
  • Soundness without completeness means users can trust positive results, while treating unverified reports as a prompt for further inspection rather than proof of a bug.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same e-graph equivalence machinery could plausibly extend to training graphs, including backward passes, since the tool operates on IR graphs rather than inference-specific code; the paper only evaluates inference because its current toolchain exports inference IRs.
  • The soundness guarantee rests entirely on hand-written rewrite rules, so mechanically verifying those rules (as some prior compiler-verification efforts do for their own rewrite sets) would strengthen the tool's core correctness claim.
  • The paper's rule set covers tensor, sequence, and expert parallelism; extending to context or pipeline parallelism, which the authors flag as future work, would test whether the relational analysis generalizes beyond the five rule families presented.
  • A combination with gradient-level checks could make the verifier's verdict actionable even when graphs are verified but performance is still poor: software bugs are excluded, so hardware and numerical causes become the remaining suspects.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper presents Scalify, a system that checks whether a single-device computational graph and a distributed or optimized graph are semantically equivalent. It combines equality saturation in egglog with Datalog-style relation propagation, layout and partition analysis, symbolic bijection inference, and discrepancy-based localization. The evaluation reports verification of Llama-3.1-8B/70B/405B and Mixtral models within minutes on a commodity machine, detection of 17 out of 19 re-implemented historical bugs, and five previously unknown bugs in Amazon's NeuronX frameworks.

Significance. If the soundness claim holds, this is a significant advance: it shows equality-saturation-based equivalence checking can scale to production-sized LLM graphs, produces localized bug reports, and catches silent errors that numeric comparison misses. The evaluation is concrete, uses externally reported historical bugs, and the new bugs were submitted to the framework developers, which mitigates self-referential evaluation. The main reason this is not an accept is that the central soundness guarantee is asserted rather than proved, and the rule semantics in Table 1 and Algorithm 2 are not specified tightly enough to audit.

major comments (3)
  1. [§5.1 (Soundness) and §8 (Limitations)] The paper's central guarantee, that a verified verdict implies semantic equivalence, rests on the assertion at the end of §5.1 that the relation analysis and e-graph rewrite rules are sound, and on the restatement in §8 that Scalify is sound. No proof, machine-checked certificate, or formal semantics is supplied for the 25 manually written meta-rules or for the Datalog-style rules in Table 1. Because equality saturation merges nodes into the same e-class whenever a rule fires, one unsound rule suffices to certify a non-equivalent graph as verified, which would invalidate both the bug-detection results and the core correctness claim. Empirical detection of 17/19 re-implemented bugs and five new bugs cannot establish a universal soundness statement. Please provide a formal semantics for the relation language in Figure 7 and a soundness proof for each rule in Table 1 and for the bijection construction in Algorithm 2, or alternatively state explicitly that the tool issues certificates that are sound only relative to the rule set, with a validation-based confidence argument rather than an absolute soundness guarantee.
  2. [§5.2.3, Algorithm 2] The bijection inference algorithm's Step 3 compares symbolic axis expressions by structural equality under the axis map M, and the Scope assumptions paragraph restricts the algorithm to reshapes that merge or split dimensions. The paper does not define what structural equality means for terms built with the axis-combination operator, nor does it prove that the inferred permutation (s1, p, s2) is semantics-preserving for all shapes satisfying the symbolic constraints. If two axes with the same symbolic expression are considered equal even when their strides or memory layouts differ, the check in Algorithm 2 could return a bijection for non-equivalent layout sequences. A concrete definition of layout semantics, the equality test, and a correctness argument for the rank-normalization and permutation search is needed to make the layout-equivalence verdict sound.
  3. [Table 1 and Figure 7] Several rules in Table 1 are printed without the side conditions that the prose uses informally. For instance, the rule for layout propagation through reshape, layout(x, z', reshape(x'.shape) ∘ ℓ, c) ← layout(x,x',ℓ,c), z'=reshape(x',s'), does not state that reshape(x') is a valid reshape or that s' matches the rank and dimension sizes of x. The dot rule for partial(z,z',c,add) does not state that the sharded dimension d is the contraction dimension of the dot. If these conditions are enforced only implicitly in the implementation, the printed rule set is not auditable and cannot support the soundness claim. Please make all rule side conditions explicit in the formal semantics.
minor comments (5)
  1. [Full text, near Figure 2 and Figure 4] The full text contains stray token sequences such as /gid608/gid3/... and a literal /uni2194.15511D in the Figure 4 caption; these look like text-extraction artifacts and should be removed before publication.
  2. [§5.1, Algorithm 1] Algorithm 1 contains a commented-out line reading // update(L_s.out, L_m.out) that appears to be leftover development code; remove it or explain its role.
  3. [§7.1, comparison to TrainVerify] The statement that TrainVerify takes days even for Llama-3.1-405B is not accompanied by a measured runtime in this paper; please provide the source of this timing or soften the claim.
  4. [Figure 12] Figure 12 would be easier to interpret if the underlying verification times for single-thread, parallel-rewrite, and layer-memoization were listed in the caption or a table; the y-axis reaches 3000 seconds but no per-bar values are given.
  5. [§6 Implementation] The paper does not mention an artifact URL or code-release plan; please provide one for reproducibility, especially since the rule set is central to the claims.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: Scalify's equivalence checks are evaluated against external historical bugs and newly reported framework bugs, with no fitted parameter renamed as a prediction.

full rationale

The paper's central derivation chain is: define rewrite rules and relational analysis over computational graphs, run equality saturation via egglog, and report a graph pair as equivalent when output nodes merge into one e-class. The load-bearing assumption is that the 25 manually written meta rules and Table 1's Datalog-style rules are sound, but the paper asserts this soundness (Section 5.1: 'the relation analysis and e-graph rewrite rules are sound') without a machine-checked proof. This is a correctness-risk concern about unproven premises, not circularity: the rules are a modeling choice that could be independently checked, and no rule is defined in terms of the verification outcome it is used to produce. The evaluation does not fit parameters to make bugs detectable: the 19 reproduced bugs come from externally reported historical issue trackers, the five new bugs are submitted to framework developers, and the scalability measurements are directly reported without hidden degrees of freedom. The only self-citations (Lou et al. [56,57]) appear in related work as inspiration for studying silent failures; they do not supply a uniqueness theorem, an ansatz, or a forbidden-alternative argument, so they are not load-bearing. No prediction is equivalent by construction to an input, no fitted value is renamed as a verified result, and no known result is merely relabeled in new coordinates. Therefore, under the stated rules that require exhibiting a specific reduction or self-citation chain, no circularity is found.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The tool adds no fitted numerical constants and no new physical entities. The verification results rest on assumptions about the correctness of the handwritten rule set, the trustworthiness of the baseline graph, and the sufficiency of the supported parallelism forms; these are listed as axioms.

assumptions (4)
  • ad hoc to paper The manually written rewrite rules and Datalog-style relation rules in Table 1 are sound.
    Section 5.1 asserts 'the relation analysis and e-graph rewrite rules are sound', but no proof or machine-checked certificate is provided. All verification results inherit this assumption.
  • domain assumption The single-device graph used as the baseline is semantically correct.
    Section 3 states the original graph 'serves as the baseline without complex transformations (thus more trustworthy)'. Equivalence checking can only detect differences from this baseline, not bugs shared by both graphs.
  • domain assumption All relevant distributed transformations for the evaluated parallelism techniques are expressible with the provided 25 meta rules.
    Section 6 reports about 6.5K LOC encoding 25 meta rules. Completeness of coverage for tensor, sequence, and expert parallelism is not proven; Section 8 acknowledges the tool is not complete.
  • ad hoc to paper Layout transformations can be scoped to reshape operations that merge or split dimensions.
    Section 5.2.3 'Scope assumptions' states this limitation. Bijection inference may return None for other kinds of layouts, causing missed bugs without alerting the user.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Verifying Computational Graphs in Production-Grade Distributed Machine Learning Frameworks." pith.science (2026). https://pith.science/paper/XQRJ4IR2

@misc{pith2026250910694,
  author       = {Pith},
  title        = {Pith review of: Verifying Computational Graphs in Production-Grade Distributed Machine Learning Frameworks},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/XQRJ4IR2}},
  note         = {Machine review of arXiv:2509.10694}
}
read the original abstract

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.

Figures

Figures reproduced from arXiv: 2509.10694 by the authors.

Figure 1
Figure 1. Incorrect layout transformation in BSH optimization. Llama-3.1-405B within minutes on a commodity machine, showing scalability across multiple parallelism techniques including tensor, sequence, and expert parallelism. Scalify uncovered five previously unknown bugs in Amazon’s Trans￾formers NeuronX [27] and NeuronX Distributed [24] frame￾works, in addition to detecting and localizing 17 out of 19 reproduced bugs from… view at source ↗
Figure 2
Figure 2. E-Graph example. result in the attention computation (the root cause is marked in red). The buggy version mistakenly reshapes the tensors to the BSH format n_seqs, n_active_tokens, hidden_size, while it should have accounted for the merging of axes from the result tensor, where the actual result tensor’s dimensions is symbolized as (s * b, h). The wrong reshape operation can lead to incorrect model outputs without e… view at source ↗
Figure 4
Figure 4. Scalify workflow. searching the whole code space is tedious. Developers need guidance to resolve discrepancies beyond confirming bugs. 5 System Design We introduce Scalify, a framework that automatically verifies the semantic equivalence of ML computational graphs from production-grade machine learning frameworks. Scalify in￾troduces the following key techniques: • Scaling e-graphs to production-scale computational … view at source ↗
Figures from the paper (8 more)
Figure 5
Figure 5. Figure 5: Illustration of the topological traversal. previously rewritten subgraphs. Each partitioned subgraph is assigned a fingerprint derived from its single-device and distributed forms. When a new subgraph shares the same fingerprint as an earlier one, Scalify reuses the me…
Figure 6
Figure 6. Figure 6: A full computation graph of different reshape, transpose and dot operators with distributed semantics. We show how the partition and layout analysis is integrated with the propagation process (via rule templates defined from [PITH_FULL_IMAGE:figures/full_fig_p006_6.png]
Figure 7
Figure 7. Figure 7: Syntax of relational analysis. We use italics to denote operations and monospace to denote relation symbols. supplements the missing information by manually specifying which tensors carry device metadata and how they should be interpreted. These registered input relati…
Figure 8
Figure 8. Figure 8: A computation graph with fine-grained slicing and unroll loop analysis. details in Section 5.2.3), which yields an axis correspondence (𝑖 ′ 2 ,𝑖′ 1 , 𝑗′ ) ↔ (𝑗,𝑖1,𝑖2). The allreduce node eliminates the partial relation and restores a normal tensor relation according to…
Figure 9
Figure 9. Figure 9: The bijection inference process described in Algorithm 2. layout transformations with each other. Scalify aims to relate two layout transformations because many optimization tech￾niques encode different layout transformations, and ensuring the equivalence of them is cr…
Figure 10
Figure 10. Figure 10: Upper graph is the oracle and bottom graph is the buggy graph. The layout relation does not propagate because the bijections of the inputs of add are not the same. During the rewrite process, Scalify checks whether the node Scalify rewrites belongs to a relation or no…
Figure 11
Figure 11. Figure 11: Scalify’s performance when checking the equivalence for different configurations.                     [PITH_FULL_IMAGE:figures/full_fig_p011_11.png]
Figure 12
Figure 12. Figure 12: Verification time based on scaling techniques. pinpointed incorrect reshape operators in all-to-all transforma￾tions and tensor sharding, where reshapes failed to produce semantically equivalent tensors. For Bugs #4–5, Scalify iden￾tified the faulty functions but not …

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

94 extracted references · 50 canonical work pages

  1. [1]

    deepspeed-2071: [BUG] FP16 used for all reduce even if BFLOAT16 is enabled.https://github.com/deepspeedai/DeepSpeed/ issues/2071

    [n.d.]. deepspeed-2071: [BUG] FP16 used for all reduce even if BFLOAT16 is enabled.https://github.com/deepspeedai/DeepSpeed/ issues/2071

  2. [2]

    deepspeed-5618: [BUG] ZeRO optimizer with MoE Expert Parallelism.https://github.com/deepspeedai/DeepSpeed/issues/5618

    [n.d.]. deepspeed-5618: [BUG] ZeRO optimizer with MoE Expert Parallelism.https://github.com/deepspeedai/DeepSpeed/issues/5618

  3. [3]

    deepspeed-5808: [BUG] sequence parallel alltoall with batch size > 1.https://github.com/deepspeedai/DeepSpeed/issues/5808

    [n.d.]. deepspeed-5808: [BUG] sequence parallel alltoall with batch size > 1.https://github.com/deepspeedai/DeepSpeed/issues/5808

  4. [4]

    deepspeed-6714: [BUG] pipeline parallelism+fp16+moe isn’t working.https://github.com/deepspeedai/DeepSpeed/issues/6714

    [n.d.]. deepspeed-6714: [BUG] pipeline parallelism+fp16+moe isn’t working.https://github.com/deepspeedai/DeepSpeed/issues/6714

  5. [5]

    deepspeed-7188: [BUG]when use overlap_comm:True with contiguous_gradients:True, grad_norm is NaN.https://github.com/ deepspeedai/DeepSpeed/issues/7188

    [n.d.]. deepspeed-7188: [BUG]when use overlap_comm:True with contiguous_gradients:True, grad_norm is NaN.https://github.com/ deepspeedai/DeepSpeed/issues/7188

  6. [6]

    megatronlm-1611: [BUG] MLA is computed in a different ordercomparedtotheogimpl.https://github.com/NVIDIA/Megatron- LM/issues/1611

    [n.d.]. megatronlm-1611: [BUG] MLA is computed in a different ordercomparedtotheogimpl.https://github.com/NVIDIA/Megatron- LM/issues/1611

  7. [7]

    megatronlm-1620: [BUG] Problem with calculation of self.q_layernorm in qkv_up_proj_and_rope_apply.https://github.com/ NVIDIA/Megatron-LM/issues/1620

    [n.d.]. megatronlm-1620: [BUG] Problem with calculation of self.q_layernorm in qkv_up_proj_and_rope_apply.https://github.com/ NVIDIA/Megatron-LM/issues/1620

  8. [8]

    megatronlm-1699: [BUG] [MLA] k_pos_emb in MLA is not re- ducedacrossTPranksiflinear_kv_down_projisColumnParallelLinear

    [n.d.]. megatronlm-1699: [BUG] [MLA] k_pos_emb in MLA is not re- ducedacrossTPranksiflinear_kv_down_projisColumnParallelLinear. https://github.com/NVIDIA/Megatron-LM/issues/1699

Show all 94 references
  1. [9]

    [n.d.]. megatronlm-32bbb76: Fix bug in distopt allgath- ers with interleaved pipeline parallelism Only first few param all-gathers were being aligned across pipeline paral- lel ranks.https://github.com/NVIDIA/Megatron-LM/commit/ 32bbb76d5767fdbf8dc60d4ef07d103cef8aca02

  2. [10]

    megatronlm-599: [BUG] SwitchMLP router weights are not synchronized within the tensor parallelism group.https://github.com/ NVIDIA/Megatron-LM/issues/599

    [n.d.]. megatronlm-599: [BUG] SwitchMLP router weights are not synchronized within the tensor parallelism group.https://github.com/ NVIDIA/Megatron-LM/issues/599

  3. [11]

    megatronlm-5fffdfc: LinearWithFrozenWeight backward fix when TP > 1.https://github.com/NVIDIA/Megatron-LM/commit/ 5fffdfc737f14297bc3781dfc9e273199d1df52e

    [n.d.]. megatronlm-5fffdfc: LinearWithFrozenWeight backward fix when TP > 1.https://github.com/NVIDIA/Megatron-LM/commit/ 5fffdfc737f14297bc3781dfc9e273199d1df52e

  4. [12]

    nemo-5564: Fix all gather while writing to a file during T5 finetuning.https://github.com/NVIDIA/NeMo/pull/5564

    [n.d.]. nemo-5564: Fix all gather while writing to a file during T5 finetuning.https://github.com/NVIDIA/NeMo/pull/5564

  5. [13]

    nemo-8487: LoRA training with FSDP has spike in train loss

    [n.d.]. nemo-8487: LoRA training with FSDP has spike in train loss. https://github.com/NVIDIA/NeMo/issues/8487

  6. [14]

    nemo-9344:Skipsequence_parallelallreducewhenusingMcore DistOpt.https://github.com/NVIDIA/NeMo/pull/9344

    [n.d.]. nemo-9344:Skipsequence_parallelallreducewhenusingMcore DistOpt.https://github.com/NVIDIA/NeMo/pull/9344

  7. [15]

    transformerengine-3: Add checks for tensor parallel use case to ensure all-reduce is called only when necessary.https://github.com/ NVIDIA/TransformerEngine/pull/3

    [n.d.]. transformerengine-3: Add checks for tensor parallel use case to ensure all-reduce is called only when necessary.https://github.com/ NVIDIA/TransformerEngine/pull/3

  8. [16]

    [n.d.].transformerengine-335:[Bug]scale_invmaybenotsynchronized in TP group.https://github.com/NVIDIA/TransformerEngine/issues/ 335

  9. [17]

    transformersneuronx-0c646b0 : [GPT2]Fix layout changes.https://github.com/aws-neuron/transformers-neuronx/ commit/0c646b02ad36a82bcc13633523de09eb6ed92072

    [n.d.]. transformersneuronx-0c646b0 : [GPT2]Fix layout changes.https://github.com/aws-neuron/transformers-neuronx/ commit/0c646b02ad36a82bcc13633523de09eb6ed92072

  10. [18]

    [n.d.]. transformersneuronx-69d039d: [attention] Fixed B & S transpose issue in BSH attention output.https: //github.com/aws-neuron/transformers-neuronx/commit/ 69d039dc06cf9c1bafde2d637ab1dcf689c3e35b

  11. [19]

    transformersneuronx-e2f5241:slicethekvcachecorrectlywhen using sos.https://github.com/aws-neuron/transformers-neuronx/ commit/e2f524114f9536541fb886f5509ff7cda2a36ce5

    [n.d.]. transformersneuronx-e2f5241:slicethekvcachecorrectlywhen using sos.https://github.com/aws-neuron/transformers-neuronx/ commit/e2f524114f9536541fb886f5509ff7cda2a36ce5

  12. [20]

    Manual Optimization does not synchronize gradients in DDP

    2021. Manual Optimization does not synchronize gradients in DDP. https://github.com/Lightning-AI/pytorch-lightning/issues/9237

    2021

  13. [21]

    [Bug] Gradients not synchronized.https://github.com/kohya- ss/sd-scripts/issues/924

    2023. [Bug] Gradients not synchronized.https://github.com/kohya- ss/sd-scripts/issues/924

    2023

  14. [22]

    DDP: moving model to CPU and back to GPU breaks gradient synchronization.https://github.com/pytorch/pytorch/issues/104336

    2023. DDP: moving model to CPU and back to GPU breaks gradient synchronization.https://github.com/pytorch/pytorch/issues/104336

    2023

  15. [23]

    CUDA Toolkit.https://developer.nvidia.com/cuda- toolkit

    Accessed 2025. CUDA Toolkit.https://developer.nvidia.com/cuda- toolkit

    2025

  16. [24]

    NeuronX Distributed (NxD).https://awsdocs- neuron.readthedocs-hosted.com/en/latest/libraries/neuronx- distributed/index.html

    Accessed 2025. NeuronX Distributed (NxD).https://awsdocs- neuron.readthedocs-hosted.com/en/latest/libraries/neuronx- distributed/index.html

    2025

  17. [25]

    PyTorch.https://pytorch.org/

    Accessed 2025. PyTorch.https://pytorch.org/

    2025

  18. [26]

    TensorFlow: An end-to-end platform for machine learning.https://www.tensorflow.org/

    Accessed 2025. TensorFlow: An end-to-end platform for machine learning.https://www.tensorflow.org/

    2025

  19. [27]

    Accessed2025.TransformersNeuron.https://github.com/aws-neuron/ transformers-neuronx

  20. [28]

    XLA (Accelerated Linear Algebra).https://openxla

    Accessed 2025. XLA (Accelerated Linear Algebra).https://openxla. org/xla

    2025

  21. [29]

    Saurabh Agarwal, Chengpo Yan, Ziyi Zhang, and Shivaram Venkatara- man. 2023. Bagpipe: Accelerating Deep Recommendation Model Training. InProceedings of the 29th Symposium on Operating Sys- tems Principles(Koblenz, Germany)(SOSP ’23). Association for Computing Machinery, New Yo...

    2023

  22. [30]

    Jai Arora, Sirui Lu, Devansh Jain, Tianfan Xu, Farzin Houshmand, PhitchayaMangpoPhothilimthana,MohsenLesani,PraveenNarayanan, Karthik Srinivasa Murthy, Rastislav Bodik, Amit Sabne, and Charith Mendis. 2025. TensorRight: Automated Verification of Tensor Graph Rewrites.Proc. ACM...

    2025 doi

  23. [31]

    Sanjith Athlur, Nitika Saran, Muthian Sivathanu, Ramachandran Ram- jee, and Nipun Kwatra. 2022. Varuna: scalable, low-cost training of massive deep learning models. InProceedings of the Seventeenth Euro- peanConferenceonComputerSystems(Rennes,France)(EuroSys’22). Association f...

    2022

  24. [32]

    Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffr...

    2020

  25. [33]

    Tianqi Chen, Thierry Moreau, Ziheng Jiang, Lianmin Zheng, Eddie Yan, Haichen Shen, Meghan Cowan, Leyuan Wang, Yuwei Hu, Luis Ceze, Carlos Guestrin, and Arvind Krishnamurthy. 2018. TVM: An AutomatedEnd-to-EndOptimizingCompilerforDeepLearning.In13th USENIXSymposiumonOperatingSys...

    2018

  26. [34]

    Arnab Choudhury, Yang Wang, Tuomas Pelkonen, Kutta Srini- vasan, Abha Jain, Shenghao Lin, Delia David, Siavash Soleimanifard, Michael Chen, Abhishek Yadav, Ritesh Tijoriwala, Denis Samoylov, and Chunqiang Tang. 2024. MAST: Global Scheduling of ML Training across Geo-Distribute...

    2024

  27. [35]

    Lim, and Santosh Nagarakatte

    Sangeeta Chowdhary, Jay P. Lim, and Santosh Nagarakatte. 2020. Debugging and detecting numerical errors in computation with posits. InProceedingsofthe41stACMSIGPLANConferenceonProgramming Language Design and Implementation(London, UK)(PLDI 2020). Association for Computing Mach...

    2020

  28. [36]

    Basile Clément and Albert Cohen. 2022. End-to-end translation valida- tion for the halide language.Proc. ACM Program. Lang.6, OOPSLA1, Article 84 (April 2022), 30 pages.https://doi.org/10.1145/3527328

    2022 doi

  29. [37]

    Yaoyao Ding, Cody Hao Yu, Bojian Zheng, Yizhi Liu, Yida Wang, and Gennady Pekhimenko. 2023. Hidet: Task-Mapping Programming Paradigm for Deep Learning Tensor Programs. InProceedings of the 28th ACM International Conference on Architectural Support for ProgrammingLanguagesandOp...

    2023 doi

  30. [38]

    Charis Eleftheriadis, Nikolaos Kekatos, Panagiotis Katsaros, and Stavros Tripakis. 2022. On Neural Network Equivalence Checking using SMT Solvers. arXiv:2203.11629 [cs.AI]https://arxiv.org/abs/ 2203.11629

    2022 arXiv

  31. [39]

    ChengFu,HanxianHuang,BramWasti,ChrisCummins,RiyadhBagh- dadi, Kim Hazelwood, Yuandong Tian, Jishen Zhao, and Hugh Leather

  32. [40]

    Hao Guan, Ying Xiao, Jiaying Li, Yepang Liu, and Guangdong Bai

  33. [41]

    Gunawi, Mingzhe Hao, Riza O

    Haryadi S. Gunawi, Mingzhe Hao, Riza O. Suminto, Agung Laksono, Anang D. Satria, Jeffry Adityatama, and Kurnia J. Eliazar. 2016. Why Does the Cloud Stop Computing?: Lessons from Hundreds of Service Outages. InProceedings of the 7th ACM Symposium on Cloud Computing (SoCC)(Santa...

    2016

  34. [42]

    InProceedings of the 45th International Conference on Software Engineering(Melbourne, Victoria, Australia) (ICSE ’23)

    A Comprehensive Study of Real-World Bugs in Machine Learn- ing Model Optimization. InProceedings of the 45th International Conference on Software Engineering(Melbourne, Victoria, Australia) (ICSE ’23). IEEE Press, 147–158.https://doi.org/10.1109/ICSE48619. 2023.00024

  35. [43]

    Guoliang He, Zak Singh, and Eiko Yoneki. 2023. MCTS-GEB: Monte Carlo Tree Search is a Good E-graph Builder. InProceedings of the 3rd Workshop on Machine Learning and Systems(Rome, Italy) (EuroMLSys ’23). Association for Computing Machinery, New York, NY, USA, 26–33.https://doi...

    2023

  36. [44]

    Jakob Hartmann, Guoliang He, and Eiko Yoneki. 2024. Optimizing Tensor Computation Graphs with Equality Saturation and Monte Carlo Tree Search. InProceedings of the 2024 International Conference on Parallel Architectures and Compilation Techniques(Long Beach, CA, USA)(PACT ’24)...

    2024

  37. [45]

    PengHuang,ChuanxiongGuo,LidongZhou,JacobR.Lorch,Yingnong Dang, Murali Chintalapati, and Randolph Yao. 2017. Gray Failure: The Achilles’ Heel of Cloud-Scale Systems. InProceedings of the 16th Workshop on Hot Topics in Operating Systems (HotOS XVI). ACM, British Columbia, Canada, 7

    2017

  38. [46]

    Pollard, Nadesh Ramanathan, and John Wickerson

    Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. 2021. Formal verification of high-level synthesis.Proc. ACM Program. Lang.5, OOPSLA, Article 117 (Oct. 2021), 30 pages. https://doi.org/10.1145/3485494

    2021 doi

  39. [47]

    Jang, Zhenning Yang, Zhen Zhang, Xin Jin, and Mosharaf Chowdhury. [n.d.]. Resilient Distributed Training of Large Models Using Pipeline Templates(SOSP ’23)

  40. [48]

    Le, Yonghui Wu,andZhifengChen.2019

    YanpingHuang,YoulongCheng,AnkurBapna,OrhanFirat,MiaChen, Dehao Chen, HyoukJoong Lee, Jiquan Ngiam, Quoc V. Le, Yonghui Wu,andZhifengChen.2019. GPipe:EfficientTrainingofGiantNeural Networks using Pipeline Parallelism.https://arxiv.org/pdf/1811.06965

    2019 arXiv

  41. [49]

    Zhihao Jia, James Thomas, Todd Warszawski, Mingyu Gao, Matei Zaharia, and Alex Aiken. 2019. Optimizing DNN computation with relaxed graph substitutions.Proceedings of Machine Learning and Systems1 (2019), 27–39

    2019

  42. [50]

    Zhihao Jia, Oded Padon, James Thomas, Todd Warszawski, Matei Za- haria,andAlexAiken.2019. TASO:optimizingdeeplearningcomputa- tionwithautomaticgenerationofgraphsubstitutions.InProceedingsof the27thACMSymposiumonOperatingSystemsPrinciples(Huntsville, Ontario, Canada)(SOSP ’19)....

    2019

  43. [51]

    Wookeun Jung, Thanh Tuan Dao, and Jaejin Lee. 2021. DeepCuts: a deep learning optimization framework for versatile GPU workloads. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation(Virtual, Canada) (PLDI 2021). Ass...

    2021

  44. [52]

    TrainingwithConfidence:CatchingSilentErrorsinDeep Learning Training with Automated Proactive Checks

    YuxuanJiang,ZimingZhou,BoyuXu,BeijieLiu,RunhuiXu,andPeng Huang.2025. TrainingwithConfidence:CatchingSilentErrorsinDeep Learning Training with Automated Proactive Checks. InProceedings of the 19th USENIX Symposium on Operating Systems Design and Implementation(OSDI’25).USENIXAs...

    2025

  45. [53]

    Liu, Jinkun Lin, Fabian Ruffy, Cheng Tan, Jinyang Li, Aurojit Panda, and Lingming Zhang. [n.d.]. Generating Diverse and Valid Test Cases for Deep Learning Compilers(ASPLOS ’23)

  46. [54]

    Transformersinvision: A survey.ACM computing surveys (CSUR)54, 10s (2022), 1–41

    Salman Khan, Muzammal Naseer, Munawar Hayat, Syed Waqas Zamir, FahadShahbazKhan,andMubarakShah.2022. Transformersinvision: A survey.ACM computing surveys (CSUR)54, 10s (2022), 1–41

    2022

  47. [55]

    JiaweiLiu,YuxiangWei,SenYang,YinlinDeng,andLingmingZhang

  48. [56]

    Amanda Liu, Gilbert Bernstein, Adam Chlipala, and Jonathan Ragan- Kelley. 2024. A Verified Compiler for a Functional Tensor Language. Proc.ACMProgram.Lang.8,PLDI,Article160(June2024),23pages. https://doi.org/10.1145/3656390

    2024 doi

  49. [57]

    InProceedings of the 19th USENIX Symposium on Operating Systems Design and Implementation (OSDI ’25)

    Chang Lou, Dimas Shidqi Parikesit, Yujin Huang, Zhewen Yang, Senapati Diwangkara, Yuzhuo Jing, Achmad Imam Kistijantoro, Ding Yuan,SumanNath,andPengHuang.2025.DerivingSemanticCheckers from Tests to Detect Silent Failures in Production Distributed Systems. InProceedings of the ...

    2025

  50. [58]

    Yunchi Lu, Youshan Miao, Cheng Tan, Peng Huang, Yi Zhu, Xian Zhang, and Fan Yang. 2025. TrainVerify: Equivalence-Based Verifi- cation for Distributed LLM Training. SOSP ’25 (to appear). Preprint available athttps://arxiv.org/abs/2506.15961. 13

    2025 arXiv

  51. [59]

    Chang Lou, Yuzhuo Jing, and Peng Huang. 2022. Demystifying and Checking Silent Semantic Violations in Large Distributed Systems. In Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI ’22). USENIX Association, Carls- bad, CA, USA, 91–1...

    2022

  52. [60]

    Jayashree Mohan, Amar Phanishayee, and Vijay Chidambaram. 2021. CheckFreq: Frequent, Fine-Grained DNN Checkpointing. In19th USENIX Conference on File and Storage Technologies (FAST 21). USENIX Association, 203–216.https://www.usenix.org/conference/ fast21/presentation/mohan

    2021

  53. [61]

    Chandrakana Nandi, Max Willsey, Amy Zhu, Yisu Remy Wang, Brett Saiki, Adam Anderson, Adriana Schulz, Dan Grossman, and Zachary Tatlock. 2021. Rewrite rule inference using equality saturation.Proc. ACM Program. Lang.5, OOPSLA, Article 119 (Oct. 2021), 28 pages. https://doi.org/...

    2021 doi

  54. [62]

    DongningMa,FredLin,AlbanDesmaison,JoelCoburn,DanielMoore, Sriram Sankar, and Xun Jiao. 2024. Dr. DNA: Combating Silent Data Corruptions in Deep Learning using Distribution of Neuron Activations. InProceedings of the 29th ACM International Conference on Architectural Support fo...

    2024

  55. [63]

    Kexin Pei, Yinzhi Cao, Junfeng Yang, and Suman Jana. 2017. Deep- Xplore: Automated Whitebox Testing of Deep Learning Systems. In Proceedings of the 26th Symposium on Operating Systems Principles (Shanghai, China)(SOSP ’17). Association for Computing Machinery, New York, NY, US...

    2017

  56. [64]

    Hung Viet Pham, Thibaud Lutellier, Weizhen Qi, and Lin Tan. 2019. CRADLE: Cross-Backend Validation to Detect and Localize Bugs in Deep Learning Libraries. In2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE). 1027–1038.https: //doi.org/10.1109/ICSE.2019.00107

    2019

  57. [65]

    Anjali Pal, Brett Saiki, Ryan Tjoa, Cynthia Richey, Amy Zhu, Oliver Flatt, Max Willsey, Zachary Tatlock, and Chandrakana Nandi. 2023. EqualitySaturationTheoryExplorationàlaCarte.Proc.ACMProgram. Lang.7, OOPSLA2, Article 258 (Oct. 2023), 29 pages.https://doi. org/10.1145/3622834

    2023 doi

  58. [66]

    Louis-NoëlPouchet,EmilyTucker,NiansongZhang,HongzhengChen, Debjit Pal, Gabriel Rodríguez, and Zhiru Zhang. 2024. Formal Ver- ification of Source-to-Source Transformations for HLS. InProceed- ings of the 2024 ACM/SIGDA International Symposium on Field Programmable Gate Arrays(M...

    2024

  59. [67]

    Yiming Qiu, Patrick Tser Jern Kon, Ryan Beckett, and Ang Chen

  60. [68]

    Jacques Arnaud Pienaar, Mangpo Phothilimthana, Max Willsey, Remy Wang, Sudip Roy, and Yichen Yang. 2021. Equality Saturation for Tensor Graph Superoptimization. InMLSys

    2021

  61. [69]

    QingchaoShen,HaoyangMa,JunjieChen,YongqiangTian,Shing-Chi Cheung, and Xiang Chen. 2021. A comprehensive study of deep learning compiler bugs. InProceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software En...

    2021

  62. [70]

    Mohammad Shoeybi, Mostofa Patwary, Raul Puri, Patrick LeGresley, Jared Casper, and Bryan Catanzaro. 2020. Megatron-LM: Training Multi-Billion Parameter Language Models Using Model Parallelism. arXiv:1909.08053 [cs.CL]https://arxiv.org/abs/1909.08053

    2020 arXiv

  63. [71]

    Florian Tambon,Amin Nikanjam, LeAn, Foutse Khomh,and Giuliano Antoniol. 2021. Silent Bugs in Deep Learning Frameworks: An Empirical Study of Keras and TensorFlow.CoRRabs/2112.13314 (2021). arXiv:2112.13314https://arxiv.org/abs/2112.13314

    2021 arXiv

  64. [72]

    Meta AI Research. 2023. LLaMA 3.1: Enhanced Capabilities in Large Language Modeling.https://ai.meta.com/llama. Version 3.1

    2023

  65. [73]

    DeepSeek Team. 2023. DeepSeek v3: A Next-Generation Deep Learn- ing Search Engine.https://www.deepseek.ai. Version 3

    2023

  66. [74]

    John Thorpe, Pengzhan Zhao, Jonathan Eyolfson, Yifan Qiao, Zhihao Jia, Minjia Zhang, Ravi Netravali, and Guoqing Harry Xu. 2023. Bam- boo:MakingPreemptibleInstancesResilientforAffordableTrainingof LargeDNNs.In20thUSENIXSymposiumonNetworkedSystemsDesign and Implementation (NSDI...

    2023

  67. [75]

    DeepTest: automated testing of deep-neural-network-driven autonomous cars

    YuchiTian,KexinPei,SumanJana,andBaishakhiRay.2018. DeepTest: automated testing of deep-neural-network-driven autonomous cars. In Proceedings of the 40th International Conference on Software Engi- neering(Gothenburg, Sweden)(ICSE ’18). Association for Computing Machinery, New Y...

    2018

  68. [76]

    Equality saturation: a new approach to optimization(POPL ’09)

    Tate,MichaelStepp,ZacharyTatlock,andSorinLerner.[n.d.]. Equality saturation: a new approach to optimization(POPL ’09)

  69. [77]

    Verdoolaege, Gerda Janssens, and Maurice Bruynooghe. [n.d.]. Equiv- alence checking of static affine programs using widening to handle recurrences(TOPLAS ’12)

  70. [78]

    Wang,ZhenJia,ShuaiZheng,ZhenZhang,XinweiFu,T.S.EugeneNg, and Yida Wang. [n.d.]. Fast Failure Recovery in Distributed Training with In-Memory Checkpoints(SOSP ’23)

  71. [79]

    Haoyu Wang, Junjie Chen, Chuyue Xie, Shuang Liu, Zan Wang, Qingchao Shen, and Yingquan Zhao. 2023. MLIRSmith: Random Program Generation for Fuzzing MLIR Compiler Infrastructure. In 202338thIEEE/ACMInternationalConferenceonAutomatedSoftware Engineering (ASE). 1555–1566.https://...

    2023

  72. [80]

    Colin Unger, Zhihao Jia, Wei Wu, Sina Lin, Mandeep Baines, Carlos Efrain Quintero Narvaez, Vinay Ramakrishnaiah, Nirmal Prajapati, Pat McCormick, Jamaludin Mohd-Yusof, Xi Luo, Dhee- vatsa Mudigere, Jongsoo Park, Misha Smelyanskiy, and Alex Aiken

  73. [81]

    In16th USENIX Symposium on Operating Systems Design and Implemen- tation (OSDI 22)

    Unity: Accelerating DNN Training Through Joint Opti- mization of Algebraic Transformations and Parallelization. In16th USENIX Symposium on Operating Systems Design and Implemen- tation (OSDI 22). USENIX Association, Carlsbad, CA, 267–284. https://www.usenix.org/conference/osdi...

  74. [82]

    Shaobu Wang, Guangyan Zhang, Junyu Wei, Yang Wang, Jiesheng Wu, and Qingchao Luo. [n.d.]. Understanding Silent Data Corruptions in a Large Production CPU Population(SOSP ’23)

  75. [83]

    Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. egg: Fast and extensible equality saturation.Proc. ACM Program. Lang.5, POPL, Article 23 (Jan. 2021), 29 pages.https://doi.org/10.1145/3434304

    2021 doi

  76. [84]

    Mengdi Wu, Xinhao Cheng, Shengyu Liu, Chunan Shi, Jianan Ji, Kit Ao, Praveen Velliengiri, Xupeng Miao, Oded Padon, and Zhihao Jia

  77. [85]

    Haojie Wang, Jidong Zhai, Mingyu Gao, Zixuan Ma, Shizhi Tang, Liyan Zheng, Yuanzhi Li, Kaiyuan Rong, Yuanyong Chen, and Zhihao Jia. 2021. PET: Optimizing Tensor Programs with Partially Equivalent Transformations and Automated Corrections. In15th USENIX Sym- posium on Operating...

    2021

  78. [86]

    Jiannan Wang, Thibaud Lutellier, Shangshu Qian, Hung Viet Pham, and Lin Tan. 2022. EAGLE: creating equivalent graphs to test deep learning libraries. InProceedings of the 44th International Conference on Software Engineering(Pittsburgh, Pennsylvania)(ICSE ’22). As- sociation f...

    2022

  79. [87]

    Alpa:Automat- ing Inter- and Intra-Operator Parallelism for Distributed Deep Learn- ing

    Lianmin Zheng, Zhuohan Li, Hao Zhang, Yonghao Zhuang, Zhifeng Chen, Yanping Huang, Yida Wang, Yuanzhong Xu, Danyang Zhuo, EricP.Xing,JosephE.Gonzalez,andIonStoica.2022. Alpa:Automat- ing Inter- and Intra-Operator Parallelism for Distributed Deep Learn- ing. In16th USENIX Sympo...

    2022

  80. [88]

    Chijin Zhou, Bingzhou Qian, Gwihwan Go, Quan Zhang, Shanshan Li, and Yu Jiang. 2024. PolyJuice: Detecting Mis-compilation Bugs in Tensor Compilers with Equality Saturation Based Rewriting.Proc. ACM Program. Lang.8, OOPSLA2, Article 317 (Oct. 2024), 27 pages. https://doi.org/10...

    2024 doi

  81. [90]

    arXiv:2405.05751 [cs.LG]https://arxiv.org/abs/2405.05751 14

    Mirage: A Multi-Level Superoptimizer for Tensor Programs. arXiv:2405.05751 [cs.LG]https://arxiv.org/abs/2405.05751 14

    arXiv

  82. [91]

    XiaofeiXie,LeiMa,HaijunWang,YuekangLi,YangLiu,andXiaohong Li. 2019. DiffChaser: Detecting Disagreements for Deep Neural Networks. InProceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI-19. International Joint ConferencesonArtificial...

    2019 doi

  83. [92]

    Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey. 2023. Better Together: Unifying Datalog and Equality Saturation.Proc. ACM Program. Lang.7, PLDI, Article 125 (June 2023), 25 pages.https: //doi.org/10.1145/3591239

    2023 doi

  84. [2022]

    ACM Program

    Coverage-guided tensor compiler fuzzing with joint IR-pass mutation.Proc. ACM Program. Lang.6, OOPSLA1, Article 73 (April 2022), 26 pages.https://doi.org/10.1145/3527317

    2022 doi

  85. [2023]

    Q-gym: An Equality Saturation Framework for DNN Inference Exploiting Weight Repetition. InProceedings of the International Con- ferenceonParallelArchitecturesandCompilationTechniques(Chicago, Illinois)(PACT’22).AssociationforComputingMachinery,NewYork, NY, USA, 291–303.https:/...

  86. [2024]

    InProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles(Austin, TX, USA)(SOSP ’24)

    Unearthing Semantic Checks for Cloud Infrastructure-as-Code Programs. InProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles(Austin, TX, USA)(SOSP ’24). Asso- ciation for Computing Machinery, New York, NY, USA, 574–589. https://doi.org/10.1145/3694715.3695974

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.