형식 이론(Formal Theories)의 관점에서 본 MLIR 내 AI 모델 컴파일 읽기

MLIR과 같은 컴파일러 인프라(Compiler infrastructures)는 IR 추상화(IR abstractions), 인터페이스(interfaces), 매치 앤 리라이트(match-and-rewrite), 흐름 분석(flow analysis), 타입 변환(type conversion), 단계적 로워링(staged lowering) 등 일련의 설계 원칙에 기반합니다. 이러한 개념들은 실무에서 그 효용성이 입증되었습니다. 훌륭한 설계는 일반적으로 엔지니어링 지식, 직관 및 경험을 통해 도출됩니다. 그러나 이들 중 상당수는 형식 이론(formal theory)과 대응 관계를 가집니다. MLIR의 매치 앤 리라이트(match-and-rewrite) 엔진은 항 재작성 시스템(term-rewriting-system)~ extcite{baadernipkow1998}과 대응되며, 단계적 로워링(staged lowering)은 정제 계산(refinement calculus)~ extcite{back1998}의 구조를 가지고, 범위 분석(range analysis)은 추상 해석(abstract interpretation)~ extcite{cousot1977,cousot1979}에 근거를 두고 있습니다. 이러한 대응 관계를 강조하는 것은 유익한데, 각 이론이 구조적 문제를 논의하기에 충분히 정밀한 어휘를 제공하기 때문입니다. 더욱이, 코딩 에이전트(coding agents)가 구현 비용을 낮춤에 따라, 훌륭한 설계와 추상화가 주요 관심사가 되고 있습니다~ extcite{Lattner2026ClaudeCCompiler}. 코딩 에이전트는 패스(pass)를 생성할 수 있지만, 표현(representation)이 노출하는 의미론(semantics)에 대해서만 추론할 수 있습니다. 필수적인 구조가 누락되었을 때, 그 한계는 구현의 문제가 아니라 추상화의 문제입니다. 자연스러운 다음 질문은 그러한 기질(substrate)을 어떻게 잘 설계할 것인가 하는 점입니다. 잘 선택된 추상화는 경험과 직관에서 나오지만, 종종 형식 이론에서 더 정밀하게 다뤄지는 개념들을 반영합니다. 우리는 이러한 형식적 개념에 대한 지식이 주어진 추상화에 대해 완전성(completeness)이 무엇을 의미하는지, 이상적인 설계는 무엇인지, 그리고 실제적인 트레이드오프(trade-offs)가 어디에서 벗어나는지를 명확히 해준다고 주장합니다.