MAGS가 220개 사례에서 명세 검증 코드를 생성했다

MAGS는 220개 사례 모두에서 안전 보장을 갖춘 프로그램을 생성했습니다. 대상은 CUDA 커널 100개와 터미널 스크립트 100개였습니다. 로봇 팔 작업 20개도 포함됐습니다. 저는 100%라는 숫자보다 사람이 안전 요구사항을 검토해 먼저 고정했다는 점에 멈췄습니다. 기계가 증명하는 것은 그 기준을 지키는 일이기 때문입니다.

ILGPU가 CUDA·ROCm·OpenCL·Metal을 지원한다는 소식이 있습니다. MAGS의 CUDA 커널 안전 검증과 함께 보면 GPU 코드의 서로 다른 문제를 비춥니다. 하나는 여러 백엔드 지원이고, 다른 하나는 정해 둔 안전 요구사항을 만족하는지입니다.

기존 테스트나 정적 분석, 언어 모델의 판정만으로는 모든 예외를 다루기 어렵습니다. MAGS는 요구사항을 기계가 확인할 수 있는 형태로 만들고, Dafny로 검증한 뒤 위반을 찾아 코드를 고칩니다. 실행해 보고 문제가 없기를 기대하는 데 그치지 않고, 정해 둔 안전 조건을 코드가 지키는지 확인한다는 점이 반갑습니다.

다만 보장은 사람이 검토해 고정한 요구사항에 한정됩니다. 100%는 평가한 220개 사례에서 그 명세에 맞는 보장을 갖춘 프로그램을 생성한 비율이지, 모든 상황에서 안전하다는 뜻은 아닙니다. 자동으로 형식화한 요구사항이 실제 대상의 동작을 충분히 담지 못하면 실패가 나타났습니다. 요구사항의 정확성이 검증 결과의 의미를 바꿉니다.

도입을 검토하신다면 중요한 기능 하나의 안전 요구사항을 문장으로 적고, 그 요구가 실제 동작을 정확히 가리키는지 구현 담당자와 맞춰 보십시오. 시험 환경에서 요구를 어기는 오류 사례를 만들어 검증기가 잡는지 확인하고, 실행 결과도 같은 기준으로 대조하십시오. 둘이 어긋나면 명세부터 다시 다듬으십시오.

안전 요구사항을 실제 동작과 맞춰 보는 일과 코드가 그 요구를 지키는지 증명하는 일 가운데 무엇부터 확인하시겠습니까?