ProCerDCL: 딥러닝 컴파일러 최적화의 질의 효율적인 블랙박스 확률론적 검증

저희는 블랙박스 확률론적 검증을 위한 질의 효율적인 프레임워크인 \tool를 제시합니다. 고정되고 샘플링 가능한 입력 분포와 이진 속성 오라클(binary property oracle)이 주어지면, \tool는 주어진 임계값 $\theta$에 대해 해당 속성의 위반 확률 $p$를 평가합니다. 독립적인 샘플링과 상태 비저장형 오라클 동작 하에서, 수용(acceptance)은 $p\le\theta$임을 주장하고, 거부(rejection)는 사용자가 지정한 분리 마진 $\eta$에 대해 $p>\theta+\eta$임을 주장하며, 결론을 내릴 수 없는 판정(inconclusive verdict)은 어느 쪽 결론에도 충분한 증거가 부족함을 나타냅니다. 각 유형의 오류 판정 확률은 지정된 오류 예산(error budget)으로 경계 지어집니다. 이 세 가지 값(three-valued contract)을 효율적으로 지원하기 위해, \tool는 단일 순차 테스트를 사용함으로써 베이스라인이 요구하는 구간 계열(interval family)을 제거합니다. 이 테스트는 수정된 정확한 이항 신뢰 구간(corrected exact binomial confidence intervals) 또는 언제든지 유효한 신뢰 시퀀스(anytime-valid confidence sequence)를 통해 반복 샘플링 검사를 처리합니다. 저희는 \tool를 확률론적 로컬 모델 의미론적 일관성(probabilistic local model semantic consistency)에 적용했는데, 여기서 속성 오라클은 지정된 교란 분포 하에서 참조 실행과 컴파일된 실행 간의 결정 수준 불일치(decision-level inconsistencies)를 감지합니다. 저희 평가는 TorchInductor와 TensorRT 전반에 걸쳐 24개의 태스크를 다루었으며, 샘플링 효율성, 결론 도출 가능성, 진단적 동작을 검토했습니다. 샘플링 효율성의 경우, 쌍으로 이루어진 단일 모델 클린 레이블 반경 검색(paired one-model clean-label radius searches)을 사용했는데, 베이스라인은 더 약한 결정 계약을 제공하면서도 일치하는 수치 매개변수 하에서 3.6~4.2배 더 많은 고유 샘플이 필요합니다. 모델 의미론적 일관성 검사에서는 $\theta=10^{-3}$일 때, 21개 태스크의 840개 입력-백엔드 인스턴스를 거쳐 817개의 수용 판정, 19개의 결론 불가 판정, 그리고 4개의 거부 판정이 나왔습니다. 또한 문서화된 두 가지 컴파일러 결함에 대한 사례 연구는 이러한 로컬 판정들이 무엇을 진단할 수 있는지 추가로 보여줍니다.