論文の概要: Verify Implementation Equivalence of Large Models
- arxiv url: http://arxiv.org/abs/2603.21851v1
- Date: Mon, 23 Mar 2026 11:39:56 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-24 19:11:39.63889
- Title: Verify Implementation Equivalence of Large Models
- Title(参考訳): 大規模モデルの実装等価性検証
- Authors: Qi Zhan, Xing Hu, Xin Xia, Shanping Li,
- Abstract要約: 本稿では,大規模モデル実装のグラフ上での実装等価性をチェックするためのフレームワークであるEmergeを紹介する。
手動でルールを書く代わりに、Emergeは2つの実装をEグラフで表現し、実行値から候補関係を推測し、要求に応じて書き直しルールを合成する。
- 参考スコア(独自算出の注目度): 9.854606980804016
- License: http://creativecommons.org/licenses/by/4.0/
- 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.
- Abstract(参考訳): 同じ大きなモデルの2つの実装がフレームワーク間で同等であるかどうかを検証することは、実際には難しい。
同じ計算を実現したとしても、それらのグラフは演算子分解、テンソルレイアウト、融合または不透明なカーネルの使用で大きく異なり、手書きの書き直しルールの構築と保守が困難になる。
本稿では,大規模モデル実装の計算グラフ上での実装等価性をチェックするためのフレームワークであるEmergeを紹介する。
手動でルールを書く代わりに、EmergeはEグラフで2つの実装を表現し、実行値から候補関係を推測し、既存のルールが不十分な場合に要求の書き直しルールを合成する。
それぞれの合成規則は、SMTに基づくシンボル抽出可能なケースのチェックや不透明カーネルの制約対応ランダム化テストなど、最も有効な方法を用いて検証され、Eグラフ再構築によってより大きな等価性を確立する。
現在の実装では、HuggingFace TransformerとvLLMから取得した推論計算グラフをターゲットにしています。
私たちの評価では,Emerge が実装ペアの正当性を実用的コストで確立し,デバッグに有用な副産物を提供するとともに,13 の既知の実装バグの10 つを検出し,後に開発者が確認した8 つの実装問題を明らかにする。
さらに、Emergeは手動で作成したものと好意的に比較できるブロックレベルのルールを合成する。
関連論文リスト
- Type-Aware Retrieval-Augmented Generation with Dependency Closure for Solver-Executable Industrial Optimization Modeling [0.42753669499145647]
本稿では,モデルエンティティタイプと最小限の依存性のクロージャを強制し,実行可能性を保証するタイプアウェア検索拡張生成(RAG)手法を提案する。
本手法は, 電池生産における需要応答最適化とフレキシブルなジョブショップスケジューリングという2つの制約集約型産業事例で検証する。
論文 参考訳(メタデータ) (2026-03-03T17:41:34Z) - DAG-Math: Graph-Guided Mathematical Reasoning in LLMs [54.231935013127206]
大型言語モデル (LLM) は, CoT (Chain-of-Thought) による数学的問題に対して高い性能を示す
我々は、有向非巡回グラフ(DAG)上の一定の規則に基づくプロセスとしてCoTをモデル化することを提案する。
ここでは,モデルのCoT軌道がDAG構造にどの程度よく依存するかを定量化する計量である論理的近接性を導入する。
論文 参考訳(メタデータ) (2025-10-19T21:05:17Z) - Deterministic Legal Agents: A Canonical Primitive API for Auditable Reasoning over Temporal Knowledge Graphs [0.0]
本稿では,時間的知識グラフの推論のためのセキュアな実行層として設計された形式的プリミティブAPIを提案する。
私たちのフレームワークは、モノリシックなクエリエンジンの代わりに、標準的なプリミティブ、構成可能、監査可能なプリミティブのライブラリを提供します。
このアーキテクチャは不透明な検索を監査可能な推論に変換し、エージェントの内部プロセスをブラックボックスから決定論的プリミティブの検証可能なログに変換する。
論文 参考訳(メタデータ) (2025-10-07T15:04:23Z) - SLICET5: Static Program Slicing using Language Models with Copy Mechanism and Constrained Decoding [13.61350801915956]
静的プログラムスライシングはソフトウェア工学の基本的な技術である。
ourtoolは静的プログラムスライシングをシーケンス・ツー・シーケンスタスクとして再構成する新しいスライシングフレームワークである。
ourtoolは、最先端のベースラインを一貫して上回る。
論文 参考訳(メタデータ) (2025-09-22T03:14:47Z) - Fast Controlled Generation from Language Models with Adaptive Weighted Rejection Sampling [90.86991492288487]
トークンの制約を評価するのは 違法にコストがかかる
LCDは文字列上のグローバル分布を歪め、ローカル情報のみに基づいてトークンをサンプリングすることができる。
我々のアプローチは最先端のベースラインよりも優れていることを示す。
論文 参考訳(メタデータ) (2025-04-07T18:30:18Z) - Representation Disentaglement via Regularization by Causal
Identification [3.9160947065896803]
本稿では,不整合表現学習における基礎となるデータ生成過程の仮定を記述するために,因果コライダー構造モデルを提案する。
そこで本研究では,大規模生成モデルの挙動を因果同定によって課される絡み合った制約に整合させるモジュール型正規化エンジンReIを提案する。
論文 参考訳(メタデータ) (2023-02-28T23:18:54Z) - Training and Inference on Any-Order Autoregressive Models the Right Way [97.39464776373902]
Any-Order Autoregressive Models (AO-ARMs) のファミリは、任意の条件付きタスクにおいてブレークスルーのパフォーマンスを示している。
我々は、AO-ARMの以前の定式化に対して行うべき重要な改善について確認する。
本手法はトラクタビリティを損なうことなく性能を向上する。
論文 参考訳(メタデータ) (2022-05-26T18:00:02Z) - FactGraph: Evaluating Factuality in Summarization with Semantic Graph
Representations [114.94628499698096]
文書と要約を構造化された意味表現(MR)に分解するFactGraphを提案する。
MRは、コアセマンティックの概念とその関係を記述し、文書と要約の両方の主要な内容を標準形式で集約し、データの疎結合を減少させる。
事実性を評価するための異なるベンチマークの実験では、FactGraphは以前のアプローチよりも最大15%優れていた。
論文 参考訳(メタデータ) (2022-04-13T16:45:33Z) - Duality-Induced Regularizer for Semantic Matching Knowledge Graph
Embeddings [70.390286614242]
本稿では, 類似のセマンティクスを持つエンティティの埋め込みを効果的に促進する新しい正規化器(duality-induced RegulArizer (DURA))を提案する。
実験により、DURAは、最先端のセマンティックマッチングモデルの性能を一貫して改善することを示した。
論文 参考訳(メタデータ) (2022-03-24T09:24:39Z) - ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system
description) [0.4893345190925177]
本稿では,飽和式自動定理証明器の勾配押し上げと神経誘導の実装について述べる。
勾配ブースティング法では、論理式のアリティに基づく符号化を考慮し、手動で抽象的な特徴を生成できる。
ニューラルネットワークでは,シンボルに依存しないグラフニューラルネットワーク(GNN)と,その用語や節の埋め込みを用いる。
論文 参考訳(メタデータ) (2020-02-13T09:44:38Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。