Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verify Implementation Equivalence of Large Models

Qi Zhan, Xing Hu, Xin Xia, Shanping Li

Abstract

Verifying whether two implementations of the same large model are equivalent across frameworks is difficult in practice. Even when they realize the same computation, their graphs may differ substantially in operator decomposition, tensor layout, and the use of fused or opaque kernels, making manual rewrite rules hard to build and maintain. We present Emerge, a framework for checking Implementation Equivalence over computation graphs of large-model implementations. Instead of writing rules manually, Emerge represents the two implementations in an e-graph, infers candidate relations from execution values, and synthesizes rewrite rules on demand when existing rules are insufficient. Each synthesized rule is validated using the strongest applicable method, including SMT- based checking for symbolically tractable cases and constraint-aware randomized testing for opaque kernels, and then propagated through e-graph rebuilding to establish larger equivalences. Our current implementation targets inference computation graphs captured from HuggingFace Transformers and vLLM. Our evaluation shows that Emerge establishes equivalence for correct implementation pairs at practical cost, while also providing useful by-products for debugging: it detects 10 of 13 known implementation bugs and uncovers 8 previously unknown implementation issues that were later confirmed by developers. In addition, Emerge synthesizes block-level rules that compare favorably with manually authored ones.

Verify Implementation Equivalence of Large Models

Abstract

Verifying whether two implementations of the same large model are equivalent across frameworks is difficult in practice. Even when they realize the same computation, their graphs may differ substantially in operator decomposition, tensor layout, and the use of fused or opaque kernels, making manual rewrite rules hard to build and maintain. We present Emerge, a framework for checking Implementation Equivalence over computation graphs of large-model implementations. Instead of writing rules manually, Emerge represents the two implementations in an e-graph, infers candidate relations from execution values, and synthesizes rewrite rules on demand when existing rules are insufficient. Each synthesized rule is validated using the strongest applicable method, including SMT- based checking for symbolically tractable cases and constraint-aware randomized testing for opaque kernels, and then propagated through e-graph rebuilding to establish larger equivalences. Our current implementation targets inference computation graphs captured from HuggingFace Transformers and vLLM. Our evaluation shows that Emerge establishes equivalence for correct implementation pairs at practical cost, while also providing useful by-products for debugging: it detects 10 of 13 known implementation bugs and uncovers 8 previously unknown implementation issues that were later confirmed by developers. In addition, Emerge synthesizes block-level rules that compare favorably with manually authored ones.
Paper Structure (33 sections, 6 equations, 4 figures, 2 tables, 2 algorithms)

This paper contains 33 sections, 6 equations, 4 figures, 2 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Emerge in a Nutshell
  3. Input Relation.
  4. Congruence and Graph Rebuilding.
  5. Rule Synthesis and Application.
  6. Opaque Kernels.
  7. Approach
  8. Formalization
  9. Relation Inference
  10. Rule Synthesis
  11. Rule Validation
  12. Rule Application
  13. E-Class Merge and Graph Rebuild
  14. Fault Localization
  15. Implementation
  16. ...and 18 more sections

Figures (4)

  • Figure 1: A part of GPT-2 Model used to illustrate equivalence verification between two implementations. Simplified and adjusted for clarity.
  • Figure 2: Rule synthesis from execution traces. ① Initial relation ② Relation inferred from input values ③ Relation inferred from rule synthesis.
  • Figure 3: RQ2 results on correctness and scalability.
  • Figure 4: Comparison of tensor-parallel equivalence rules. Top: normalized block-level rules synthesized by Emerge from execution traces. Bottom: manually authored component rules used by Entangle. All rules assume compatible tensor shapes and partition layouts. R2 and E4 additionally assume that query, key, and value tensors are partitioned into disjoint head groups under a fixed query-to-KV head mapping $\pi$.