텐서 대수적 속성 스켈레톤: AI 컴파일러를 위한 속성 기반 테스트 증폭

TVM 및 ONNX-MLIR과 같은 딥러닝 (DL) 컴파일러는 텐서 계산 그래프 (tensor computation graphs)를 타겟 백엔드에 최적화된 실행 파일로 낮춥니다 (lower). 이러한 AI 컴파일러를 테스트하는 작업은 퍼징 (fuzzing) 맥락에서 잘 형성된 입력값 (well-formed inputs)을 생성하는 측면에서 상당한 진전을 이루었습니다. 그러나 이러한 생성 방식만으로는 그래프 변환 (graph transformations) 및 최적화 (optimizations) 과정에서 보존되어야 하는 대수적 불변량 (algebraic invariants)으로부터 발생하는 의미론적 드리프트 (semantic drifts)를 포착하지 못합니다. 텐서 대수 (tensor algebra)는 수십 년 동안 연구되어 왔지만, 이를 DL 컴파일러를 위한 실행 가능한 속성 기반 테스트 (Property-Based Tests, PBTs)로 변환하는 것은 연산자 (operators), 입력값 (inputs), 그리고 테스트 오라클 (test oracles)을 공동으로 구축해야 하기 때문에 이루어지지 않았습니다. 핵심 과제는 더 이상 DL 컴파일러를 위한 퍼징용 잘 형성된 입력값을 생성하는 것이 아니라, 텐서 대수에 기반한 입력값과 오라클을 사용하여 실행 가능한 PBT를 부트스트래핑 (bootstrapping)하는 것입니다. 우리는 GPT 5.5를 활용하여 DL 컴파일러를 위한 LLM 기반 에이전트형 속성 기반 테스트 프레임워크인 Propilot을 통해 이 비전을 실현합니다. 첫째, Propilot은 텐서 대수 지식을 재사용 가능한 속성 스켈레톤 (property skeletons)으로 표현하며, 각 스켈레톤은 연산자 제약 조건 (operator constraints), 형상 및 값 규칙 (shape and value rules), 그리고 오라클 템플릿 (oracle templates)과 결합됩니다. 둘째, 타겟 컴파일러가 주어지면, Propilot은 쌍을 이루는 텐서 계산 그래프, 구체적인 텐서 입력값, 그리고 오라클로서의 기대되는 의미론적 관계를 생성함으로써 이러한 스켈레톤을 실행 가능한 PBT로 인스턴스화 (instantiates)합니다. 다음으로, 생성된 테스트가 유효하지 않거나 정보가 없는 PBT로 퇴화하는 것을 방지하기 위해, Propilot은 실행 전 각 PBT 후보의 적용 가능성과 안전성을 검증합니다. 검증 피드백, 실행 결과, 그리고 커버리지 (coverage) 신호는 후속 생성을 안내합니다. 우리는 212개의 연산자와 20개의 속성 스켈레톤을 사용하여 TVM에서 Propilot을 평가하였으며, 4,579개의 PBT를 생성했습니다. 직접적인 LLM 기반 PBT 생성과 비교했을 때, Propilot은 중복성을 49% 줄이고 명시적인 속성 스켈레톤을 통해 유효하지 않은 테스트를 제거합니다. 이러한 효과는 의미론적 오류 (semantic errors)와 수치적 불일치 (numerical discrepancies)를 찾아내는 것으로 이어집니다.