{"id":"076ef924-ea00-4ee8-a759-b86191139cdd","arxiv_id":"2509.10694","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Scalify verifies semantic equivalence of baseline and distributed ML computational graphs using equality saturation and relational reasoning, finding real silent errors in production frameworks.","lead":"A new tool called Scalify checks whether a machine learning computation run on one device and the same computation distributed across many devices really compute the same thing, by comparing their computation graphs. It found five previously unknown bugs in Amazon's production AI frameworks and verified a 405-billion-parameter model in minutes.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Soundness of the 25 rewrite rules is asserted, not proved; a single unsound rule would let Scalify certify buggy graphs.","rationale":"The reader's weakest assumption identifies the same load-bearing concern I find: the soundness of the 25 rewrite rules and the Table 1 Datalog-style relations is asserted in Section 5.1 but never formally proved, machine-checked, or validated against a reference oracle. This matters because the system's core guarantee is exactly that verified graphs are semantically equivalent; any unsound rule directly breaks that guarantee. The paper honestly acknowledges several limitations (incompleteness, graph-level scope, inference-only evaluation, manual diagnosis), and the 17/19 detection result plus five new bugs provide strong empirical evidence that the tool is useful. However, the soundness claim is a mathematical assertion about all graphs and all rule applications, and empirical success on a finite bug corpus cannot establish it. The concrete test I propose combines a known-bug injection check with a fuzzing-based differential test against an exact oracle; either would give evidence for or against the soundness premise. My recommendation is CONDITIONAL, consistent with the reader: no formal soundness proof, no large-scale negative-oracle validation, and no shipped artifact or machine-checked certificate. If the authors add either a formal soundness argument for each rule family or an experimental validation against an exact reference over a broad graph corpus, the concern would be substantially resolved.","tokens_in":23861,"tokens_out":1558,"duration_ms":13511,"concrete_test":"Inject a controlled non-equivalent graph pair (e.g., the BSH reshape-transpose swap without the compensating transpose) and confirm Scalify reports unverified; then run a broader differential test: generate 10,000 small tensor programs covering the rule families in Table 1, compute exact semantics with a reference interpreter, apply Scalify to equal and perturbed pairs, and measure the false-positive rate. If any perturbed pair is reported verified, the soundness assertion in Section 5.1 is violated.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The paper's central claim is that Scalify soundly verifies semantic equivalence of computational graphs at production scale. Section 5.1 states 'the relation analysis and e-graph rewrite rules are sound,' but no proof or machine-checked certificate is provided for any of the 25 manually written meta rules or the Datalog-style rules in Table 1. One unsound rule or a rule applied outside its intended domain would allow a non-equivalent graph pair to merge into the same e-class, yielding a false 'verified' verdict and undermining both the bug-detection results and the core correctness guarantee. The paper's own limitation section claims soundness, but soundness here is a universal statement about all rule applications, and empirical success on 19 reproduced bugs plus 5 new discoveries cannot establish it. The full-text paper in this package also contains passages suffixed with '/gid...' tokens (e.g., around Figure 2 and Section 5.2.1) whose provenance is unclear, but the core concern is the unproved rule-soundness premise, which the reader's weakest_assumption independently identifies.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":24200,"tokens_out":8635,"duration_ms":77971,"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":[{"comment":"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.","section":"§5.1 (Soundness) and §8 (Limitations)"},{"comment":"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.","section":"§5.2.3, Algorithm 2"},{"comment":"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.","section":"Table 1 and Figure 7"}],"minor_comments":[{"comment":"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.","section":"Full text, near Figure 2 and Figure 4"},{"comment":"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.","section":"§5.1, Algorithm 1"},{"comment":"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.","section":"§7.1, comparison to TrainVerify"},{"comment":"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.","section":"Figure 12"},{"comment":"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.","section":"§6 Implementation"}],"recommendation":"major_revision","confidential_remarks":"This is a strong systems paper with one load-bearing gap: the soundness guarantee is asserted without a proof or formal semantics. If the authors can supply a rigorous soundness argument or explicitly downgrade the guarantee to rule-set-relative certificates, I would support acceptance. The stray /gid strings appear to be extraction artifacts and are not themselves a reason for rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know this paper is a real engineering contribution, not a toy. Scalify builds on equality saturation (egglog) but adds relational reasoning for sharding/layout and symbolic bijection inference for reshape-transpose sequences, and the combination verifies Llama-3.1-405B in under three minutes on a commodity CPU. That result is credible: they operate on the graph IR, not tensors, so runtime depends on graph size, and their scaling plots (flat in seq len/batch/TP degree, linear in layers) match that claim. The bug-finding evidence is also solid: 17/19 re-implemented historical bugs detected, five new bugs in Amazon's NeuronX stack, with submissions to developers. Localization to source lines is a nice touch.\n\nThe weak spot is the one the stress test flags. Section 5.1 says the relation analysis and rewrite rules \"are sound,\" but there is no proof — not even a sketch — for the 25 hand-written meta rules or the Datalog rules in Table 1. For a verifier, soundness is the product. One unsound rule, or a rule applied outside its intended domain, lets Scalify certify a buggy graph. Empirical success on 22 bugs cannot establish a universal claim. This is not fatal: the rules are mostly standard algebraic facts about collectives and reshapes, and the authors are honest that completeness is not guaranteed. But the paper should either ship a machine-checked proof of the rule set, or state the guarantee as \"verified relative to the rules\" and justify why each rule is trustable. Also minor: the TrainVerify comparison uses published numbers, not a run on their hardware; \"eliminates software bugs\" in Section 3 is too strong; no artifact is provided, which matters for a reproducibility-oriented venue.\n\nI doubt the /gid tokens in the PDF are substantive — looks like a rendering artifact — but worth checking in the camera-ready.\n\nBottom line: this is a systems paper with a plausible core idea and unusually strong evaluation. The soundness gap is addressable and should be pushed, not a desk-reject reason. I'd accept for peer review and ask for the proof or a precise rule-soundness statement, plus artifact release.\n\nRecommendation: engage. Send to a serious venue; it will be a useful benchmark for graph-equivalence checking.","headline":"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.","tokens_in":24565,"tokens_out":1316,"would_cite":true,"duration_ms":11435,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Equality saturation can verify semantic equivalence of large ML computational graphs, making silent distributed-framework errors detectable at graph level.","keywords":["equality saturation","e-graph","computational graph verification","silent errors","distributed machine learning","Datalog reasoning","layout optimization","bug localization"],"falsifier":"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.","tokens_in":23669,"feed_emoji":"✅","tokens_out":3516,"duration_ms":31322,"temperature":0.7,"pith_summary":"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.","feed_headline":"Verifier checks 405B-parameter models in minutes","feed_subtitle":"Semantic graph comparison surfaces silent distributed-training bugs that numeric checks miss.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Defines equality saturation, the core rewrite-search technique the paper adapts for computational-graph verification.","marker":"[72]"},{"why":"Provides the egg e-graph engine that originally demonstrated practical equality-saturation rewriting.","marker":"[83]"},{"why":"Supplies egglog, the Datalog-augmented e-graph engine Scalify builds on for relational reasoning over tensor sharding and layout.","marker":"[86]"},{"why":"TrainVerify is the SMT-based baseline the paper compares against, showing Scalify avoids solver cost and fragile reductions.","marker":"[58]"},{"why":"Transformers NeuronX is one of the two production frameworks where Scalify uncovered previously unknown bugs and reproduced historical ones.","marker":"[27]"},{"why":"NeuronX Distributed is the other production framework in which Scalify found two of the five new bugs.","marker":"[24]"}],"fun_headline_variants":["Scalify verifies 405B-parameter graphs in minutes","Distributed ML silent bugs exposed by graph equivalence","New verifier catches unknown bugs in Amazon ML","Graph semantic check finds errors in huge models","Equality saturation scales to 405B-parameter verification"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Scalify verifies 405B-parameter graphs in minutes","Distributed ML silent bugs exposed by graph equivalence","New verifier catches unknown bugs in Amazon ML","Graph semantic check finds errors in huge models","Equality saturation scales to 405B-parameter verification"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00044,"raw_usage":{"total_tokens":2191,"prompt_tokens":863,"completion_tokens":1328,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":479,"completion_tokens_details":{"reasoning_tokens":1253}},"tokens_in":479,"tokens_out":1328,"duration_ms":9666,"temperature":1.0,"reasoning_tokens":1253,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T15:53:07.961603+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines equality saturation, the core rewrite-search technique the paper adapts for computational-graph verification."},{"cited_title":"TrainVerify: Equivalence-Based Verification for Distributed LLM Training","cited_arxiv_id":"2506.15961","evidence_quote":"TrainVerify is the SMT-based baseline the paper compares against, showing Scalify avoids solver cost and fragile reductions."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Transformers NeuronX is one of the two production frameworks where Scalify uncovered previously unknown bugs and reproduced historical ones."},{"cited_title":"NeuronX Distributed (NxD).https://awsdocs- neuron.readthedocs-hosted.com/en/latest/libraries/neuronx- distributed/index.html","cited_arxiv_id":null,"evidence_quote":"NeuronX Distributed is the other production framework in which Scalify found two of the five new bugs."}],"review_version":1}