Operator Semantic Properties Catalog ( AICF Semantic Optimization Rules)

Overview

AICF 는 연산의 수학적 성질을 이용하여 의미를 보존하면서 실행 전략을 변경하는 컴파일러를 목표로 한다.

이를 위해 각 연산은 다음과 같은 Semantic Property 를 가질 수 있다.

Operator
   ↓
Semantic Properties
   ↓
Allowed Transformations
   ↓
Execution Strategy

즉, 최적화는 단순한 패턴 매칭이 아니라.

연산의 수학적 불변성 invariance 를 이용한 변환

으로 정의된다.

 

1. Associativity

Definition

연산 순서를 변경해도 결과과 동일한 성질

(a ⊕ b) ⊕ c = a ⊕ (b ⊕ c)

Optimization

가능한 실행 전략

• tree reduction
• block reduction
• warp reduction

Σ a_i
↓
parallel reduction

Used in

• Sum
• Mean
• Dot product
• GEMM accumulation

 

2. Commutativity

Definition

연산 순서를 바꿔도 결과가 동일

a ⊕ b = b ⊕ a

Example

a + b = b + a

 Optimization

• operand reorder
• paralled scheduling

예

thread scheduling redorder

Used in

• Add
• Multiply
• Reduction

 

3. Permutation Invariance

Definition

입력 순서가 결과에 영향을 주지 않음

f(x1, x2, x3) = f(x3, x1, x2)

Example

Reduction

Σ a_i

순서 무관

Optimization

가능한 변환

• tile reorder
• chunk reorder
• asynchronous pipeline

GEMM example

C[i,j] = Σ_k A[i,k] * B[k,j]

k 순서 변경 가능

k tile order
0 1 2 3
=
2 0 3 1

 

4. Shift Invariance

Definition

입력에 상수를 더하거나 빼도 결과가 동일

f(x) = f(x - c)

Example

Softamx

softmax(x)
=
softmax(x - max(x))

Optimization

• numerical stabilization
• streaming reduction

Used in

• Softmax
• LogSumExp

 

5. Linearity

Definition

연산이 선형성을 가질 때

f(a + b) = f(a) + f(b)

또는

f(ca) = c f(a)

Example

Matrix multiplication

A(B + C)
=
AB + AC

Optimization

• operation fusion
• algebraic rewrite

예

GEMM + bias
↓
GEMM epilogue

 

6. Idempotence

Definition

같은 연산을 여러 번 적용해도 결과 동일

f(f(x)) = f(x)

Example

ReLU

ReLU(ReLU(x)) = ReLU(x)

Optimization

• redundant op removal

예

ReLU
ReLU
->
ReLU

 

7.Domain Pruning

Definition

입력 영역 일부에서 결과가 고정됨

Example

ReLU

x ≤ 0 → output = 0

Optimization

가능한 전략

• early exit
• sparse propagation
• conditional compute skip

예

if x ≤ 0
skip compute

 

8. Monotonicity

Definition

입력이 증가하면 출력도 증가

x1 ≤ x2 → f(x1) ≤ f(x2)

Example

ReLU

x1 < x2
ReLU(x1) ≤ ReLU(x2)

Optimization

• bounds propagtaion
• pruning

예

range analysis

 

9. Streaming Compatibility

Definition

전체 데이터를 보지 않고 부분 계산 가능

f(x1, x2, x3, ...)
=
update(state, xi)

Example

Online softmax

running max
running sum

Optimization

• streaming algorithms
• tiled execution

Used in

• FlashAttention
• online reduction

 

10. Tile Compatibility

Definition

연산이 블록 단위로 분할 가능

f(A) =
combine(f(A_tile))

Example

GEMM

C_tile += A_tile * B_tile

Optimization

• tiling
• shared memory blocking

 

Summary Table

Associativity	Sum	parallel reduction
Commutativity	Add	operand reorder
Permutation invariance	GEMM reduction	tile reorder
Shift invariance	Softmax	stable softmax
Linearity	GEMM	fusion
Idempotence	ReLU	redundant removal
Domain pruning	ReLU	compute skip
Monotonicity	ReLU	bounds analysis
Streaming compatibility	Softmax	online algorithm
Tile compatibility	GEMM	tiling

 

AICF Core Principle

AICF 에서 최적화는 다음 형태로 정의된다.

Operator
   ↓
Semantic Properties
   ↓
Allowed Transformations
   ↓
Execution Strategy

즉

최적화는 heuristic 이 아니라 수학적 불변성에 기반한다.