{"id":"39426a9e-2d6f-46f7-aecb-29ca01d71185","arxiv_id":"2506.15961","paper_version":2,"verdict":"REJECT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"TrainVerify verifies distributed LLM training execution plans against logical model definitions using symbolic dataflow graphs, shape reduction, and staged SMT solving, scaling to 671B-parameter models.","lead":"TrainVerify is a new system that symbolically checks whether a distributed training plan for a large language model is mathematically equivalent to the original single-device model, and the authors report verifying plans for Llama3 405B and DeepSeek-V3 671B. The work matters because silent parallelization bugs can waste weeks of GPU time, and this is the first attempt to rule out a broad class of them with formal methods.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem C.12 is false: single-index agreement does not imply full equivalence, so the shape-reduction soundness proof is invalid and the central guarantee is unsupported.","rationale":"The reader identified the weakest assumption as Theorem C.12, the correctness of shape reduction, and supplied a counterexample. That concern is correct and load-bearing; I have verified that the theorem is false even when the kernel functions are well-formed (Definition C.8), using linear maps representable as MatMul, which are explicitly within the paper's LLM-operator set. The proof sketch's step 2 claims that single-index agreement plus linear dependency mappings yields global permutation equivalence, but affine functions can agree at one index without being identical. This invalidates the theorem and breaks the chain from reduced-shape verification to full-size equivalence for the reported 405B/671B plans. I considered other possible concerns—staged verification's asynchronous relation pool is ultimately sound because each stage's own worker result is included in the final conjunction, and the focus on real arithmetic is an explicit scope choice. The load-bearing formal result is the shape-reduction theorem, and it fails. Because the paper's core contribution is the claim of provably correct execution plans, a false theorem in the proof means the central claim is not established. The reader's REJECT verdict remains appropriate; the paper would need a substantially revised correctness argument, or a more restricted theorem with additional hypotheses that actually hold for parallelization-equivalence pairs, before the formal guarantee can be accepted.","tokens_in":28493,"tokens_out":8943,"duration_ms":95014,"concrete_test":"Implement the counterexample as a two-element sDFG and run TrainVerify's shape-reduction pipeline on it. Use f = MatMul([[1,1],[1,1]], x) and g = MatMul([[1,1],[2,0]], x). If the reduced shape collapses both to a single output element, the solver will confirm agreement at index 0 and report equivalence; the original functions are not equivalent at index 1. A positive report would demonstrate unsoundness. Even without running code, independently re-derive the proof of Theorem C.12: check whether the claim 'τ_f ≡_P τ_g from a single-index precondition plus linearity' survives substituting τ_f(i)=[0,1] and τ_g(i)=[0,1-i]; it does not, because the two affine maps agree at i=0 but are not permutation-equivalent globally.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central scalability claim relies on Theorem C.12, which states that if f and g (functions composed by LLM operators) agree at one output index for all inputs, then they agree at every output index for all inputs. The proof step 2 asserts that this single-index precondition plus Observation 2 (linear dependency mappings) yields global mapping-permutation equivalence 'due to linear algebra.' This step is invalid: two affine/linear dependency maps can agree at one point without being identical. A concrete counterexample within the paper's own definitions uses single MatMul operators. Let f(x) = [[1,1],[1,1]]·x and g(x) = [[1,1],[2,0]]·x. Both are SIMD with the same well-formed kernel θ(a,b)=a+b, and both have affine dependency mappings: τ_f(i)=[0,1] for both outputs; τ_g(0)=[0,1], τ_g(1)=[0,0]. At index 0, f(x)[0]=x0+x1=g(x)[0] for all x, satisfying the precondition. But at index 1, f(x)[1]=x0+x1 while g(x)[1]=2x0; these differ, e.g., for x0=0, x1=1. Thus Theorem C.12 is false even with well-formed kernels and standard LLM operators. Since shape reduction is the mechanism that makes verification of 671B-parameter plans tractable, and the paper's formal claim is that reduced-shape verification provably extends to full shapes, the proof of this load-bearing theorem does not go through. The system may still be useful empirically, but its headline claim of provably correct execution plans is not established by the presented argument.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":28816,"tokens_out":5195,"duration_ms":50615,"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":[{"comment":"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.","section":"§6, Theorem 6.9; Appendix C, Theorem C.12"},{"comment":"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.","section":"Appendix C, Theorem C.12, proof step 2"},{"comment":"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.","section":"§7, §4"}],"minor_comments":[{"comment":"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.","section":"§5.2, Algorithm 1; Appendix A"},{"comment":"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.","section":"§8.3"},{"comment":"The appendix contains several typos that should be fixed, including 'opreations', 'dimention reduction', and 'Consdier this x′' in the proof of Theorem C.12.","section":"Appendix C"},{"comment":"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.","section":"§8.1, Table 3"},{"comment":"The caption reads 'The y-axes use alog2 scale'; this should be 'a log2 scale'.","section":"Figure 7 caption"}],"recommendation":"reject","confidential_remarks":"The false theorem alone justifies rejection. The ground-truth circularity is also worth editorial attention because the headline claim of correctness is weaker than it appears when both verified graphs are emitted by the same framework. There is no indication of misconduct, but the manuscript's scope and claims should be substantially revised if it is resubmitted."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nTwo things to know before you read this one. First, the paper is a serious systems effort: it verifies parallelization equivalence between a logical model graph and a distributed execution plan for Llama3-405B and DeepSeek-V3-671B plans, and that scale is new. Second, the central formal claim is not supported: Theorem C.12, which is the entire basis for shape reduction, is false as stated. The stress-test counterexample is correct: f(x)=[[1,1],[1,1]]x and g(x)=[[1,1],[2,0]]x are both SIMD MatMuls with the same kernel θ(a,b)=a+b; they agree at output index 0 for all x and differ at index 1. So single-index agreement does not imply full equivalence, and the proof step that 'by linear algebra' extends the permutation from one index to all indices does not go through.\n\nWhat is genuinely good: the problem is well chosen—silent parallelization bugs in multi-thousand-GPU training are expensive and hard to catch. Symbolic DFGs plus staged verification is a sensible decomposition, and the reported engineering numbers (verification in 0.5–47h, catching 14 mutated bug cases and two confirmed nnScaler bugs) suggest the system has real value as a bug-finding tool. The authors also clearly scope what they do not verify (kernels, runtimes) and state that the logical model is assumed correct.\n\nThe soft spots, in proportion. The false theorem is load-bearing: shape reduction is what makes 671B verification tractable, and the paper explicitly claims reduced-shape verification provably extends to full shapes. Since that proof fails, the 'provably correct execution plans' claim is unsupported. That alone would justify rejection of the formal contribution. The evaluation is also mostly self-referential—both graphs come from nnScaler, a same-team framework, and the 14 bugs are author-mutated rather than organically found—and no code or artifact is shipped, which makes claims like 'we verify 671B' hard to check. I do not consider the self-citation a problem; the overlap with nnScaler is disclosed and the framework is the natural target.\n\nWho this is for: systems and verification people interested in distributed training correctness. As a formal-methods paper it needs major rework—either a corrected shape-reduction theorem with genuinely restrictive structural assumptions, or a repositioning as an empirical checker. As a systems paper, the idea and initial results deserve referee time. I would send it out, but I would not accept it in this form.\n\nRecommendation: engage with it; reject the formal claim, encourage a revised version that either fixes the theorem or drops the provability language.","headline":"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.","tokens_in":29347,"tokens_out":2993,"would_cite":false,"duration_ms":30038,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["distributed training","parallelization equivalence","formal verification","symbolic dataflow graph","shape reduction","staged verification","SMT solver","LLM training"],"falsifier":"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.","tokens_in":28274,"feed_emoji":"✅","tokens_out":7676,"duration_ms":69503,"temperature":0.7,"pith_summary":"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.","feed_headline":"Distributed LLM training plans get formal equivalence proofs","feed_subtitle":"A verifier checks that multi-GPU execution is mathematically the same model, covering Llama3 405B and DeepSeek-V3 671B plans.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the parallelized IRGraph execution plan, lineage metadata, and the nnScaler framework that TrainVerify verifies; the whole method operates on these graphs.","marker":"[46]"},{"why":"Z3 is the SMT solver that discharges the equivalence formulas and returns counterexamples.","marker":"[33]"},{"why":"Provides the Llama3 model family and the production-scale distributed configurations used for the verification experiments.","marker":"[36]"},{"why":"Provides the DeepSeek-V3 architecture and training setup that constitutes the largest verified plan (671B parameters).","marker":"[34]"},{"why":"Automatic differentiation is the basis for reconstructing the backward pass and optimizer computations in the graph-completion step.","marker":"[7]"}],"fun_headline_variants":["Formal proof: distributed LLM training matches the model","TrainVerify: proven equivalence for distributed LLM training","Distributed training plans proven equal to logical model","Equivalence proofs for distributed LLM training up to 671B","Verifying distributed LLM training: equivalence proofs at scale"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Formal proof: distributed LLM training matches the model","TrainVerify: proven equivalence for distributed LLM training","Distributed training plans proven equal to logical model","Equivalence proofs for distributed LLM training up to 671B","Verifying distributed LLM training: equivalence proofs at scale"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000491,"raw_usage":{"total_tokens":2358,"prompt_tokens":836,"completion_tokens":1522,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":452,"completion_tokens_details":{"reasoning_tokens":1442}},"tokens_in":452,"tokens_out":1522,"duration_ms":10577,"temperature":1.0,"reasoning_tokens":1442,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T19:29:12.558362+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"nnScaler: Constraint-guided parallelization plan generation for deep learning training","cited_arxiv_id":null,"evidence_quote":"Supplies the parallelized IRGraph execution plan, lineage metadata, and the nnScaler framework that TrainVerify verifies; the whole method operates on these graphs."},{"cited_title":"Z3:Anefficientsmtsolver","cited_arxiv_id":null,"evidence_quote":"Z3 is the SMT solver that discharges the equivalence formulas and returns counterexamples."},{"cited_title":"Deepseek-v3 technical report, 2025","cited_arxiv_id":null,"evidence_quote":"Provides the DeepSeek-V3 architecture and training setup that constitutes the largest verified plan (671B parameters)."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Automatic differentiation is the basis for reconstructing the backward pass and optimizer computations in the graph-completion step."}],"review_version":1}