Mirage: A Multi-Level Superoptimizer for Tensor Programs

작성일 | In , , |

논문 링크

Q : 이 논문을 아주 자세하게 읽고 논문의 강점과 독창적인 지점을 설명해주고 핵심 알고리즘을 예시 입력을 들어서 전체적인 과정을 설명해줘 추가적으로 논문의 한계점에 대해서도 알려줘

A :

논문 『Mirage: A Multi-Level Superoptimizer for Tensor Programs』를 자세히 분석한 내용을 정리하여 설명합니다.

📌 결론 압축 정리

『Mirage』는 GPU에서 실행되는 텐서 프로그램을 위한 최초의 다계층 슈퍼 옵티마이저로, 커널(kernel), 블록(thread block), 스레드(thread)의 GPU 계산 계층 전체를 아우르는 µGraph라는 새로운 그래프 표현을 사용하여 대규모 탐색 공간을 효과적으로 탐색하고, 기존 방식 대비 최대 2.9배의 성능 개선을 달성하였다.

1️⃣ 논문의 강점 및 독창성

✅ 주요 강점

  • 기존의 옵티마이저와 달리, 커널 수준부터 스레드 수준까지의 모든 레벨을 포괄적으로 최적화 가능
  • 알고리즘 변형(algebraic transformations), 스케줄링(schedule transformations), 그리고 새로운 맞춤형 커널(custom kernels) 생성까지 모두 자동화 가능
  • GPU 메모리 계층을 모두 활용하여, 중간 결과를 device 메모리뿐만 아니라 shared memory와 register file에 효율적으로 배치하여 성능 극대화
  • 추상 표현식(Abstract Expressions) 기반의 가지치기(pruning)를 통해 탐색 공간을 크게 줄이면서 최적성 보장
  • 유한체(finite field)를 활용한 확률적 등가성 검증(probabilistic equivalence verification)으로 정확도 보장

✅ 독창적 기여

  • µGraph라는 새로운 다계층 텐서 프로그램 표현 도입
  • 기존의 Halide, TVM과 같은 스케줄 기반 최적화 및 TASO, PET 등 대수적 변환 기반 최적화를 통합
  • GPU에서의 계산과 메모리 계층(커널, 블록, 스레드)에 따라 프로그램을 세부적으로 표현할 수 있도록 설계
  • 추상 표현식과 SMT solver를 결합하여 탐색 효율성을 극대화한 점

2️⃣ 핵심 알고리즘 및 예시 입력을 통한 설명

Mirage는 크게 세 단계로 최적화를 수행합니다:

  1. µGraph 생성 (Expression-Guided µGraph Generation)
  2. µGraph의 확률적 등가성 검증
  3. µGraph의 추가 최적화(메모리 레이아웃, 스케줄링, 메모리 계획)

아래에서는 예시 입력을 이용하여 핵심 알고리즘 (µGraph 생성 과정)을 설명합니다.

🛠 예시 입력 프로그램

Y = RMSNorm(X, G), \quad Z = MatMul(Y, W)

🔍 Mirage를 이용한 최적화 예시 과정

단계 설명 예시
원본 텐서 프로그램 입력된 텐서 연산 RMSNorm → MatMul
µGraph 생성 새로운 맞춤형 커널 생성, 블록 및 스레드 수준의 그래프 정의 RMSNorm과 MatMul을 하나의 커널 내로 융합
추상 표현식을 이용한 가지치기 추상 표현식에서 벗어난 후보군 삭제 불필요한 중간 연산(X×Y 등)을 가지치기
확률적 등가성 검증 두 µGraph가 동일한 출력을 내는지 랜덤 입력으로 유한체 내에서 검증 여러 번의 랜덤 입력 테스트
추가 최적화 메모리 레이아웃 최적화, 연산자 스케줄링, 메모리 할당 계획 shared memory와 register 활용 극대화

Mirage가 찾아낸 최종 µGraph는 RMSNorm과 MatMul을 완벽히 융합하여 중간 결과를 shared memory 및 register에만 저장해 GPU 메모리 접근 비용을 최소화하여 기존 방법 대비 1.9배(A100), 1.6배(H100) 빠른 성능을 보여주었습니다.

3️⃣ 성능 비교 (기존 접근법 대비 성능 향상)

DNN Benchmark Mirage 성능 향상 (A100) Mirage 성능 향상 (H100)
Group-query Attention 2.2배 2.2배
QK Normalization 1.2배 1.4배
RMSNorm 1.9배 1.6배
LoRA 1.8배 1.7배
Gated MLP 1.5배 2.9배
nTrans 1.8배 2.0배

4️⃣ 논문의 한계점

  • LAX fragment 제한
    Mirage는 multi-linear operator, division, exponential 연산이 하나씩만 사용된 “LAX 프로그램”만 확률적으로 검증이 가능합니다. 따라서 ReLU 등 비선형 연산이 포함된 텐서 프로그램에서는 확률적 등가성 검증이 어렵습니다.

  • 탐색 공간의 크기
    µGraph의 표현력이 강력한 대신 탐색 공간이 매우 큽니다. 추상 표현식으로 가지치기를 하더라도, 프로그램 복잡도 증가에 따라 탐색 시간이 급격히 늘어납니다.

  • 임의 연산자 추가의 한계
    Mirage에서 새로운 연산자를 추가하려면 연산자에 대한 추상 표현식과 유한체 상에서의 구현을 제공해야 하는 번거로움이 존재합니다.

📍 최종 평가 및 활용 가능성

Mirage는 텐서 프로그램의 GPU 최적화 영역에서 기존 접근법과 차별화된 혁신적인 아이디어를 제시합니다. 특히 여러 GPU 계층을 모두 다루는 µGraph는 향후 자동화된 최적화 시스템 구축에 핵심적인 역할을 할 수 있습니다. 그러나, 탐색 공간 제한 및 LAX 프로그램 검증 방식의 한계는 향후 연구에서 추가적인 개선이 요구됩니다. 특히 ReLU와 같은 비선형 연산이 포함된 프로그램의 최적화 방법에 대한 추가 연구가 필요합니다.

종합적으로 Mirage는 GPU 상의 텐서 프로그램 최적화 분야에 새로운 가능성을 열어주었으며, 기존 방법 대비 상당한 성능 향상을 보여줬습니다. 이는 딥러닝 모델의 실행 속도 및 효율성 개선에 매우 큰 영향을 미칠 것으로 기대됩니다.

Q : 논문의 핵심알고리즘을 예시를 들어 아주 자세하게 설명해주고 정리해 줘

A :

논문에서 제시된 핵심 알고리즘인 “µGraph 생성(Expression-Guided µGraph Generation)” 과정을 예시 입력을 바탕으로 단계별로 자세하게 설명하겠습니다.

🧑‍💻 0단계: 핵심 개념 간단 정리

논문의 핵심 아이디어는 GPU의 커널(Kernel), 블록(Thread Block), 스레드(Thread) 계층을 모두 고려한 최적화로, 이를 µGraph라는 다계층 그래프 표현을 통해 자동으로 최적화된 GPU 프로그램을 찾는 것입니다.

µGraph의 구성요소는 다음과 같습니다:

  • Kernel Graph: 여러 GPU 커널 연산자와 Device Memory 간 텐서 이동 표현
  • Block Graph: 각 GPU 커널 내 Thread Block 단위의 연산 표현, Shared Memory 활용
  • Thread Graph: Thread 단위 연산, Register 활용 극대화

🚩 1단계: 예시 프로그램 입력 및 초기 설정

예시로, 다음 텐서 프로그램을 최적화한다고 가정합시다.

💡 예시 프로그램

Y = RMSNorm(X, G), \quad Z = MatMul(Y, W)

이 프로그램의 기본적인 계산 흐름:

  • RMSNorm 연산: 입력 텐서 (X, G)를 정규화하여 텐서 (Y)를 생성
  • MatMul 연산: 생성된 텐서 (Y)를 이용해 가중치 텐서 (W)와 행렬곱 수행하여 텐서 (Z)를 생성

이 과정에서 일반적인 최적화 없이 두 커널로 나누어 수행하면:

  • 중간 텐서 (Y)를 device memory에 저장
  • 두 커널의 연속된 실행으로 인해 높은 메모리 접근 비용 및 커널 시작 비용 발생

🚩 2단계: Kernel Graph 생성 과정

Mirage는 Kernel Graph에서 새로운 맞춤형(Custom) 커널을 생성합니다.

과정 설명 결과
입력 텐서 확인 입력 텐서: (X, G, W) Device Memory에서 관리
Kernel Graph 생성 기존 RMSNorm과 MatMul을 새로운 Graph-defined operator로 융합 (Z = f_{new}(X,G,W))

즉, 기존 두 개의 연산(RMSNorm, MatMul)을 하나의 새로운 맞춤형 커널로 융합하는 단계가 진행됩니다.

🚩 3단계: Block Graph 생성 과정 (핵심)

Kernel Graph로 정의된 새로운 연산자 (f_{new}(X,G,W))는 세부적으로 다시 Block Graph로 나누어 표현됩니다.

이 Block Graph는 각 GPU Thread Block이 실행할 연산을 정의합니다.
다음 요소들이 정의됩니다:

  • Grid Dimensions: Thread Block을 배열하는 방식 결정
  • imap: 입력 텐서를 Thread Block별로 어떻게 나눠줄지 지정
  • fmap: Thread Block 반복(iteration) 간 데이터 접근 방법
  • omap: 출력 텐서를 GPU 메모리에 최종적으로 저장하는 방법

예를 들어 논문의 최적화된 최종 µGraph에서는 다음과 같이 정의되었습니다:

  • Grid Dimensions: [x=128] → 128개 Thread Block 병렬 실행
  • 입력 텐서의 imap 및 fmap 설정:
    • X: 전체 블록에서 복제 (imap: {x↔∅}), 반복 차원 i를 통해 데이터를 분할하여 로딩 (fmap: {i↔h})
    • W: 128개 블록으로 d 차원 분할 (imap: {x↔d})
  • 출력 텐서의 omap 설정:
    • 출력 텐서 Z는 각 블록에서 생성된 결과를 d 차원을 기준으로 GPU 메모리에 병합 저장 (omap: {x↔d})

즉, Block Graph는 다음과 같이 연산 흐름이 구성됩니다:

  1. 입력 iterator가 device memory에서 shared memory로 데이터 로딩
  2. 블록 연산자(예: RMSNorm의 sum, sqrt, div와 MatMul의 연산자들)가 shared memory 데이터를 처리
  3. 결과는 다시 shared memory에 저장 후 for-loop accumulator를 통해 반복(iteration) 결과를 누적

🚩 4단계: Thread Graph 생성 과정 (세부 연산)

각 Block Graph의 연산은 Thread Graph로 더욱 미세하게 나눠져서 각 CUDA Thread가 실행할 연산으로 정의됩니다.

  • Thread Graph는 데이터를 register에서 유지하고 처리합니다.
  • Thread Graph 수준에서는 element-wise 연산(Sqrt, Div 등)을 매우 효율적으로 처리합니다.

예시로 논문의 최적화 µGraph에서 thread graph로 정의된 연산:

  • 각 thread가 Mul → Sqrt → Div 등 element-wise 연산을 연속 수행
  • 연산의 중간 결과를 모두 Register에 저장하여 추가 메모리 접근 최소화

🚩 5단계: Abstract Expression 기반의 Pruning (가지치기)

Mirage는 다음과 같은 추상 표현식(Abstract Expression)을 사용하여 불필요한 그래프를 탐색 중 제거(pruning)합니다.

예시로 주어진 연산에서:

  • 원본 식의 추상 표현식: 
    E(Z) = Matmul(Div(X, RMS(X)), W)
  • 탐색 과정에서 의미 없는 연산(예: X×G, X+W 등)이 등장하면 추상 표현식을 통해 빠르게 제거됩니다.

이 가지치기를 통해 탐색 시간이 크게 줄어듭니다. (실제 논문에서 Abstract Expression을 사용하지 않을 경우 탐색 시간이 급격히 증가함)

🚩 6단계: 확률적 등가성 검증(Probabilistic Equivalence Verification)

추상 표현식에서 살아남은 후보 µGraph들에 대해 유한체(Zp, Zq)를 이용한 확률적 검증을 수행합니다.

  • 랜덤 입력 텐서를 유한체 내에서 생성
  • 원본 µGraph와 후보 µGraph의 결과값이 유한체 내에서 동일한지 검사
  • 반복하여 검사하여 매우 높은 확률로 등가성 검증 (오류율을 원하는 만큼 낮출 수 있음)

이 과정을 거쳐 유효한 최적의 µGraph가 선택됩니다.

🚩 7단계: 추가 최적화 (Tensor Layout, Operator Scheduling, Memory Planning)

최종적으로 선택된 µGraph는 추가적인 최적화를 수행합니다.

  • Tensor Layout 최적화: 메모리에서 텐서의 배치 결정
  • Operator Scheduling: CUDA Thread 내 연산자 실행 순서를 결정 (동기화 최소화)
  • Memory Planning: shared memory, register 활용 극대화를 위한 메모리 할당 전략 수립

이 단계에서 최종적으로 성능이 최대화됩니다.

📌 최종적으로 완성된 µGraph 결과

최종 µGraph는 모든 중간 연산을 커널 내부(shared memory 및 register file)에 유지하며 커널 실행 횟수 및 메모리 접근 횟수를 최소화한 매우 효율적인 GPU 프로그램으로 자동 생성됩니다.

실제 논문의 실험에서 이 방법으로 생성된 µGraph는 기존의 잘 최적화된 접근법 대비 최대 2.9배까지 속도 향상이 달성됨을 검증하였습니다.

위의 과정을 통해 논문의 핵심 알고리즘인 µGraph 생성 과정을 상세히 이해할 수 있습니다.

Q : 이 논문에서 제시한 결과를 자세하게 보고 다른 방법론에 비하여 특출난 점과 논문에서 제기하는 어떠한 방법이 이러한 결과를 도출하게 되었는지 논문에서 제시하는 이유와 너의 생각을 알려줘

A :

논문에서 제시된 『Mirage』의 실험 결과를 기반으로, 기존 방법론 대비 특출난 성과의 원인을 논문에서 언급한 내용과 더불어 분석하여 정리해 드리겠습니다.

📌 1. 논문에서 제시한 실험 결과

Mirage는 대표적인 6가지 DNN 벤치마크를 사용하여 실험하였습니다.
실험에 사용된 GPU는 NVIDIA A100 및 H100이며, 다음과 같은 성능 향상을 보였습니다.

벤치마크 Mirage의 속도 향상 (A100) Mirage의 속도 향상 (H100)
Group-query Attention (GQA) 2.2배 2.2배
QK Normalization (QKNorm) 1.2배 1.4배
RMSNorm 1.9배 1.6배
LoRA 1.8배 1.7배
Gated MLP 1.5배 2.9배
nTrans 1.8배 2.0배

또한 전체 DNN 모델의 end-to-end 성능에서도 1.1배~1.9배의 개선을 보였습니다.

📌 2. 기존 방법론과 Mirage의 비교

논문은 Mirage와 비교한 기존의 두 가지 주요 최적화 방법론을 다음과 같이 구분했습니다.

① 기존의 Algebraic Transformation 기반 접근법 (예: TASO, PET)

  • 한계점:
    • 커널 수준에서만 연산 최적화가 가능
    • 미리 정의된 커널 집합만 탐색하여 제한적 성능 개선
  • Mirage의 차별점:
    • GPU의 커널(kernel), 블록(block), 스레드(thread) 모든 수준을 포괄하는 µGraph를 이용해 탐색 공간이 훨씬 더 넓고 세부적인 최적화 가능

② 기존의 Schedule Transformation 기반 접근법 (예: Halide, TVM, Triton)

  • 한계점:
    • 사용자가 연산 알고리즘을 명시적으로 지정해야 하며, 알고리즘의 근본적 변형 없이 스케줄링만 최적화 가능
  • Mirage의 차별점:
    • 자동으로 새로운 알고리즘 및 맞춤형 커널(custom kernel) 자체를 생성할 수 있어, 수동으로 정의된 알고리즘의 한계를 뛰어넘음

📌 3. Mirage의 특출난 점 (차별성 및 우수성의 원인 분석)

Mirage가 기존 방법 대비 성능적으로 우수한 결과를 얻은 이유는 다음과 같습니다.

🏅 (1) µGraph를 이용한 다계층 최적화의 통합

  • 기존 접근: 커널 or 스케줄 중 하나만 집중하여 최적화 수행
  • Mirage 접근: 알고리즘 변형, 스케줄링, 새로운 맞춤형 커널 생성을 모두 통합적으로 고려하여 수행 → 높은 성능 개선
  • 실제 사례:
    • RMSNorm과 MatMul을 하나의 커널로 융합해 device 메모리 접근과 커널 실행 횟수를 줄임으로써, 1.9배 성능 향상 달성

🏅 (2) 추상 표현식 기반의 효율적인 탐색 (Abstract Expression Pruning)

  • 기존 접근: 탐색 공간이 크기 때문에 많은 시간이 소요되거나 비효율적
  • Mirage 접근: Abstract Expression을 이용해 연산의 유효성을 미리 SMT solver를 통해 검증하여 탐색 공간을 급격히 축소 (최대 2000배 이상 단축)
  • 효과: 성능은 유지하면서 탐색 시간을 크게 단축하여 현실적이고 효율적인 최적화 달성

🏅 (3) GPU 계층 구조의 효율적인 활용 (Memory Planning 및 Layout 최적화)

  • 기존 접근: 주로 device 메모리에만 집중, shared memory나 register 파일 최적화는 제한적
  • Mirage 접근: 중간 데이터를 shared memory 및 register 파일에 최대한 유지함으로써 메모리 접근 비용을 크게 낮춤
  • 실제 사례:
    • Gated MLP에서 두 MatMul을 병렬로 수행하고 shared memory로 연산을 처리해 H100 GPU에서 최대 2.9배 성능 향상

🏅 (4) 확률적 등가성 검증 (Probabilistic Equivalence Verification)

  • 기존 접근: 복잡한 그래프 등가성을 검증하기 어렵거나 제한적인 방법 사용
  • Mirage 접근: 유한체(finite fields)를 사용한 효율적이고 확률적 검증을 통해 신뢰성 높은 자동 검증
  • 효과: 검증 단계에서의 정확성을 높이면서도 빠르게 연산을 수행해 탐색 효율을 극대화

📌 4. 논문에서 제시한 우수성 이유 (논문에서 명시적 언급)

논문에서 Mirage의 우수성 원인을 다음과 같이 강조했습니다.

µGraph 표현을 통해 Kernel, Block, Thread 계층 전체를 일관적으로 표현하고 최적화하여 기존 최적화 기술이 발견하지 못했던 새로운 맞춤형 커널 및 연산 방법론을 발견함으로써 우수한 성능을 얻음. (논문 원문 중 Abstract, Introduction, §2 참고)

즉, Mirage가 기존 방식 대비 우수한 결과를 도출할 수 있었던 핵심 이유는 µGraph의 혁신적인 표현 방식 및 탐색 방법론에 있다고 명시적으로 언급하고 있습니다.

📌 5. 개인적인 분석과 견해 (나의 생각)

저는 Mirage의 성과가 다음의 두 가지 핵심 아이디어에서 비롯됐다고 생각합니다.

  • 다계층 접근의 강력함: 기존의 제한적인 커널 단위, 혹은 스케줄링 단위 접근과 달리 Mirage의 모든 GPU 계층을 통합적으로 접근하는 방법이 높은 성능 개선의 핵심이었다고 생각합니다. 특히 기존 최적화 기술들이 간과한 새로운 커널과 최적화 알고리즘의 자동 생성 능력이 우수한 결과를 도출한 주요 원인이었습니다.

  • 효율적인 탐색 알고리즘: Abstract Expression을 통한 가지치기 기법은 탐색 공간을 극적으로 줄이면서도 이론적 근거를 갖추어 최적성을 보장한 점에서 매우 인상적입니다. 현실적으로 탐색 시간을 수천 배 단축시켜 자동 최적화가 실제 응용 가능한 수준으로 성능을 개선한 핵심 요소입니다.

Mirage의 접근은 앞으로 자동 최적화 기술 연구에 큰 영향을 미칠 것이며, 다계층 최적화 및 효과적인 탐색 공간 관리 방법론이 더욱 중요해질 것으로 예상합니다.

📌 정리 및 결론

Mirage는 기존 최적화 접근법과는 달리 모든 GPU 계층을 통합하여 최적화하며, 새로운 연산자 생성과 효율적인 탐색 방법을 통해 매우 뛰어난 성과를 달성했습니다. 이러한 독창적 방법론이 Mirage의 특출난 성능 결과를 이끌었으며, 앞으로 GPU 최적화 분야에 매우 의미 있는 공헌을 할 것으로 판단됩니다.

Q : 이 논문의 입력데이터와 추론 과정에 대해서 예시를 들어 아주 자세하게 설명해 주겠니? 추가적으로 모델아키텍처의 구성 및 모델을 구성하는 연산과 메모리 요구량 컴퓨팅 요구량 대해서도 설명해줘

A :

논문 『Mirage: A Multi-Level Superoptimizer for Tensor Programs』의 입력 데이터, 추론 과정, 모델 아키텍처 구성, 연산 및 메모리 요구량, 컴퓨팅 요구량을 예시를 들어 아주 상세하게 설명하겠습니다.

✅ 1. 논문의 모델 아키텍처 구성

Mirage의 모델 아키텍처(µGraph)는 GPU 연산의 계층 구조를 따라 3개의 레벨로 구성됩니다.

  • Kernel Graph (커널 레벨)
    여러 개의 GPU 커널 연산들이 device memory의 텐서를 입출력으로 받아 수행하는 최상위 그래프.

  • Block Graph (블록 레벨)
    하나의 GPU 커널을 구성하는 Thread Block들이 수행하는 연산을 표현하는 그래프. Thread Block 단위로 shared memory를 적극 활용.

  • Thread Graph (스레드 레벨)
    하나의 Thread Block 내 각 개별 Thread가 register file을 활용하여 수행하는 연산 그래프. 가장 하위 수준이며 element-wise 연산 수행.

✅ 2. 입력 데이터 예시

예를 들어 Mirage가 다루는 구체적 연산 예시로 논문에서 제시된 RMSNorm + MatMul 최적화 케이스를 사용하겠습니다.

입력 데이터의 예시 텐서:

  • 입력 텐서 ( X ): (예: 16개의 배치, hidden size = 1024) ⇒ shape [batch=16, hidden=1024]
  • 가중치 텐서 ( G ): RMSNorm을 위한 텐서 ⇒ shape [hidden=1024]
  • 가중치 텐서 ( W ): MatMul의 가중치 텐서 ⇒ shape [hidden=1024, dim=4096]

이러한 입력 텐서는 GPU의 device memory에서 유지됩니다.

✅ 3. Mirage의 추론 과정 (상세 단계별 예시)

Mirage가 위의 입력 텐서를 받아 연산을 수행하는 과정은 다음과 같이 진행됩니다.

▶️ (1) Kernel Graph 단계

Kernel Graph는 원본의 두 개 연산자(RMSNorm, MatMul)를 하나의 맞춤형 커널로 융합합니다.

  • 입력 텐서: (X, G, W)
  • 맞춤형 커널의 출력 텐서: (Z) ⇒ shape [batch=16, dim=4096]

커널 융합 효과:

  • 커널 호출 횟수: 2회 → 1회로 감소
  • 중간 텐서의 device memory 접근을 최소화하여 속도 개선

▶️ (2) Block Graph 단계

Kernel Graph에서 정의한 맞춤형 커널을 세부적으로 Block Graph로 표현합니다.

  • Grid dimension: [x=128] ⇒ 128개의 Thread Block 병렬 실행
  • For-loop 반복 횟수: [i=16] ⇒ hidden size(1024)를 16회 나누어 반복

Block Graph 연산 흐름:

  1. Input Iterator: device memory → shared memory로 데이터를 로딩
    • 텐서 (X, G, W)를 각 블록의 shared memory로 로딩
    • imap: 블록마다 텐서 분할 방식 (예: (W) 텐서는 dimension d를 128개 블록으로 나누어 로딩)
    • fmap: 반복(iteration)에서 데이터를 나누는 방식 (예: hidden 차원을 반복마다 나누어 로딩)
  2. 블록 연산자: RMSNorm의 일부 연산 (Square, Sum)과 MatMul 연산 수행
    • shared memory에 저장된 데이터로 각 블록별 연산 수행
    • For-loop accumulator로 반복(iteration) 결과를 shared memory에서 누적
    • 모든 중간 텐서를 shared memory에서 유지하여 device memory 접근 최소화
  3. Output Saver: 연산 완료된 결과를 shared memory → device memory로 이동하여 최종 텐서 구성

▶️ (3) Thread Graph 단계

Block Graph 내 연산을 Thread 단위로 표현하여 각 Thread가 register file에서 연산합니다.

Thread Graph에서의 연산 예시:

  • RMSNorm의 element-wise 연산(Sqrt, Div 등)을 register file을 활용하여 빠르게 수행
  • 중간 결과를 register에서 유지하여 최적의 성능 달성

이로써 shared memory 접근 빈도를 추가로 낮추어 최대의 성능 향상 도모.

✅ 4. 모델 연산의 메모리 요구량 분석

GPU 메모리 계층의 활용 전략 및 요구량:

메모리 유형 역할 용량 및 사용 특성
Device Memory 입력/출력 텐서 및 최종 결과 저장 가장 용량이 크나, 접근 속도가 가장 느림
Shared Memory Thread Block 내 중간 텐서 저장 블록당 수십 KB 사용 가능. 접근속도 빠름(약 10배)
Register File 각 Thread 내 연산 시 중간값 저장 Thread당 수십~수백 개 register, 접근 속도 매우 빠름(약 100배)

예시 연산에서 메모리 활용 예측량:

  • Device Memory:
    • 입력 텐서: (16*1024 + 1024 + 1024*4096)*2바이트(half precision) ≈ 8MB
    • 출력 텐서: (16*4096)*2바이트 ≈ 128KB
  • Shared Memory (Block Graph 기준):
    • 각 블록은 분할된 텐서 조각을 저장
    • 수 KB ~ 수십 KB 수준으로 관리됨
  • Register File (Thread Graph 기준):
    • Thread당 중간 결과 약 수십 바이트 ~ 수백 바이트 수준 관리
    • thread별 제한된 register(~256개)를 활용하여 연산 효율화

✅ 5. 컴퓨팅 요구량 분석 (연산량)

예시 연산 (Z = Matmul(RMSNorm(X,G), W)) 의 연산량을 산출해보면:

  • RMSNorm 계산:
    • 입력 텐서의 제곱 및 합 연산: 대략 16(batch) × 1024(hidden) = 16,384개의 연산
    • element-wise 연산(sqrt, div): 역시 약 16,384개 수준
  • MatMul 계산:
    • (16,1024) × (1024,4096): (16×1024×4096×2 ≈ 134,217,728)개의 곱셈 및 덧셈 연산 수행

총 컴퓨팅 요구량(대략적):

  • 약 1억 3천만 연산 이상이며, 연산이 GPU 계층별로 병렬화되어 처리됨

Mirage는 이러한 계산을 효율적으로 GPU의 계층 구조에 따라 최적화해 높은 연산 처리 속도 달성.

✅ 결론 (Mirage의 최적화 원인 요약)

Mirage는 다음 방법을 통해 탁월한 성능을 구현합니다:

  • Kernel 융합을 통한 Device Memory 접근 최소화
  • Shared Memory 및 Register File을 최대한 활용
  • 각 GPU 계층의 연산을 분할하여 병렬화
  • 메모리 접근 비용을 획기적으로 줄이고 연산을 병렬화하여 성능 극대화

이러한 방법론이 Mirage의 높은 성능 개선을 가능하게 만든 핵심 원인입니다.

이상과 같이 논문의 입력 데이터, 추론 과정, 모델 아키텍처 및 연산, 메모리 요구량, 컴퓨팅 요구량을 예시를 들어 자세하게 설명하였습니다.

Q : 이 논문의 한계를 극복하기 위한 방법으로 어떤 연구흐름이 있는지 정리해서 자세하게 설명해 줘

A :

논문에서 제시된 Mirage의 한계를 명확히 정의하고, 이를 극복하기 위한 연구 흐름을 현재 관련 분야에서 진행 중인 연구 방향 및 구체적인 아이디어로 나누어 설명하겠습니다.

🚩 Mirage 논문에서 명시된 한계점 요약

Mirage가 논문에서 밝힌 주요 한계점은 다음과 같습니다:

Mirage의 한계점 구체적인 설명
LAX Fragment 제한 Mirage의 확률적 등가성 검증 기법이 multi-linear 연산, division, 제한적인 exponential 연산이 포함된 LAX 프로그램으로 제한되어 있음. ReLU와 같은 비선형 연산은 다루기 어려움
탐색 공간의 크기 문제 Mirage의 µGraph는 매우 강력한 표현력을 가지나 그만큼 탐색 공간이 기하급수적으로 증가, 복잡한 프로그램에서는 탐색 시간이 길어짐
신규 연산자 추가의 어려움 새로운 연산자를 Mirage에 추가하려면 추상 표현식 및 유한체 연산을 별도로 제공해야 하므로 추가 연산자를 쉽게 적용하기 어렵다는 제한 존재

🔍 한계 극복을 위한 연구 흐름과 방안

각 한계점을 극복하기 위한 최근의 연구 흐름과 이를 적용 가능한 방안을 구체적으로 설명하겠습니다.

1️⃣ LAX Fragment 제한을 극복하기 위한 연구흐름

Mirage의 확률적 등가성 검증은 multi-linear 연산만을 허용하므로, ReLU 등 비선형 연산에 한계가 있습니다.
이를 극복하기 위한 연구 흐름은 다음과 같습니다:

✅ (1) SMT & Symbolic Verification 기반 접근법 확장

  • 아이디어: 비선형 연산 포함 시 SMT solver 기반의 symbolic verification 접근을 도입하여 수학적 증명을 통해 등가성을 보장.
  • 관련 연구:
    • PET(2021) 논문에서 symbolic verification을 SMT solver로 활용하여 비선형 연산 지원 연구 시도
  • 장점:
    • ReLU 등 비선형 연산에 대해 정확성 증명 가능
  • 단점:
    • 복잡도 증가로 인해 계산 비용이 높아짐
  • Mirage 적용 가능성:
    • 현재 논문에서도 잠시 언급한 solver-based verifier와 결합하여 비선형 연산 지원 가능성을 높임

✅ (2) 근사 등가성 검증(Approximate Equivalence Verification) 연구

  • 아이디어: Floating point 연산의 허용 오차 내에서의 근사적 등가성을 판단하는 기법을 활용
  • 관련 연구:
    • Numerical Equivalence Testing (최근 딥러닝 컴파일러 관련 연구에서 활발히 진행)
    • Monte Carlo 기반의 랜덤 테스트 확장
  • 장점:
    • 비선형 연산 포함한 거의 모든 연산을 빠르게 근사적으로 등가성 검증 가능
  • 단점:
    • 수학적 엄밀성 보장 어려움, 정확도가 떨어질 가능성 존재
  • Mirage 적용 가능성:
    • Mirage에 이 기법을 도입하여 비선형 연산을 근사적으로 포함할 수 있음

2️⃣ 탐색 공간 크기 문제 극복을 위한 연구흐름

µGraph의 표현력이 높을수록 탐색 공간도 크게 증가합니다.
이를 극복하기 위해 최근 연구들은 다음 접근법을 사용하고 있습니다:

✅ (1) 머신러닝 기반의 탐색 공간 탐색 최적화(ML-guided Search)

  • 아이디어: 기존의 rule-based 또는 exhaustive search 대신 머신러닝(강화학습)을 이용하여 최적의 µGraph를 빠르게 탐색.
  • 관련 연구:
    • TVM의 Ansor(2020), TensorIR(2022): ML 기반의 자동 탐색 기법 사용
  • 장점:
    • 탐색 시간을 극적으로 단축하고 성능을 유지
  • 단점:
    • ML 모델 학습이 필요하며 초기 학습 시간이 소요됨
  • Mirage 적용 가능성:
    • Mirage의 abstract expression과 ML 탐색을 결합하면 더 빠르고 효율적인 탐색 가능

✅ (2) 계층적 탐색 기법(Hierarchical Search) 연구

  • 아이디어: 탐색 공간을 계층적으로 나누어 하위 수준 탐색 결과를 기반으로 상위 수준 탐색을 수행하는 전략
  • 관련 연구:
    • Welder(2023), ASPEN(2023) 등 계층적 최적화를 이용해 단계별로 점진적 탐색 공간 축소
  • 장점:
    • 높은 표현력 유지하면서도 탐색 비용 감소
  • 단점:
    • 계층 설계가 복잡해질 수 있음
  • Mirage 적용 가능성:
    • 이미 Mirage가 kernel, block, thread 수준으로 계층 구조를 가지고 있으므로 더욱 정교한 계층적 탐색 전략 도입 가능

3️⃣ 신규 연산자 추가의 어려움을 극복하기 위한 연구 흐름

Mirage는 신규 연산자 추가 시 abstract expression과 유한체 구현을 요구합니다.
이러한 부담을 낮추기 위한 연구 흐름은 다음과 같습니다:

✅ (1) 자동화된 연산자 추가 프레임워크(Auto-Operator Integration)

  • 아이디어: 연산자의 정의만으로 자동으로 abstract expression 및 verification code를 생성하는 툴 제공
  • 관련 연구:
    • TVM, XLA 등 컴파일러 생태계에서 자동 연산자 추가를 위한 IR(intermediate representation) 추상화 연구 활발
  • 장점:
    • 연산자 추가 부담 감소, 높은 확장성
  • 단점:
    • 추상화 설계 및 구현에 초기 개발 비용 존재
  • Mirage 적용 가능성:
    • Mirage 프레임워크 내부에 자동 IR 생성 기능을 도입하여 쉽게 신규 연산자 추가 가능하게 함

✅ (2) 연산자 표준화 및 추상화 계층 추가(Operator Standardization)

  • 아이디어: 범용적인 연산자 세트(Convolution, Activation, Normalization 등)를 미리 정의하고, Mirage가 이를 기반으로 확장 가능한 구조 제공
  • 관련 연구:
    • MLIR, TVM Relay 등 컴파일러 프레임워크에서 표준 연산자 라이브러리 제공
  • 장점:
    • 표준 연산자 정의로 연산자 추가 용이성 향상
  • 단점:
    • 새로운 혁신적 연산자 적용 시 약간의 제한 발생 가능성
  • Mirage 적용 가능성:
    • Mirage의 µGraph 구조에 연산자 표준화를 일부 도입하면, 새로운 연산자의 추가 부담이 크게 낮아짐

🧑‍🔬 결론 (한계를 극복하는 연구 흐름 요약)

Mirage가 가진 한계는 다양한 방향에서 활발히 연구 중이며, 주요 연구 흐름을 요약하면 다음과 같습니다:

  • 비선형 연산 지원: SMT 기반 symbolic verification, Approximate verification 방법 연구
  • 탐색 공간 축소: ML-guided 탐색 전략, 계층적 탐색 기법 연구
  • 신규 연산자 추가 용이성: 자동 연산자 추가 프레임워크, 연산자 표준화 및 추상화 계층 제공 연구

위 연구 흐름을 Mirage에 접목하면 Mirage의 현존 한계를 극복하고, 더 범용적이며 효율적인 GPU 텐서 프로그램 최적화 시스템으로 발전 가능할 것입니다.

Q : Mirage가 사용하는 µGraph의 핵심적인 아이디어와 기존 최적화 기법(예: Halide, TVM, TASO 등)과의 구체적인 차별점은 무엇인가요?

A :

Mirage가 사용하는 µGraph의 핵심적인 아이디어와 기존 최적화 기법과의 구체적인 차별점은 다음과 같습니다.

  1. µGraph의 핵심적인 아이디어:

Mirage의 µGraph는 GPU에서 실행되는 텐서 프로그램을 최적화하기 위해, GPU의 세 가지 핵심 계층 구조(Kernel, Thread Block, Thread)를 모두 포함하는 통합된 표현 방식을 사용합니다. µGraph는 각 계층에서 수행되는 연산과 데이터 이동을 일관된 형태로 나타내며, 특히 Device Memory, Shared Memory, Register File의 계층적 메모리 구조를 효율적으로 이용합니다. 이를 통해 Mirage는 단순히 연산 스케줄링이나 알고리즘 변형 중 하나만 최적화하는 것이 아니라, 이 모든 요소를 통합적으로 고려하여 전체 GPU 실행 효율을 극대화합니다.

  1. 기존 최적화 기법과의 구체적인 차별점:

  • Halide 및 TVM과의 차별점: Halide와 TVM은 “알고리즘(무엇을 계산할지)”과 “스케줄(어떻게 계산할지)”을 명확히 분리한 최적화 방식을 따릅니다. 이러한 방식에서는 사용자가 반드시 연산 알고리즘을 미리 정의해야 하며, 주어진 알고리즘을 어떤 순서와 방식으로 실행할지를 스케줄링하는 것에만 중점을 둡니다. 반면, Mirage는 알고리즘과 스케줄링의 명확한 구분 없이 둘 모두를 동시에 고려하여 자동으로 최적의 새로운 맞춤형 커널 및 알고리즘을 찾아냅니다.

  • TASO와의 차별점: TASO는 텐서 연산 간의 algebraic transformation(대수적 변환)에 초점을 맞추어, 연산 그래프를 kernel 수준에서만 최적화합니다. 하지만 TASO는 사용자가 제공하는 미리 정의된 커널 연산 집합 내에서만 변환을 수행하므로, 커널 수준 이외의 세부적인 GPU 메모리 계층(shared memory, register)을 활용한 추가적 최적화는 하지 못합니다. Mirage는 TASO의 algebraic transformation에 추가로 GPU의 메모리 계층 전반을 다루는 새로운 맞춤형 커널 생성 및 스케줄링을 통합적으로 수행하여, 기존 접근법이 찾지 못한 훨씬 더 세부적이고 효율적인 최적화 기회를 발견합니다.

정리하면, Mirage의 µGraph는 기존 최적화 방식들이 개별적으로 다루던 “알고리즘 변형(algebraic transformations)”과 “스케줄 최적화(schedule optimizations)”, 그리고 “커널 생성(custom kernel generation)”을 모두 단일한 통합 구조에서 다루는 것이 핵심적인 차별점이자 장점입니다. 이로 인해 Mirage는 기존 접근법 대비 크게 향상된 GPU 실행 성능(논문에서 최대 2.9배 향상)을 달성할 수 있었습니다.

Q : Mirage가 제시한 Abstract Expression 기반의 탐색 공간 가지치기 기법은 구체적으로 어떻게 탐색 공간을 줄이고, 동시에 최적성을 보장할 수 있는지 자세히 설명해 줄 수 있나요?

A :

Mirage에서 제안한 Abstract Expression 기반의 탐색 공간 가지치기(Pruning) 기법은 다음과 같은 원리로 작동하여 탐색 공간을 효과적으로 줄이면서도 최적성을 보장할 수 있습니다.

  1. Abstract Expression (추상 표현식)의 개념과 역할:

Mirage의 탐색 과정에서는 수많은 연산 조합(µGraph 후보)을 검토해야 합니다. 이때 불필요한 탐색을 최소화하기 위해, 구체적인 값 대신 연산의 수학적 특성을 추상화하여 표현하는 방식을 사용합니다. 이를 “Abstract Expression”이라고 부릅니다.

추상 표현식은 실제 입력값이나 텐서의 구체적 요소(element) 값을 고려하지 않고, 연산 자체의 형태와 특성만을 논리적이고 기호적인 형태로 표현한 것입니다.

예를 들어,

  • MatMul(A, B) → sum(k, mul(A, B))
  • Div(A, B) → div(A, B)
  • Add(A, B) → add(A, B)
  • Exp(A) → exp(A)

이처럼 수학적 연산을 기호적으로만 표현하여 서로 다른 실제 연산의 경우에도 동일하거나 유사한 형태의 추상 표현식을 가지면 유사성을 빠르게 판단할 수 있습니다.

  1. 가지치기(Pruning) 기법의 작동 원리:

Mirage는 µGraph를 탐색하면서, 다음의 가지치기 원칙을 적용합니다.

  • 탐색 중인 연산 조합(µGraph의 중간 단계)이 입력 텐서 프로그램이 목표로 하는 연산 결과와 무관한 연산 형태를 가지는 경우, 더 이상 그 하위 탐색을 진행하지 않고 즉시 제거(가지치기)합니다.

  • 탐색 과정에서 만들어진 µGraph의 중간 연산 결과를 Abstract Expression으로 표현하고, 이것이 최종 목표 연산의 Abstract Expression의 부분 표현식(Subexpression)에 해당하는지 빠르게 확인합니다.

  1. 최적성 보장을 위한 조건과 논리적 근거:

Mirage는 Abstract Expression을 SMT(Satisfiability Modulo Theories) Solver라는 논리적 정리 증명 도구로 확인합니다. 구체적으로, 아래와 같은 원칙에 의해 최적성을 보장합니다.

  • 연산을 추가할 때마다 Abstract Expression은 항상 더 복잡해지며, 새로운 연산을 추가할 경우 기존 표현식의 부분 표현식(subexpression)이 되어야 합니다.
  • 즉, 최종적으로 목표하는 연산과 무관한(부분 표현식이 아닌) 중간 연산은 아무리 연산을 더 추가해도 결코 목표 연산의 부분 표현식이 될 수 없습니다. 따라서 이들을 제거하더라도 최적해(최적 µGraph)를 잃어버리지 않습니다.

구체적 예시로 설명하면 다음과 같습니다.

목표 연산이 다음과 같다고 할 때:

목표연산: MatMul(A,B) + MatMul(C,D)

이를 Abstract Expression으로 표현하면:

add(sum(k, mul(A,B)), sum(k, mul(C,D)))

만약 탐색 중 다음과 같은 형태가 나타나면 유지할 가치가 있습니다:

sum(k, mul(A,B)) 또는 sum(k, mul(C,D))

(부분 표현식이므로 추가 연산을 통해 목표식으로 발전 가능)

반면, 다음과 같은 형태는 제거됩니다:

sum(k, mul(A,C)), div(A,B)

(이는 목표식의 부분 표현식이 아니므로 향후 어떤 추가 연산을 붙여도 목표식으로 발전 불가능)

  1. Abstract Expression을 이용한 탐색 효율성 증가 효과:

이러한 방식으로 Mirage는 탐색 과정에서 최종 연산 결과와 무관한 수많은 탐색을 조기에 제거하여, 탐색 공간의 크기를 매우 효율적으로 줄입니다. 논문에서도 이 방법이 없으면 탐색 시간이 수백 배에서 수천 배 증가한다고 보고하고 있습니다.

  1. Mirage에서 최적성을 보장하는 근거와 논리적 증명:

Mirage는 Abstract Expression의 “부분 표현식 관계(subexpression relation)”와 “연산 추가 시 Abstract Expression의 단조적 증가(monotonic increase)” 특성을 이용하여 다음과 같은 이론적 보장(Theorem)을 제공합니다:

  • 만약 최적의 µGraph가 존재한다면, 이 µGraph는 목표 연산의 Abstract Expression과 동등(equivalent)해야 합니다.
  • 따라서 Abstract Expression으로 가지치기를 하더라도 최적 µGraph를 결코 잘라내지 않으며, 최적성(optimality)을 항상 유지합니다.

정리하면, Mirage의 Abstract Expression 기반의 가지치기 기법은 탐색 공간을 매우 효과적으로 축소하면서도, 논리적이고 기호적인 부분 표현식 관계를 통해 최적성을 엄밀히 보장할 수 있습니다. 이러한 독특한 접근법이 Mirage가 기존 방법 대비 압도적으로 효율적이면서도 정확한 최적화 결과를 찾을 수 있는 핵심 요인입니다.

Q : Mirage에서 사용된 Probabilistic Equivalence Verification (확률적 등가성 검증)이 기존의 등가성 검증 방법들과 비교하여 어떤 이점을 가지며, 특히 비선형 연산이 포함된 경우에는 어떤 한계가 있는지 구체적인 예시를 들어 설명해 줄 수 있나요?

A :

Mirage에서 사용된 확률적 등가성 검증(Probabilistic Equivalence Verification)의 기존 방법과 비교한 이점과 한계를 명확히 정리하여 설명드리겠습니다.

  1. Mirage가 제안한 확률적 등가성 검증 방법 (Probabilistic Equivalence Verification)이란?

Mirage는 두 텐서 프로그램이 정확히 동일한 결과를 산출하는지 검증하는 문제를 해결하기 위해, 유한체(Finite Field) 내에서 랜덤 입력값을 통해 두 프로그램을 실행하고 그 결과를 비교하는 방식을 사용합니다. 이를 통해 두 프로그램이 수학적으로 등가임을 매우 높은 확률로 보장할 수 있습니다.

구체적인 과정은 다음과 같습니다:

  • 두 개의 큰 소수(prime number) p, q를 선정하여 두 유한체(Z_p, Z_q)를 구성
  • 이 유한체 내에서 입력 데이터를 랜덤하게 생성
  • 두 텐서 프로그램을 유한체 내에서 실행하여 결과값을 비교
  • 여러 번 반복 수행하여 등가성을 높은 신뢰도로 검증 (확률적으로 보장)

예를 들어 다음 두 프로그램이 있다고 가정합시다:

  • 프로그램 A: (X + Y) × Z
  • 프로그램 B: (X × Z) + (Y × Z)

이 두 프로그램은 수학적으로 정확히 같은 연산을 수행합니다. Mirage는 두 프로그램의 입력 (X,Y,Z)을 유한체(Z_p,Z_q) 내에서 랜덤으로 선정하여 각각의 출력을 비교해 정확한 등가성을 확률적으로 보장할 수 있습니다.

  1. 기존의 등가성 검증 방법과 비교한 Mirage 확률적 방법의 이점:

  • 속도 및 효율성: 기존의 Symbolic (기호적) 방법론은 복잡한 수학적 표현을 solver를 통해 증명해야 하므로 연산이 복잡해질수록 시간이 급격히 증가합니다. 반면 Mirage의 확률적 등가성 검증 방법은 간단한 연산을 랜덤 입력을 통해 반복적으로 수행하면 되기 때문에, 복잡한 프로그램의 경우에도 검증 속도가 매우 빠릅니다.

  • 확장성: 기존 방식은 새로운 연산이 추가될 때마다 solver가 사용할 추가적인 수학적 정의를 제공해야 하는 어려움이 있습니다. 하지만 Mirage 방식은 단순히 유한체 내에서 연산 정의만 제공하면 되기 때문에, 새로운 연산 추가가 비교적 쉽습니다.

  • 이론적 정확성 보장: 유한체 내에서 검증을 여러 번 반복하면 잘못된 프로그램이 정확한 프로그램으로 잘못 판정될 확률을 원하는 만큼 작게 줄일 수 있습니다. 즉, 이론적으로는 100%에 매우 가까운 정확성을 확보할 수 있습니다.

  1. Mirage 방식의 한계 (비선형 연산 포함시 문제):

Mirage의 확률적 등가성 검증 방식은 “LAX Fragment”라는 제한된 범위에서만 엄밀하게 적용 가능합니다. 이 범위는 다음과 같은 연산들만 포함합니다:

  • Multi-linear 연산 (MatMul, Convolution 등 선형 연산)
  • Division 연산
  • 제한적 사용(각 연산 경로당 한 번 이하)의 지수함수(exp 연산)

이 범위를 벗어난 연산, 특히 ReLU와 같은 비선형 연산이 포함된 경우는 Mirage의 확률적 검증이 제대로 적용되지 못하는 한계를 갖습니다.

예를 들어 다음 두 프로그램을 살펴봅시다:

  • 프로그램 A: ReLU(X) + ReLU(Y)
  • 프로그램 B: ReLU(X + Y)

두 프로그램은 완전히 다르며, 입력 값에 따라 결과가 크게 달라질 수 있습니다. Mirage의 유한체 내에서의 연산은 덧셈, 곱셈, 나눗셈 등 필드 연산 위주이기 때문에 비선형 연산(ReLU)을 정확히 표현할 수 없습니다. 유한체 내에서 ReLU는 의미가 없으며, Mirage는 이런 비선형성을 제대로 다룰 수 없기 때문에, 이러한 비선형 연산 포함시 등가성 검증이 어렵습니다.

  1. 이러한 한계를 극복하기 위한 연구 흐름:

이러한 비선형 연산 문제를 극복하기 위해 최근 연구들은 다음 두 가지 접근법을 주로 사용합니다:

(1) Approximate Numeric Verification (근사적 수치 검증 방법):

  • Floating point 환경에서 허용 오차 이내의 근사적 등가성 검증을 수행
  • Monte Carlo 방식으로 랜덤한 입력 데이터를 통해 두 연산 결과를 오차 범위 내에서 근사적으로 비교하는 방식
  • Mirage 방식과 유사한 효율성으로 비선형 연산 처리 가능, 하지만 수학적 엄밀성을 다소 잃게 됨

(2) SMT/Symbolic Verification:

  • 비선형 연산 포함 프로그램의 수학적 속성을 SMT solver를 통해 증명
  • PET 등 일부 시스템에서 연구된 방식
  • 정확성은 매우 높지만 계산 복잡도가 크게 증가하여 성능상의 단점이 존재
  1. 정리:

Mirage에서 제안한 확률적 등가성 검증 방식은 기존의 symbolic verification에 비해 매우 빠르고 효율적이며, 이론적으로도 강력한 정확성을 보장할 수 있습니다. 하지만 “비선형 연산” 포함 시, 유한체 기반의 이 접근법은 그 한계가 명확히 드러납니다. 이러한 비선형 연산의 문제를 극복하려면 근사적 검증 또는 SMT-based symbolic 검증과 같은 다른 방법과 결합하는 하이브리드 방식이 향후 가장 유망한 접근법으로 생각됩니다.