RESOLVE: 테스트, 축소, 증명을 통한 언어 독립적인 GPU 커널 검증

AI 시스템은 이제 프로덕션(production) GPU 커널을 작성하고 최적화할 수 있지만, 이를 검증하는 것은 여전히 중요한 과제로 남아 있습니다. 몇 가지 임의 입력에 대해 커널을 평가하고 그 출력이 신뢰할 수 있는 참조 커널과 숫자 공차 범위 내에서 일치하는지 확인하는 것만으로는 충분하지 않습니다. 레이스(races)는 테스트에서 나타나지 않는 비결정적 동작을 유발할 수 있으며, 숫자 공차 범위는 광범위한 보정 후에도 버그를 숨기거나 거짓 양성(false positives)을 유발할 수 있습니다. 이 문제를 해결하기 위해, 우리는 테스트와 형식 검증(formal verification)을 결합하여 포괄적인 커널 검증 파이프라인을 구축하는 RESOLVE를 제시합니다. 이는 세 단계로 작동합니다. 첫째, 실행 타이밍을 교란하는 바이너리 계측(binary instrumentation)을 사용하여 비결정성을 테스트하고 레이스를 노출합니다. 둘째, 에이전트가 후보 커널과 참조 커널을 재작성하여 분석하기 더 간단하지만 모든 테스트에서 비트 단위로 동일한 출력을 생성하는 '축소된 동시성(reduced-concurrency)' 버전을 얻습니다. 셋째, 축소된 커널은 F*/Pulse 프레임워크에서 형식적으로 분석되어 실수에 대해 동일한 계산을 수행함을 증명합니다. 이는 숫자 공차 범위의 필요성을 우회합니다. 우리는 RESOLVE가 KernelBench를 사용하여 광범위한 선택의 커널을 검증할 수 있으며, 세 가지 최신 프레임워크 및 언어(CUTLASS, Triton, Gluon)에서 융합된 GEMM에 걸쳐 동등성(equivalence)을 증명할 수 있음을 보여줍니다. 또한, 검증하기가 악명이 높은 메가 커널(mega-kernels)도 분석하고, 두 개의 명확한 버그를 포함하여 이전에 보고되지 않은 네 가지 문제를 발견했습니다. 우리는 에이전트가 RESOLVE를 사용하여 이러한 문제들을 최소한의 성능 영향으로 수리할 수 있음을 보여주며, 에이전트가 결과를 엄격하게 확인할 수 있을 때 공격적으로 최적화할 수 있음을 강조합니다.