Doctoral Thesis Proposal - Bohan Hou
November 5, 2026 3:00PM—4:30PM
Location:
8102
-
Gates and Hillman Centers
Speaker:
BOHAN HOU,
Ph.D. Student, Computer Science Department, Carnegie Mellon University
https://spectrometerhbh.github.io/
High-performance machine learning (ML) kernels require control over computation schedules, data placement, parallel execution, and specialized hardware instructions. As accelerators evolve, optimizing kernels demands growing engineering effort. This thesis studies compiler abstractions that improve performance and programming productivity while supporting automation and correctness for human developers and agents.
The completed research develops two compiler foundations. TensorIR introduces computation blocks and scheduling primitives for manually constructing tensorized programs and automatically exploring optimization spaces using human-validated transformations. MetaSchedule builds on these interfaces, while Relax and MLC-LLM use TensorIR as a kernel compilation foundation. TIRx introduces execution scopes, tensor layouts, and tile-primitive dispatch to expose hardware control on Hopper, Blackwell, and heterogeneous accelerators while automating recurring implementation tasks. Event Tensor extends tile programming to dynamic megakernels, and TIRx Harness enables agent-driven kernel generation and optimization.
Unlike traditional autotuning within predefined optimization spaces, agents can generate kernels with unanticipated execution strategies and numerical optimizations. Their growing productivity makes correctness review a bottleneck: testing and concrete execution checks cannot establish correctness for all valid inputs and GPU executions. The proposed research develops proof-producing verification of TIRx kernels. We will formalize TIRx program states, execution transitions, and functional correctness in Lean. A stable semantic core determines what execution and correctness mean, while proof strategies adapt to individual implementations. Agents will construct machine-checkable proofs of full functional correctness for unmodified kernels, using reusable algorithmic and hardware lemmas. The framework targets symbolic shapes, arbitrary input data, data-dependent control flow, and permitted asynchronous and weak-memory behaviors without relying on a predefined optimization space. When necessary, agents may introduce explicit, human-reviewable assumptions for specialized optimizations. Arithmetic is modeled over mathematical real numbers, excluding finite-precision rounding analysis.
Our ultimate goal is to verify the supported high-performance implementations in TIRx-kernels, assessing whether agent-generated proofs can reduce manual correctness review while preserving kernel performance.
Thesis Committee
Tianqi Chen (Chair)
Zhihao Jia
Tim Dettmers
Zhijian Liu (University of California San Diego)
Contact
Matt Stewart