It Takes Two to Entangle

A giant AI model is too big for one GPU, so programmers hand-convert the simple single-GPU model into a distributed version spread across many GPUs — and that manual rewrite quietly introduces bugs that make the distributed model compute something subtly different from the original; this paper (New York University and ByteDance — Zhanghan Wang, Ding Ding, Aurojit Panda, and colleagues) presents Entangle, which statically proves whether the original model's outputs can be reconstructed from the distributed version's, catching such bugs before deployment and pointing at the operator that is wrong.

The argument in one glance

Problem

Splitting a model across GPUs is a hand rewrite that quietly introduces bugs

Today's large machine-learning models need more memory and compute than any single GPU can provide, so they are run across many GPUs spread over many servers, for both training and inference. But a model is first written as a sequential specification — a series of operations assuming everything runs on one processor, on local data. To distribute it, an implementer converts that specification into a distributed version by deciding how to partition the model's state and computation, choosing among distribution strategies (data parallelism, tensor parallelism, sequence and context parallelism, expert parallelism for mixture-of-experts models, and more). Doing so is not automatic: the implementer must hand-insert communication operations (like all-reduce and all-gather) and transformation operations so that the distributed version still computes what the sequential one did. This is exactly where bugs creep in. An implementer might use an incorrect parameter — the wrong padding, a wrong offset, a wrong scaling factor — or simply forget a needed operation, and the result is a distributed model whose outputs differ from the sequential model's. These bugs are insidious because the distributed model still runs and produces plausible numbers; it just computes the wrong thing, silently corrupting training or inference. This is not hypothetical: the work was motivated by real bugs introduced at ByteDance when distributing a recent model, and similar bugs have been found across open-source distributed ML implementations.
What people did

Test the distributed model, or review the code by hand

The usual ways to catch such bugs are dynamic and manual. You can run the distributed implementation and compare its outputs against the sequential model on some inputs, or compare training curves, or have engineers carefully review the added communication and transformation code. These approaches do find some bugs, and they are what practitioners reach for today.
Why it fell short

Testing misses subtle bugs and cannot cover every case

Testing and review are fundamentally incomplete. Comparing outputs on sample inputs only checks the cases you happened to try, and a distribution bug may only manifest on particular shapes, partition counts, or numerical patterns, so it slips through. Many of these bugs do not crash or produce obviously wrong output; they cause a subtle divergence that looks like ordinary training noise or a small accuracy loss, so no test flags them, and they can go undetected until they have wasted enormous amounts of compute or shipped a degraded model. Manual review, meanwhile, does not scale to the size and intricacy of modern distributed implementations, where the added communication and transformation logic is spread across a large codebase and many GPUs. What was missing was a way to prove, statically and before deployment, that a distributed implementation computes exactly what its sequential specification does — not just on sampled inputs but in general — and to do so for real, large models rather than toy examples.
This paper's idea

Prove the distributed model refines the sequential one, operator by operator

Entangle statically checks a property the authors call model refinement: can the sequential model's outputs be reconstructed from the distributed model's outputs, assuming the inputs were partitioned correctly? The insight is that a correct distribution strategy guarantees exactly this — if the inputs are split the right way, then combining the distributed outputs (by gathering and reducing them across GPUs) recovers the original sequential result. So Entangle looks for a relation mapping the distributed model's outputs back to the sequential model's outputs. It finds this relation using iterative term rewriting (equality saturation): it applies rewrite rules to build up equivalent forms and searches for a way to express each sequential output as a combination — a concatenation, a reduction, and so on — of distributed tensors. The distributed model refines the sequential one if Entangle can find a complete clean relation: one that reconstructs every sequential output purely by gathering and combining distributed outputs, with no extra computation. If no such clean relation exists for some output, that is a bug. To scale to real models, Entangle processes each sequential operator individually, which keeps the number of rewritten terms small and makes runtime grow linearly with model size — it checks state-of-the-art models like GPT, Qwen2, and Llama-3 in 10 to 245 seconds, under five minutes. And because it works one operator at a time, when it finds a bug it can point at the specific operator whose outputs could not be reconstructed, giving programmers actionable help in localizing the problem. Crucially, the per-operator approach is sound: Entangle always reports a bug if one exists.

Why this problem is worth solving

Distributed training and inference are how every large model runs, and a silent correctness bug in that distribution can waste vast compute or ship a broken model.

Every frontier model is trained and served across many GPUs, because none fits on one, and the code that spreads it out is written by hand. A bug in that code does not announce itself: the distributed model still runs, still consumes its enormous compute budget, and still produces numbers — they are just subtly wrong. In training, that can mean weeks of expensive GPU time spent optimizing the wrong computation, or a model that quietly underperforms what it should. In inference, it can mean serving incorrect results at scale. Because these bugs hide inside plausible behavior, they can persist for a long time before anyone notices, and by then the cost is enormous. Catching them before deployment therefore has outsized value: it protects the single most expensive activity in modern AI from a class of errors that testing is poorly suited to find. And since the same distribution strategies are applied over and over to new models, a tool that checks them statically pays off repeatedly, across every model an organization distributes.

The key is to reframe correctness as a reconstruction question that can be checked without running anything.

The naive notion of correctness — does the distributed model produce the same outputs as the sequential one? — is hard to check statically, because the two run on different data layouts across different numbers of devices. Entangle’s reframing is subtler and more checkable: the distributed model is correct if the sequential model’s outputs can be reconstructed from the distributed model’s outputs, given a correct input partitioning. This is exactly what a correct distribution strategy promises — that gathering and combining the per-GPU results recovers the original answer — so it captures correctness precisely while turning it into a question about the existence of a mathematical relation between two computation graphs. That question can be attacked symbolically, without executing the model on any input, which is what makes the check static and complete rather than sample-based. The relation also has to be clean — reconstructing the outputs purely by gathering and combining, not by doing extra computation that would paper over a missing operation — because a bug often looks exactly like needing an extra step that a correct distribution would not require. Framing the problem as finding a clean reconstruction relation is what lets Entangle both prove correctness and, by its absence, pinpoint bugs.

What people did before, and where it broke

Compare distributed and sequential outputs on sample inputs. Run both and check they agree on some tests. Where it broke. It only covers the inputs you try; distribution bugs that manifest on particular shapes, partition counts, or numerics slip through.
Watch training curves for anomalies. Notice if the distributed model trains worse. Where it broke. Subtle bugs look like ordinary training noise or a small accuracy loss, so they go undetected while wasting compute.
Review the added communication and transformation code by hand. Have engineers audit the distribution logic. Where it broke. It does not scale to the size and intricacy of real distributed implementations spread across a large codebase and many GPUs.
Trust that the distribution strategy was applied correctly. Assume the standard parallelism transformations are bug-free. Where it broke. Applying them requires hand-inserting parameters and operations, where wrong padding, offsets, scaling, or forgotten operations introduce real bugs.
The gap. No approach statically proved, for real large models, that a distributed implementation computes exactly what its sequential specification does, and pointed at the faulty operator when it did not.

How Entangle works

Checking that a distributed model reconstructs its sequential specification

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Prove the implementation matches its specification, rather than testing it. Entangle’s foundation is to treat the distributed model as an implementation that must provably refine the sequential specification — establishing equivalence by construction instead of by sampling inputs. Statically proving that a lower-level, transformed program correctly implements a higher-level specification, rather than testing outputs, is the same approach the work on lightweight modular verification for WebAssembly-to-native compilation covered elsewhere on this site takes, checking that a translation preserves meaning rather than trusting it. Entangle applies this to the translation from a sequential model to its distributed form, where the transformation is a hand-applied distribution strategy.

Search a space of equivalent expressions with equality saturation. To discover how a sequential output can be rebuilt from distributed tensors, Entangle applies rewrite rules and grows a compact representation of many equivalent forms, then looks for one that matches. Using term rewriting over an e-graph to explore the space of expressions equal to a target, rather than reasoning about one form at a time, is the same technique the work on finding reusable instructions via e-graph anti-unification (ISAMORE) covered elsewhere on this site builds on, letting equality saturation surface the form you need. Entangle uses it to find the reconstruction relation, and its absence to flag a bug.

Reason about the very distribution strategies that make bugs possible. Entangle’s whole subject is the parallelism strategies — data, tensor, sequence, context, and expert parallelism — that programmers compose to spread a model across GPUs, and whose manual application is where errors enter. Working at the level of how partitioning strategies compose to distribute a machine-learning model is the same terrain the work on composing SPMD partitioning strategies for machine learning (PartIR) covered elsewhere on this site occupies, treating the distribution as a structured, analyzable object. Where that line of work builds correct distributions, Entangle checks that a hand-built one is in fact correct.

Following a matrix multiply through Entangle

Checking a distributed matrix-multiply operator refines the sequential one

A trace, drawn from the paper's example, of how Entangle verifies one operator by finding a reconstruction relation.

Step 1 of 5

Take one operator from the sequential model

Entangle processes the sequential model one operator at a time. Consider a matrix multiplication producing an output tensor; Entangle's job is to reconstruct that sequential output from the distributed model's tensors.

Working per-operator keeps the search small and localizes any bug.

Why it works

Refinement captures correctness that testing samples only approximate. Comparing outputs on some inputs misses cases → but proving the sequential outputs are reconstructible from the distributed ones in general → so correctness is established symbolically rather than by luck of the tests.
The clean-relation requirement exposes missing operations. A bug often looks like needing an extra computation to fix up the output → but requiring reconstruction by gathering and combining alone → so a missing or wrong operation shows up as the absence of a clean relation.
Equality saturation finds the reconstruction if it exists. The right way to rebuild an output from distributed tensors is not obvious → but growing many equivalent forms with rewrite rules and searching them → so Entangle discovers the concatenations and reductions that reconstruct each output.
Per-operator processing makes it scale. Reasoning about a whole model at once explodes the rewriting → but checking one operator at a time bounds the terms considered → so runtime grows linearly and real models check in minutes.
Per-operator processing also localizes bugs. A whole-model failure would not say where the bug is → but a per-operator check names the operator whose output could not be reconstructed → so programmers get actionable guidance, not just a yes-or-no.

What it costs (trade-offs and scope)

It checks refinement, assuming a correct input partitioning. Entangle verifies the sequential output can be reconstructed given that inputs are partitioned correctly, using a user-provided input mapping; the guarantee is relative to that assumption, so an incorrect input mapping is outside what it certifies.
It reasons symbolically about operator semantics, not numerics. The approach proves the computation graphs correspond, not that floating-point rounding or numerical behavior matches exactly; bugs that are purely numerical rather than structural are a different problem.
Its power depends on the rewrite rules. Finding a reconstruction relation relies on the rewrite rules and lemmas Entangle knows; an unusual operation or distribution pattern outside that rule set could require extending it, and the search space, while bounded per operator, still depends on those rules.
Soundness is the priority, which shapes what it reports. Entangle is built to always report real bugs (no missed bugs); the paper’s design centers this guarantee, and users should read the reported operator-level errors as the actionable output rather than expecting an automatic fix.
Reported speeds are for specific models and setups. The 10-to-245-second checking times are for particular state-of-the-art models (GPT, Qwen2, Llama-3) and deployments; the exact runtime depends on the model’s size and the operators and strategies involved.

The evaluation

Catching bugs in distributed ML model implementations

Property	Sample-based testing	Manual code review	Entangle
Coverage
Catches subtle silent bugs
Scales to real large models
Bug localization
When it runs

A comparison of ways to catch bugs in distributed ML model implementations. By statically checking model refinement — whether the sequential model's outputs can be reconstructed from the distributed model's outputs — using equality saturation, processing one operator at a time, Entangle soundly finds distribution bugs before deployment and names the faulty operator, checking models like GPT, Qwen2, and Llama-3 in 10 to 245 seconds. Exact figures should be read from the paper.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

This explainer is based on the paper’s full text (the authors’ copy hosted at New York University, of the ASPLOS 2026 paper). The described system is the paper’s: Entangle statically identifies bugs in distributed ML model implementations by checking model refinement — whether a sequential model’s outputs can be reconstructed from a distributed model implementation’s outputs, assuming a user-provided input partitioning is correct. It uses iterative term rewriting (equality saturation, over an e-graph) to generate a relation mapping the distributed model’s outputs to the sequential model’s outputs; the distributed model refines the sequential one if Entangle finds a complete clean relation (one reconstructing all sequential outputs purely by gathering and combining distributed outputs, without extra computation), and the lack of a clean relation indicates a bug. It processes each sequential operator individually, which keeps runtime linear in model complexity and enables bug localization (naming the operator whose outputs could not be reconstructed), and this per-operator approach is sound (Entangle always reports bugs if they exist). It works with PyTorch and other frameworks (including TensorFlow and JAX). The paper reports checking state-of-the-art models including GPT, Qwen2, and Llama-3 in 10 to 245 seconds (under five minutes), and that the work was motivated by real distribution bugs at ByteDance. The distribution-strategy background above (data, tensor, sequence, context, and expert parallelism, and communication operations like all-reduce and all-gather) is standard distributed-ML context provided to make the approach intuitive. The step-by-step walkthrough follows the paper’s matrix-multiply example but is simplified. Exact definitions, the rewriting rules and lemmas, the completeness and soundness arguments, and the full evaluation and bug case studies should be read from the paper.

Background

Why building AI systems increasingly means verifying the transformations that build them

It helps to see Entangle within a broad pattern: as machine-learning systems grow, more and more of the engineering is not writing the model but mechanically transforming it — distributing it across GPUs, quantizing it, compiling it, fusing its operators — and each transformation is an opportunity to silently change what the model computes. The original model may be correct, but the version that actually runs is the product of a chain of rewrites, any of which can introduce a discrepancy that testing struggles to catch because the failure is subtle rather than a crash. The response, borrowed from decades of programming-languages research, is to treat these transformations as things to verify rather than trust: prove that the transformed artifact still means what the original did. This is translation validation applied to the AI stack, and it matters more as the transformations get more aggressive and the models get more expensive to run. Entangle’s particular contribution is to make this practical for the distribution transformation specifically, at the scale of real frontier models, by reframing correctness as reconstructibility and using equality saturation to check it operator by operator. This effort to bring rigorous, automated verification to the real systems people actually build and run, rather than idealized ones, is the same terrain the work on highly automated verification of security properties for unmodified system software (Spoq2) covered elsewhere on this site occupies, pushing formal methods to meet real code at scale. Entangle shows that the manual, error-prone step of parallelizing a model — one of the most consequential transformations in modern AI — can be checked automatically, catching silent correctness bugs before they cost weeks of compute or ship a broken model.

If you remember only three things

1. Large ML models are run across many GPUs because they do not fit on one, and distributing them is a manual process: a programmer converts a sequential model specification into a distributed version by choosing distribution strategies (data, tensor, sequence, context, expert parallelism) and hand-inserting communication and transformation operations. Mistakes — wrong padding, offsets, or scaling factors, or forgotten operations — make the distributed model compute different outputs from the sequential one. These bugs are insidious: the model still runs and produces plausible numbers, so they look like training noise and evade testing, while silently wasting compute or shipping a degraded model. Real such bugs motivated the work at ByteDance, and similar ones appear across open-source implementations.
2. Entangle statically checks model refinement: can the sequential model's outputs be reconstructed from the distributed model's outputs, given a correct input partitioning? This is exactly what a correct distribution strategy guarantees. Entangle uses iterative term rewriting (equality saturation over an e-graph) to find a relation expressing each sequential output as a combination — a concatenation, a reduction — of distributed tensors. The distributed model refines the sequential one only if there is a complete clean relation that reconstructs every output purely by gathering and combining distributed tensors, with no extra computation; the absence of one is a bug. Entangle processes each sequential operator individually, keeping runtime linear in model size and letting it name the faulty operator, and this per-operator approach remains sound — it always reports a bug if one exists.
3. Entangle works with PyTorch and other frameworks and scales to real models: the paper reports checking state-of-the-art models like GPT, Qwen2, and Llama-3 in 10 to 245 seconds (under five minutes), and it provides actionable output that helps programmers localize and fix bugs. The trade-offs: it certifies refinement relative to a user-provided input partitioning; it reasons about the computation graphs' correspondence symbolically rather than about exact floating-point numerics; its reach depends on its rewrite rules and lemmas; and it is designed around soundness, reporting operator-level errors rather than auto-fixing. Reported checking times depend on the specific models and deployments.

Check yourself

Check your understanding

1. Why do bugs get introduced when a model is distributed across GPUs, and why are they hard to catch?
2. What is "model refinement," the property Entangle checks?
3. How does Entangle search for the reconstruction relation, and what counts as a bug?
4. How does Entangle scale to real large models and help programmers, and what property does it guarantee?

Sources

The paper is “It Takes Two to Entangle” by Zhanghan Wang, Ding Ding, Hang Zhu, Haibin Lin, and Aurojit Panda (New York University and ByteDance Seed), published at ASPLOS 2026, DOI 10.1145/3779212.3790178. It is open access under CC BY, with an author copy hosted at New York University and source code at github.com/nyu-systems/Entangle.

This explainer is written from the paper’s full text (the authors’ NYU-hosted copy). Entangle statically identifies bugs in distributed ML model implementations by checking model refinement: whether a sequential model’s outputs can be reconstructed from a distributed implementation’s outputs, assuming a correct user-provided input partitioning. It uses iterative term rewriting (equality saturation over an e-graph) to find a relation mapping distributed outputs to sequential outputs; the distributed model refines the sequential one if a complete clean relation exists (reconstructing all outputs purely by gathering and combining distributed outputs, without extra computation), and the lack of one indicates a bug. Entangle processes each sequential operator individually, keeping runtime linear in model complexity, enabling bug localization by naming the faulty operator, and remaining sound (always reporting bugs if they exist). It works with PyTorch and other frameworks, and the paper reports checking GPT, Qwen2, and Llama-3 in 10 to 245 seconds, motivated by real distribution bugs at ByteDance. Numbers are the paper’s own; exact mechanisms and full results should be confirmed in the paper.