Pith. sign in

REVIEW 3 major objections 5 minor 1 cited by

TrainVerify: Equivalence-Based Verification for Distributed LLM Training

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 TrainVerify claims to be the first system to formally verify that a distributed LLM execution plan is mathematically equivalent to the model's logical definition, scaling to Llama3-405B and DeepSeek-V3-671B.

desk verdict Nice systems idea, but the shape-reduction soundness proof is false, so the 'provably correct' claim does not stand; worth refereeing as a systems paper, not as a formal-methods result. read the letter →

arxiv 2506.15961 v2 pith:6GKIUJ46 submitted 2025-06-19 cs.DC cs.AIcs.LG

Yunchi Lu , Youshan Miao , Cheng Tan , Peng Huang , Yi Zhu , Xian Zhang , Fan Yang This is my paper · ORCID
classification cs.DCcs.AIcs.LG
keywords distributedtrainingparallelizationequivalenceformalverificationsymbolicdataflowgraphshapereductionstagedSMTsolverLLM
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

TrainVerify claims that the correctness of distributed deep learning training can be verified by checking that a parallelized execution plan is mathematically equivalent to the model's logical definition. It introduces symbolic dataflow graphs, a shape-reduction technique that shrinks tensor sizes while preserving the equivalence question, and a stage-wise parallel verification algorithm that decomposes the end-to-end check. The paper reports that this approach verifies real execution plans for Llama3-405B and DeepSeek-V3-671B without running the training at full scale, and it claims to be the first system to offer provably correct execution plans for distributed training.

What carries the argument

The load-bearing machinery is the shape-reduction theorem, Theorem C.12: for SIMD functions composed from LLM operators, equality at a single output element for every input implies equality at all output elements. The proof chains two relations: kernel permutation-set equivalence ($\theta_f \sim_Q \theta_g$, kernels agree up to a permutation of arguments) and mapping permutation equivalence ($\tau_f \sim_P \tau_g$, linear dependency maps agree up to a permutation), which together give full equality by Lemma C.9. Complementing this, staged verification partitions the logical and parallelized graphs so that each stage's input-output equivalence is checked concurrently and then chained into an end-to-end proof.

What would settle it

Feed TrainVerify two SIMD functions that agree at one output position for all inputs but differ elsewhere, such as $f(x) = [x_0, x_0]$ and $g(x) = [x_0, x_1]$, and check whether it reports full equivalence.

Watch

Extended reading notes

Core claim

TrainVerify's central claim is that parallelization equivalence can be formally proven: for every admissible input, a distributed execution plan produces exactly the output of the original logical model, with both represented as dataflow graphs over symbolic reals. The proof rests on showing that the operators in transformer stacks are SIMD functions whose dependency mappings are linear index maps, which permits shape reduction, and on showing that stages of the dual graphs can be verified separately and composed. If successful, the method eliminates entire categories of silent parallelization bugs, including missing communication, wrong rank assignment, and incorrect gradient scaling, at scales up to DeepSeek-V3 (671B parameters) and Llama3-405B.

Load-bearing premise

The load-bearing premise is that equivalence verified on a reduced-shape graph, by checking a single output element, carries over to the original full-size graphs.

Editorial extensions

If this is right

  • Any execution plan that passes verification is functionally indistinguishable from the logical model, so the major silent-error classes in communication, partitioning, and scaling are provably absent from the plan.
  • Verification cost is independent of original tensor shapes and scales roughly linearly with parallelism degree, so verifying a 671B-parameter plan takes hours, not weeks of training.
  • The method plugs into graph-based parallelization frameworks that expose lineage, meaning existing training stacks can adopt it without rewriting the whole stack.
  • Because verification works symbolically over real arithmetic, it is immune to the floating-point drift that makes differential testing of parallel training unreliable.

Reading between the lines

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

  • If Theorem C.12 is sound, the single-index check becomes a general certificate for SIMD program rewrites, potentially applicable to verifying inference serving plans, model compression transforms, and tensor compiler optimizations beyond training.
  • The staging machinery could be reused to certify each plan a planner generates, turning fast but heuristic parallelization search into a pipeline that emits provably correct plans.
  • A stress test for the shape-reduction theorem is to apply it to broadcasts or reductions with non-bijective dependency mappings, where the linear-mapping assumption is most likely to fail.
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 TrainVerify, a system for verifying that a distributed execution plan for LLM training is functionally equivalent to the logical model definition. TrainVerify represents both the logical model and the parallelized plan as symbolic data flow graphs (sDFGs), uses lineage information to relate tensors across the two graphs, reduces tensor shapes to small representative dimensions, and partitions verification into stages solved in parallel with an SMT solver (Z3). The paper claims that reduced-shape verification provably extends to full-shape models, and reports successful verification of training plans for Llama3 (8B/70B/405B) and DeepSeek-V3 (16B/236B/671B) along with detection of 14 injected bug cases. The central formal claim is that parallelization equivalence can be verified at frontier scale while preserving formal correctness.

Significance. If the formal results were valid, this would be a substantial systems contribution: parallelization equivalence is a crisp and practically motivated correctness property, the lineage-based staged verification design is reasonable, and the scale of the reported evaluations is well beyond prior neural-network equivalence checkers. The paper also honestly documents several limitations, including manual shape-reduction rules and current support for only ZeRO Stage 1. However, the headline promise of provably correct execution plans rests on Theorem 6.9/C.12, which is false as stated. Since shape reduction is the mechanism that makes verification of 671B-parameter plans tractable, the formal guarantee that reduced-shape verification extends to full-size models is unsupported. The paper may still be of interest as an empirical systems study, but as written its central claim is not established.

major comments (3)
  1. [§6, Theorem 6.9; Appendix C, Theorem C.12] Theorem C.12 (and its main-text version Theorem 6.9) is false. The theorem asserts that if f and g agree at a single output index i for every input, then they agree at every output index for every input. This is not true even for SIMD functions with affine dependency mappings and well-formed kernels, all within the paper's definitions. For example, let f(x) = [x0+x1, x0+x1] and g(x) = [x0+x1, 2*x0]. Both are SIMD functions with the same kernel θ(a,b)=a+b and affine dependency mappings: τ_f(0)=τ_f(1)=[0,1]; τ_g(0)=[0,1], τ_g(1)=[0,0]. At index 0, f(x)[0]=g(x)[0] for all x, satisfying the precondition. At index 1, f(x)[1]=x0+x1 while g(x)[1]=2*x0, which differ at e.g. x0=0, x1=1. The precondition therefore does not imply full equivalence, and the soundness of shape reduction as stated in Section 5.2 is not established.
  2. [Appendix C, Theorem C.12, proof step 2] The proof step from the single-index precondition to global mapping permutation equivalence is invalid. The text says 'From the precondition, we can derive that ∃P, τ_f(i) ≡_P τ_g(i). By observation 2, we know that the P applies to all dimensions (i.e., τ_f ≡_P τ_g) due to the linear transformation.' This is a non-sequitur: two affine maps can agree at one point without being identical, and a permutation that works at one output index need not extend to all output indices. The counterexample in the previous comment satisfies Observation 2 (both dependency mappings are affine) and still violates the conclusion. The phrase 'due to the linear algebra' does not supply the missing argument, and no such argument appears elsewhere in the appendix.
  3. [§7, §4] The 'ground truth' logical model is not an independent specification: Section 7 states that the logical model is obtained by invoking nnScaler to emit a single-GPU execution plan, whose correctness is guaranteed by nnScaler, and the parallelized graph is also produced by nnScaler. Both graphs therefore share the same code path, lineage inference, and graph-construction logic. The paper acknowledges in Section 4 that the logical model is assumed correct, but the headline claim of 'provably correct execution plans' is broader than what this setup can establish: verification here checks consistency between two artifacts generated by the same framework, not conformance to an independent model definition.
minor comments (5)
  1. [§5.2, Algorithm 1; Appendix A] The optimization objective is described inconsistently: Algorithm 1 line 4 minimizes total tensor volume, while Appendix A says TrainVerify minimizes the L1 norm across input dimensions to avoid quadratic solving. The main text should state which objective is actually used.
  2. [§8.3] The 14 reproduced cases are author-mutated versions of known historical bugs rather than organically discovered failures; this is acceptable for a bug-injection study, but the claim that TrainVerify 'eliminates major classes of real-world parallelization bugs' would be better phrased as detecting representative injected instances of those classes.
  3. [Appendix C] The appendix contains several typos that should be fixed, including 'opreations', 'dimention reduction', and 'Consdier this x′' in the proof of Theorem C.12.
  4. [§8.1, Table 3] The end-to-end verification times for the largest models (L3, D3) are reported as single numbers without repeated runs or variance; given the acknowledged seed-dependent variance of Z3 in shape-reduction solving, a brief statement about run-to-run variability would strengthen the scalability claims.
  5. [Figure 7 caption] The caption reads 'The y-axes use alog2 scale'; this should be 'a log2 scale'.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation found; the verification chain is self-contained relative to its explicit logical-model assumption, though the shape-reduction proof has a serious correctness gap.

full rationale

The central derivation is not circular. TrainVerify's guarantee is explicitly conditional: the logical model is taken as the ground-truth specification, and parallelization equivalence is checked between the logical sDFG and the parallelized sDFG. The lineage information defines how partitioned tensors reconstruct the logical tensors, and the SMT solver checks the resulting algebraic identities; this is a self-contained equivalence argument, not a reduction of the conclusion to the premise. The fact that both graphs are emitted by nnScaler, with overlapping authors, and that the logical model's correctness is attributed to nnScaler, is a scoping assumption rather than a load-bearing derivation: even if the logical model were wrong, the equivalence proof itself would not be circular, only the external meaning of the guarantee would be weakened. The hand-mutated bug cases are evaluation artifacts, not inputs to the derivation. The most significant concern is a correctness gap, not circularity: Theorem C.12 asserts that agreement of two SIMD functions at a single output index for all inputs implies agreement at all output indices, and the proof step deriving global mapping-permutation equivalence 'due to the linear algebra' is mathematically invalid; two linear dependency mappings can agree at one index while disagreeing elsewhere (e.g., f(x)=[[1,1],[1,1]]x and g(x)=[[1,1],[2,0]]x agree at index 0 for all x but differ at index 1). This invalidates the claimed soundness of shape reduction as presented, but it is an unsound inference, not a circular one: the theorem's conclusion is not equivalent to its premise by construction. Therefore, the appropriate finding under the circularity rubric is no significant circularity.

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

No free parameters are fitted to data; the system's knobs (e.g., max fork, Z3 seed) are implementation choices. The axioms above are the load-bearing premises for the formal correctness claim. No new physical or mathematical entities are postulated; lineage, sDFGs, and stages are computational representations, not entities with independent empirical handles.

assumptions (5)
  • domain assumption The logical model emitted by nnScaler is the correct specification.
    Section 4 says 'TrainVerify treats the logical model as the specification and assumes it represents the desired semantics.' The logical graph is a single-device plan generated by nnScaler, whose correctness is asserted but not independently verified.
  • ad hoc to paper All LLM operators under verification are SIMD functions with dependency mappings expressible as linear combinations.
    Section 6, Observations 1 and 2. This is needed for the shape-reduction proof. The paper itself acknowledges non-SIMD operators (embedding, topK) are handled by special-casing, and masking is deferred to an appendix.
  • domain assumption Kernel functions are well-formed: every input element influences the output.
    Definition C.8. Required for Lemma C.9. It is unclear whether this holds for dropout or stochastic operators in training.
  • ad hoc to paper User-configured approximation overrides preserve the meaning of verification.
    Section 5.3: when approximations such as local BatchNorm or restricted MoE routing are allowed, TrainVerify overrides them with strict-equivalence versions. The verified plan is then not the actually executed plan.
  • domain assumption Correctness of nnScaler's single-device execution plan.
    Section 7 states the logical model is obtained by invoking nnScaler to emit a single-GPU execution plan, 'whose correctness is guaranteed by nnScaler' without independent formalization.

how reviews work

0 comments
Cite this review

Pith. "Pith review of TrainVerify: Equivalence-Based Verification for Distributed LLM Training." pith.science (2026). https://pith.science/paper/6GKIUJ46

@misc{pith2026250615961,
  author       = {Pith},
  title        = {Pith review of: TrainVerify: Equivalence-Based Verification for Distributed LLM Training},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/6GKIUJ46}},
  note         = {Machine review of arXiv:2506.15961}
}
read the original abstract

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.

Figures

Figures reproduced from arXiv: 2506.15961 by the authors.

Figure 3
Figure 3. TrainVerify System Overview. Similarly, incorrect primitives may be introduced, e.g., AllGather. All those cases will violate 𝐸3. • Incorrect communication group. For example, get_model _tp_group may be mistakenly assigned as a global group at 4 , i.e., (0,1,2,3). They will also violate 𝐸3. 4 Overview of TrainVerify To realize our verification methodology for DNN models in practice, we develop TrainVerify, a system … view at source ↗
Figure 2
Figure 2. Logical and parallelized data flow graphs (simplified) for [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 4
Figure 4. Lineage of tensors. and the computation is performed element-wise using sym￾bolic expressions. This formulation allows the output tensor to be represented as an algebraic expression over the input ten￾sors through symbolic operations. By recursively substituting input tensors with their corresponding symbolic expressions, one can compose consecutive operators—ultimately construct an algebraic expression representing… view at source ↗
Figures from the paper (6 more)
Figure 5
Figure 5. Figure 5: DNN operator MatMul: different output elements 𝑐1,1 and 𝑐2,2 are calculated using the same function but on different inputs. Therefore, verification may be performed on the same sDFG with only tensors’ shape reduced, omitting redundant elements without compromising the…
Figure 6
Figure 6. Figure 6: Implementation Overview. not natively supported. The modular design of stage checker also facilitates switching between symbolic engines—e.g., SymPy [53] or Gurobi [8]—to support operator rewriting and solver-specific optimizations. Accelerating Solving. To enable prac…
Figure 7
Figure 7. Figure 7: TrainVerify’s performance trends regarding different training configurations. The y-axes use a log2 scale. Bars indicate the time breakdown by component, while lines represent the end-to-end verification time. Exp. ID Model Layers DP TP PP NM L1 Llama3-8B 32 512 1 1 1 …
Figure 8
Figure 8. Figure 8: Verification time with vs. without stage parallelism. stages and time, as shown in Figure 7g. For data parallelism, microbatching, and tensor parallelism, the verification time grows linearly due to increased tensor copies proportional to the parallelism degree, along …
Figure 9
Figure 9. Figure 9: Reproduced incorrect parallelization cases. covering the broad categories in §8.3, as shown in [PITH_FULL_IMAGE:figures/full_fig_p012_9.png]
Figure 10
Figure 10. Figure 10: Gradient finalization under 2-way context parallelism. For simplicity, the producer flow for total_n_token is omitted. B.1 Case Study We highlight a representative case derived from the Megatron￾673 issue [18] to illustrate the subtlety of parallelization bugs and how…

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Verifying Computational Graphs in Production-Grade Distributed Machine Learning Frameworks

    cs.LG 2025-09 conditional novelty 7.0 of 10

    Scalify verifies semantic equivalence of baseline and distributed ML computational graphs using equality saturation and relational reasoning, finding real silent errors in production frameworks.

Reference graph

Works this paper leans on

77 extracted references · 56 canonical work pages · cited by 1 Pith paper

  1. [1]

    https://docs.nvidia.com/cuda/

    CUDA. https://docs.nvidia.com/cuda/

    work page

  2. [2]

    CUTLASS: CUDA Templates for Linear Algebra Subroutines.https: //github.com/NVIDIA/cutlass

    work page

  3. [3]

    https://github.com/microsoft/DeepSpeed/commit/a85b6e472534d2e 0b61fe234fae4f6a2332c95bf

    DeepSpeed: fix bug where ZeRO2 never uses the reduce method. https://github.com/microsoft/DeepSpeed/commit/a85b6e472534d2e 0b61fe234fae4f6a2332c95bf

    work page

  4. [4]

    DeepSpeed: fix EP grad_scale/grad_norm fix.https://github.com/mic rosoft/DeepSpeed/commit/e5dd5501c10227ae33dce7d5bdd897741dd 3adb7

    work page

  5. [5]

    DeepSpeed: partition balanced return wrong result.https://github.com /deepspeedai/DeepSpeed/commit/2bdf061f4dc8be70878f032d2e48 d2130514f991

    work page

  6. [6]

    Distributed Data Parallelism.https://pytorch.org/docs/stable/notes/ ddp.html

    work page

  7. [7]

    A gentle introduction to torch.autograd.https://pytorch.org/tutorials/ beginner/blitz/autograd_tutorial.html#computational-graph

    work page

  8. [9]

    Llama3: Model Details.https://github.com/meta-llama/llama3/blob/ main/MODEL_CARD.md

    work page

Show all 77 references
  1. [10]

    Megatron Core.https://developer.nvidia.com/megatron-core

  2. [11]

    Megatron: fix cross entropy loss averaging.https://github.com/NVIDI A/Megatron-LM/commit/adfa873d965b240962be6539cb5d387c5084 16b9

  3. [12]

    https://github.com/NVIDIA/Megatron-LM/commit/32bbb76d5767fd bf8dc60d4ef07d103cef8aca02

    Megatron: fix distopt allgathers with interleaved pipeline parallelism. https://github.com/NVIDIA/Megatron-LM/commit/32bbb76d5767fd bf8dc60d4ef07d103cef8aca02

  4. [13]

    https://github.com/N VIDIA/Megatron-LM/commit/9ad1944db1f97000377dc5aee36dcd65 6b1ae4a2

    Megatron: fix𝑔𝑒𝑡_𝑑𝑎𝑡𝑎_𝑝𝑎𝑟𝑎𝑙𝑙𝑒𝑙 _𝑠𝑟𝑐_𝑟𝑎𝑛𝑘. https://github.com/N VIDIA/Megatron-LM/commit/9ad1944db1f97000377dc5aee36dcd65 6b1ae4a2

  5. [14]

    https://github.com/NVIDIA/Megatron-LM/commit/6bd7 4b0e84577317c06c303f4dae26d249ab55d1#diff-c27f9f2765a43b5c78 1756ce9fe4b9abcc3618ec96157f5dc67c4a00a7900b73R777

    Megatron: fix interleaved schedule with sequence-parallel and overlap- p2p-comm. https://github.com/NVIDIA/Megatron-LM/commit/6bd7 4b0e84577317c06c303f4dae26d249ab55d1#diff-c27f9f2765a43b5c78 1756ce9fe4b9abcc3618ec96157f5dc67c4a00a7900b73R777

  6. [15]

    Megatron: fix no-interleave pipeline schedule.https://github.com/NVI DIA/Megatron-LM/commit/1f387c2cbdb4ce93f0c885862d570efb66 dca4a4

  7. [16]

    Megatron: fix scaling down expert grads.https://github.com/NVIDIA/ Megatron-LM/commit/3373641ff1093073181e219265e8c8ee58d858 7c

  8. [17]

    Megatron: fix tiling, use correct input size for splits.https://github.c om/microsoft/DeepSpeed/commit/c543a41b154a991d50cb6cc8c07db f46b0d2bdf6

  9. [18]

    https://github.com/NVIDIA/Megatron-LM/issues/673

    Megatron issue: Incorrect loss scaling in context parallel code logic. https://github.com/NVIDIA/Megatron-LM/issues/673

  10. [19]

    Megatron: LinearWithFrozenWeight backward fix when TP > 1.https: //github.com/NVIDIA/Megatron-LM/commit/5fffdfc737f14297bc378 1dfc9e273199d1df52e

  11. [20]

    https: //github.com/deepspeedai/DeepSpeed/issues/6714

    Megatron:MoEdistributedsetupinvokesunnecessaryall-reduce. https: //github.com/deepspeedai/DeepSpeed/issues/6714

  12. [21]

    https://numpy.org/

    NumPy. https://numpy.org/. 13

  13. [22]

    NVIDIA collective communications library.https://developer.nvidia.c om/nccl

  14. [23]

    PyTorch: Loss Functions.https://pytorch.org/docs/stable/nn.html#lo ss-functions

  15. [24]

    Z3 Tactic Online Guide.https://microsoft.github.io/z3guide/docs/str ategies/tactics/

  16. [25]

    Gpt-4 technical report.arXiv preprint arXiv:2303.08774, 2023

    Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. Gpt-4 technical report.arXiv preprint arXiv:2303.08774, 2023

    2023 arXiv

  17. [26]

    Gemini: A family of highly capable multimodal models

    Rohan Anil, Sebastian Borgeaud, Yonghui Wu, Jean-Baptiste Alayrac, JiahuiYu,RaduSoricut,JohanSchalkwyk,AndrewMDai,AnjaHauth, Katie Millican, et al. Gemini: A family of highly capable multimodal models. arXiv preprint arXiv:2312.11805, 1, 2023

    2023 arXiv

  18. [27]

    Tensorright: Auto- mated verification of tensor graph rewrites

    Jai Arora, Sirui Lu, Devansh Jain, Tianfan Xu, Farzin Houshmand, PhitchayaMangpoPhothilimthana,MohsenLesani,PraveenNarayanan, Karthik Srinivasa Murthy, Rastislav Bodik, et al. Tensorright: Auto- mated verification of tensor graph rewrites. InProceedings of the 52nd ACM SIGPLAN...

    2025

  19. [28]

    Automaticdifferentiationinmachinelearning: a survey.Journal of machine learning research, 18(153):1–43, 2018

    Atilim Gunes Baydin, Barak A Pearlmutter, Alexey Andreyevich Radul, andJeffreyMarkSiskind. Automaticdifferentiationinmachinelearning: a survey.Journal of machine learning research, 18(153):1–43, 2018

    2018

  20. [29]

    Maximizing parallelism in distributed training for huge neural networks.arXiv preprint arXiv:2105.14450, 2021

    Zhengda Bian, Qifan Xu, Boxiang Wang, and Yang You. Maximizing parallelism in distributed training for huge neural networks.arXiv preprint arXiv:2105.14450, 2021

    2021 arXiv

  21. [30]

    Language models are few-shot learners

    Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. Language models are few-shot learners. Advances in neural information processing systems, 2020

    2020

  22. [31]

    Tvm: An automated end-to-end optimizing compiler for deep learning

    Tianqi Chen, Thierry Moreau, Ziheng Jiang, Lianmin Zheng, Eddie Yan, Haichen Shen, Meghan Cowan, Leyuan Wang, Yuwei Hu, Luis Ceze, et al. Tvm: An automated end-to-end optimizing compiler for deep learning. In 13th USENIX Symposium on Operating Systems Design and Implementation...

    2018

  23. [32]

    The rising costs of training frontier ai models

    Ben Cottier, Robi Rahman, Loredana Fattorini, Nestor Maslej, Tamay Besiroglu, and David Owen. The rising costs of training frontier ai models. arXiv preprint arXiv:2405.21015, 2024

    2024 arXiv

  24. [33]

    Z3:Anefficientsmtsolver

    LeonardoDeMouraandNikolajBjørner. Z3:Anefficientsmtsolver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008

    2008

  25. [34]

    Deepseek-v3 technical report, 2025

    DeepSeek-AI, Aixin Liu, Bei Feng, Bing Xue, Bochao Wu, et al. Deepseek-v3 technical report, 2025

    2025

  26. [35]

    Real-timeself-drivingcarnavigationusingdeepneuralnetwork.In 2018 4th International Conference on Green Technology and Sustainable Development (GTSD), pages 7–12, 2018

    Truong-Dong Do, Minh-Thien Duong, Quoc-Vu Dang, and My-Ha Le. Real-timeself-drivingcarnavigationusingdeepneuralnetwork.In 2018 4th International Conference on Green Technology and Sustainable Development (GTSD), pages 7–12, 2018

    2018

  27. [36]

    The llama 3 herd of models.arXiv preprint arXiv:2407.21783, 2024

    AbhimanyuDubey,AbhinavJauhri,AbhinavPandey,AbhishekKadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, et al. The llama 3 herd of models.arXiv preprint arXiv:2407.21783, 2024

    2024 arXiv

  28. [37]

    On neural network equivalence checking using smt solvers, 2022

    CharisEleftheriadis,NikolaosKekatos,PanagiotisKatsaros,andStavros Tripakis. On neural network equivalence checking using smt solvers, 2022

    2022

  29. [38]

    Gpipe: Efficient training of giant neural networks using pipeline parallelism

    Yanping Huang, Youlong Cheng, Ankur Bapna, Orhan Firat, Dehao Chen,MiaChen,HyoukJoongLee,JiquanNgiam,QuocVLe,Yonghui Wu, et al. Gpipe: Efficient training of giant neural networks using pipeline parallelism. InAdvances in Neural Information Processing Systems, pages 103–112, 2019

    2019

  30. [39]

    Oobleck: Resilient distributed training of large models using pipelinetemplates

    Insu Jang, Zhenning Yang, Zhen Zhang, Xin Jin, and Mosharaf Chowd- hury. Oobleck: Resilient distributed training of large models using pipelinetemplates. InProceedingsofthe29thSymposiumonOperating Systems Principles, SOSP ’23, page 382–395, New York, NY, USA,

  31. [40]

    Taso: optimizing deep learning computation with automatic generation of graph substitutions

    Zhihao Jia, Oded Padon, James Thomas, Todd Warszawski, Matei Zaharia, and Alex Aiken. Taso: optimizing deep learning computation with automatic generation of graph substitutions. InProceedings of the 27th ACM Symposium on Operating Systems Principles, pages 47–62, 2019

    2019

  32. [41]

    John Jumper, Richard Evans, Alexander Pritzel, Tim Green, Michael Figurnov, Olaf Ronneberger, Kathryn Tunyasuvunakool, Russ Bates, AugustinŽídek,AnnaPotapenko,etal.Highlyaccurateproteinstructure prediction with alphafold.Nature, 596(7873):583–589, 2021

    2021

  33. [42]

    Scalinglawsforneurallanguagemodels

    Jared Kaplan, Sam McCandlish, Tom Henighan, Tom B Brown, Ben- jamin Chess, Rewon Child, Scott Gray, Alec Radford, Jeffrey Wu, and DarioAmodei. Scalinglawsforneurallanguagemodels. arXivpreprint arXiv:2001.08361, 2020

    2001 arXiv

  34. [43]

    Reluplex: An efficient smt solver for verifying deep neural networks

    Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification, pages 97–117. Springer, 2017

    2017

  35. [44]

    Reducing activation recomputation in large transformer models

    Vijay Anand Korthikanti, Jared Casper, Sangkug Lym, Lawrence McAfee, Michael Andersch, Mohammad Shoeybi, and Bryan Catan- zaro. Reducing activation recomputation in large transformer models. Proceedings of Machine Learning and Systems, 2023

    2023

  36. [45]

    Se- quence parallelism: Making 4d parallelism possible.arXiv preprint arXiv:2105.13120, 2021

    Shenggui Li, Fuzhao Xue, Yongbin Li, and Yang You. Se- quence parallelism: Making 4d parallelism possible.arXiv preprint arXiv:2105.13120, 2021

    2021 arXiv

  37. [46]

    nnScaler: Constraint-guided parallelization plan generation for deep learning training

    Zhiqi Lin, Youshan Miao, Quanlu Zhang, Fan Yang, Yi Zhu, Cheng Li, Saeed Maleki, Xu Cao, Ning Shang, Yilei Yang, Weijiang Xu, Mao Yang, Lintao Zhang, and Lidong Zhou. nnScaler: Constraint-guided parallelization plan generation for deep learning training. In18th USENIX Symposiu...

    2024

  38. [47]

    Kochenderfer

    Changliu Liu, Tomer Arnon, Christopher Lazarus, Clark Barrett, and Mykel J. Kochenderfer. Algorithms for verifying deep neural networks. arXiv:1903.06758, 2019

    1903 arXiv

  39. [48]

    Aceso: Efficient parallel DNN training through iterative bottleneck alleviation

    Guodong Liu, Youshan Miao, Zhiqi Lin, Xiaoxiang Shi, Saeed Maleki, Fan Yang, Yungang Bao, and Sa Wang. Aceso: Efficient parallel DNN training through iterative bottleneck alleviation. InProceedings of the Nineteenth European Conference on Computer Systems, EuroSys ’24, page 16...

    2024

  40. [49]

    Ring attention with blockwise transformers for near-infinite context

    Hao Liu, Matei Zaharia, and Pieter Abbeel. Ring attention with blockwise transformers for near-infinite context. arXiv preprint arXiv:2310.01889, 2023

    2023 arXiv

  41. [50]

    Nnsmith: Generating diverse and valid test cases for deep learning compilers

    Jiawei Liu, Jinkun Lin, Fabian Ruffy, Cheng Tan, Jinyang Li, Aurojit Panda, and Lingming Zhang. Nnsmith: Generating diverse and valid test cases for deep learning compilers. InProceedings of the 28th ACM International Conference on Architectural Support for Programming Languag...

    2023

  42. [51]

    Uncovering nested data parallelism and data reuse in dnn computation with fractaltensor

    SiranLiu,ChengxiangQi,YingCao,ChaoYang,WeifangHu,Xuanhua Shi, Fan Yang, and Mao Yang. Uncovering nested data parallelism and data reuse in dnn computation with fractaltensor. InProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, pages 160–177, 2024

    2024

  43. [52]

    Differential testing for software

    William M McKeeman. Differential testing for software. Digital Technical Journal, 10(1):100–107, 1998

    1998

  44. [53]

    Smith, Mateusz Paprocki, Ondřej Čertík, Sergey B

    Aaron Meurer, Christopher P. Smith, Mateusz Paprocki, Ondřej Čertík, Sergey B. Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason K. Moore, Sartaj Singh, Thilina Rathnayake, Sean Vig, Brian E. Granger, Richard P. Muller, Francesco Bonazzi, Harsh Gupta, Shivam Vats, F...

    2017

  45. [54]

    Towardsformalrepairandverificationofindustry-scaledeep 14 neural networks

    Satoshi Munakata, Susumu Tokumoto, Koji Yamamoto, and Kazuki Munakata. Towardsformalrepairandverificationofindustry-scaledeep 14 neural networks. In2023 IEEE/ACM 45th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), pages 360–364. IEEE, 2023

    2023

  46. [55]

    Pipedream: generalized pipeline parallelism for dnn training

    Deepak Narayanan, Aaron Harlap, Amar Phanishayee, Vivek Seshadri, Nikhil R Devanur, Gregory R Ganger, Phillip B Gibbons, and Matei Zaharia. Pipedream: generalized pipeline parallelism for dnn training. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, p...

    2019

  47. [56]

    Automatic differentiation in pytorch

    Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang, Zachary DeVito, Zeming Lin, Alban Desmaison, Luca Antiga, and Adam Lerer. Automatic differentiation in pytorch. 2017

    2017

  48. [57]

    PyTorch.https://pytorch.org//

    PyTorch Team. PyTorch.https://pytorch.org//

  49. [58]

    Deepspeed-moe: Advancing mixture-of-experts infer- ence and training to power next-generation ai scale

    Samyam Rajbhandari, Conglong Li, Zhewei Yao, Minjia Zhang, Reza Yazdani Aminabadi, Ammar Ahmad Awan, Jeff Rasley, and Yuxiong He. Deepspeed-moe: Advancing mixture-of-experts infer- ence and training to power next-generation ai scale. InInternational conference on machine learn...

    2022

  50. [59]

    Zero:Memoryoptimizationtowardstrainingatrillionparametermodels

    Samyam Rajbhandari, Jeff Rasley, Olatunji Ruwase, and Yuxiong He. Zero:Memoryoptimizationtowardstrainingatrillionparametermodels. arXiv preprint arXiv:1910.02054, 2019

    1910 arXiv

  51. [60]

    Deepspeed: System optimizations enable training deep learning models with over 100 billion parameters

    Jeff Rasley, Samyam Rajbhandari, Olatunji Ruwase, and Yuxiong He. Deepspeed: System optimizations enable training deep learning models with over 100 billion parameters. InProceedings of the 26th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining, pages 35...

    2020

  52. [61]

    Megatron-LM: Training multi- billion parameter language models using gpu model parallelism.arXiv preprint arXiv:1909.08053, 2019

    Mohammad Shoeybi, Mostofa Patwary, Raul Puri, Patrick LeGresley, Jared Casper, and Bryan Catanzaro. Megatron-LM: Training multi- billion parameter language models using gpu model parallelism.arXiv preprint arXiv:1909.08053, 2019

    1909 arXiv

  53. [62]

    Deepid3: Face recognition with very deep neural networks, 2015

    Yi Sun, Ding Liang, Xiaogang Wang, and Xiaoou Tang. Deepid3: Face recognition with very deep neural networks, 2015

    2015

  54. [63]

    Perturbing numerical calculations for statistical analysis of floating-point program (in) stability

    Enyi Tang, Earl Barr, Xuandong Li, and Zhendong Su. Perturbing numerical calculations for statistical analysis of floating-point program (in) stability. InProceedings of the 19th international symposium on Software testing and analysis, pages 131–142, 2010

    2010

  55. [64]

    PyTorch DistributedTensor (DTensor).https://github.c om/pytorch/pytorch/tree/master/torch/distributed/_tensor

    PyTorch Team. PyTorch DistributedTensor (DTensor).https://github.c om/pytorch/pytorch/tree/master/torch/distributed/_tensor

  56. [65]

    TorchFX.https://pytorch.org/docs/stable/fx.html

    PyTorch Team. TorchFX.https://pytorch.org/docs/stable/fx.html

  57. [66]

    TorchScript.https://pytorch.org/docs/stable/jit.html

    PyTorch Team. TorchScript.https://pytorch.org/docs/stable/jit.html

  58. [67]

    Revisiting differential verification: Equivalence verification with confidence

    Samuel Teuber, Philipp Kern, Marvin Janzen, and Bernhard Beck- ert. Revisiting differential verification: Equivalence verification with confidence. arXiv preprint arXiv:2410.20207, 2024

    2024 arXiv

  59. [68]

    Llama 2: Open foundation and fine- tuned chat models.arXiv preprint arXiv:2307.09288, 2023

    Hugo Touvron, Louis Martin, Kevin Stone, Peter Albert, Amjad Alma- hairi, Yasmine Babaei, Nikolay Bashlykov, Soumya Batra, Prajjwal Bhargava, Shruti Bhosale, et al. Llama 2: Open foundation and fine- tuned chat models.arXiv preprint arXiv:2307.09288, 2023

    2023 arXiv

  60. [69]

    Attention is all you need.Advances in neural information processing systems, 30, 2017

    Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin. Attention is all you need.Advances in neural information processing systems, 30, 2017

    2017

  61. [70]

    {PET}: Optimizing tensor programs with partially equivalent transformationsandautomatedcorrections

    Haojie Wang, Jidong Zhai, Mingyu Gao, Zixuan Ma, Shizhi Tang, Liyan Zheng, Yuanzhi Li, Kaiyuan Rong, Yuanyong Chen, and Zhihao Jia. {PET}: Optimizing tensor programs with partially equivalent transformationsandautomatedcorrections. In 15thUSENIXSymposium on Operating Systems D...

    2021

  62. [71]

    Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification

    Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Advances in Neural Information Processing Systems, 34, 2021

    2021

  63. [72]

    Program slicing.IEEE Transactions on software engi- neering, (4):352–357, 1984

    Mark Weiser. Program slicing.IEEE Transactions on software engi- neering, (4):352–357, 1984

    1984

  64. [73]

    XLA — TensorFlow, compiled.https: //developers.googleblog.com/2017/03/xla-tensorflow-compiled.html

    XLA and TensorFlow teams. XLA — TensorFlow, compiled.https: //developers.googleblog.com/2017/03/xla-tensorflow-compiled.html

    2017

  65. [74]

    Oneflow: Redesign the distributed deep learning framework from scratch.arXiv preprint arXiv:2110.15032, 2021

    Jinhui Yuan, Xinqi Li, Cheng Cheng, Juncheng Liu, Ran Guo, Sheng- hang Cai, Chi Yao, Fei Yang, Xiaodong Yi, Chuan Wu, et al. Oneflow: Redesign the distributed deep learning framework from scratch.arXiv preprint arXiv:2110.15032, 2021

    arXiv

  66. [75]

    Gonzalez, and Ion Stoica

    Lianmin Zheng, Chengfan Jia, Minmin Sun, Zhao Wu, Cody Hao Yu, Ameer Haj-Ali, Yida Wang, Jun Yang, Danyang Zhuo, Koushik Sen, Joseph E. Gonzalez, and Ion Stoica. Ansor: Generating High- Performance tensor programs for deep learning. In14th USENIX Symposium on Operating Systems...

    2020

  67. [76]

    Alpa: Automating inter-and{Intra-Operator} parallelism for distributed deep learning

    Lianmin Zheng, Zhuohan Li, Hao Zhang, Yonghao Zhuang, Zhifeng Chen, Yanping Huang, Yida Wang, Yuanzhong Xu, Danyang Zhuo, Eric P Xing, et al. Alpa: Automating inter-and{Intra-Operator} parallelism for distributed deep learning. In16th USENIX Symposium on Operating Systems Desi...

    2022

  68. [77]

    striding

    In this case, the combination of1 and 4 results in the final gradients being over-scaled by a factor ofCP. TrainVerifyeliminatessuchbugsbycomparingdataflow of shape-reduced symbolic tensors. While the violation could be detected earlier via𝐿 == 𝐿0, practical implementations ty...

  69. [2023]

    Association for Computing Machinery

Pith tools

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