기술 요약: 소프트웨어 수준에서의 부동 소수점 신경망 검증
문제 정의
신경망 검증은 이상적인 실수 모델에 대한 형식적 보증을 제공하는 데 있어 상당한 발전을 이루었으나, 이러한 접근 방식은 종종 배포된 시스템의 구체적인 구현 세부 사항을 고려하지 못한다. 사이버 물리 시스템(CPS), 사물인터넷(IoT)과 같은 안전 필수 애플리케이션에서 신경망은 유한 정밀도 부동 소수점 산술(일반적으로 32비트 IEEE 754)을 사용하여 구현되며 표준 수학 라이브러리(예: math.h)에 의존한다. 이러한 저수준의 세부 사항은 무한 정밀도 모델로부터 도출된 안전성 증명을 무효화할 수 있는 반올림 오차와 비결합적 동작을 도입한다. 예를 들어, 본 논문은 SoftSign 활성화 함수가 실수 산술에서는 단조 증가하지만, 32비트 부동 소수점으로 구현될 때는 그렇지 않게 된다는 점을 보여준다.
소프트웨어 수준에서 신경망 코드를 검증하려는 기존의 시도들은 엇갈린 결과를 냈다. 소프트웨어 검증기들은 대규모 신경망 인스턴스로 확장하는 데 어려움을 겪는 경우가 많아, 실무자들이 무해한 무한 정밀도 모델로 회귀하거나 검증을 포기하고 테스트로 전환하게 만든다. 또한, 기존 도구들은 특정 설정에서 잘못된 결과를 생성하는 것이 관찰되었으며, 이는 부동 소수점 구현에 대한 안전 오라클로서의 신뢰성에 의구심을 던진다. 자동화된 소프트웨어 검증기를 특히 신경망 코드에 대해 엄격하고 표준화된 방식으로 평가하는 작업이 부족한 실정이다.
방법론
이러한 격차를 해결하기 위해 저자들은 8개의 최첨단 자동화된 소프트웨어 검증기를 신경망 코드에 대해 엄격하게 평가하였다. 방법론은 세 가지 주요 구성 요소로 이루어졌다:
벤치마크 구축 (NeuroCodeBench 2.0): 저자들은 912개의 검증 예제를 포함하는 포괄적인 벤치마크를 구축하였다. 이 벤치마크는 다음을 포함한다:
- 수학 함수: 표준
math.h 함수의 속성(예: 단조성, 주기성, 선형 경계)을 테스트하는 58개의 인스턴스.
- 활성화 함수: 일반적인 활성화 함수(예: ReLU, TanH, SoftSign, GELU)의 속성을 테스트하는 57개의 인스턴스.
- 신경망 레이어: 아핀 변환, 정규화, 풀링 및 SoftMax 레이어를 다루는 86개의 인스턴스.
- 전체 신경망: Hopfield 네트워크, SAT 인코딩된 ReLU 네트워크, 다항 근사 네트워크, Lipschitz 유계 네트워크, 그리고 VNN-COMP(확률 밀도 및 강화 학습 작업)에서 파생된 네트워크를 포함하는 711개의 인스스턴스.
- 그라운드 트루스 (Ground Truth): 모든 인스턴스는 브루트 포스 테스팅, 전수 조사 또는 반례 생성과 같은 기법을 사용하여 "안전(safe)" 또는 "불안전(unsafe)"으로 사전 라벨링되어, 평가를 위한 알려진 정답 판정을 보장한다.
표준화 및 호환성: 공정한 비교와 재현성을 보장하기 위해, 저자들은 모든 벤치마크 인스턴스를 국제 소프트웨어 검증 경연 대회(SV-COMP)에서 사용하는 형식으로 변환하였다. 여기에는 모델 구현, 안전 속성 및 필요한 의존성을 포함하는 자립형 C 파일을 생성하는 과정이 포함된다. 워크플로우는 리소스 제한 및 실행을 관리하기 위해 BenchExec 프레임워크를 활용하였으며, 이를 통해 도구들이 2024년 SV-COMP 에디션에서 사용된 것과 동일한 구성으로 실행되도록 보장하였다.
실험적 평가: 본 연구는 두 가지 조건 하에서 8개의 도구(2LS, CBMC, CPAChecker, DIVINE, ESBMC, PeSCo, Pinaka, UAutomizer)를 평가하였다:
- 베이스라인 (Baseline): 일반 벤치마크 인스턴스에 검증기를 실행.
- 운영 모델 (Operational Models):
math.h 라이브러리의 명시적인 C 구현(MUSL 및 CORE-MATH 사용)을 제공하여, 함수 정의를 공급하는 것이 검증 결과 개선에 도움이 되는지 확인.
- 역사적 분석: 저자들은 또한 분야의 트렌드를 관찰하기 위해 한 가지 도구(ESBMC)의 2018년부터 2026년까지의 역사적 성능을 분석하였다.
주요 기여
- NeuroCodeBench 2.0: 부동 소수점 신경망의 소프트웨어 수준 검증을 위해 특별히 설계된 대규모 그라운드 트루스 벤치마크를 구축하였다. 이는 단순 함수부터 최대 170K 개의 파라미터를 가진 전체 네트워크에 이르기까지 912개의 인스턴스를 포함한다.
- SV-COMP 통합: 벤치마크를 SV-COMP 인프라와 호환되는 형식으로 구성하여, 이를 2026년 공식 벤치마크 세트의 일부로 만들었다. 이를 통해 표준 도구 구성을 사용하여 자동화되고 재현 가능한 평가가 가능하다.
- 엄격한 평가: 신경망 코드에 대해 8개의 최첨단 소프트웨어 검증기를 비교하는 최초의 체계적인 연구로서, 성능과 정확성의 상당한 편차를 드러냈다.
- 운영 모델 분석: 수학 라이브러리(MUSL, CORE-MATH)의 명시적 구현을 제공하는 것이 검증기 성능을 향상시키는지 조사하였으며, 그 영향이 도구에 따라 다르며 종종 미미하거나 부정적임을 발견하였다.
결과
평가는 신경망을 위한 소프트웨어 검증의 현재 상태에 관한 몇 가지 중요한 발견을 도출하였다:
- 낮은 정확도 및 확장성: 결과는 "다소 실망스러운" 것으로 묘কে되었다. 도구들은 벤치마크 전반에 걸쳐 큰 편차를 보였는데, 가장 성능이 좋은 도구인 CBMC가 912개 중 371개의 인스턴스를 올바르게 해결한 반면, 다른 도구들은 훨씬 적게 해결하였다. 카테고리별 평균 해결률은 다양했으며, 복잡한 카테고리(예: 강화 학습)의 경우 해결률이 3%까지 떨어지기도 했다. 대부분의 도구는 한 번에 단일 신경층 이상을 검증하는 데 실패했다.
- 잘못된 판정: 여러 도구가 높은 비율의 잘못된 결과를 생성했다. 예를 들어, CBMC는 약 25%의 잘못된 확정적 판정(대부분 거짓 양성)을 생성하였으며, Pinaka와 UAutomizer 역시 상당한 오류율을 보였다. 오직 ESBMC만이 상당한 수의 인스스턴스를 해결한 도구들 중에서 잘못된 판정을 생성하지 않았다.
- 운영 모델의 영향:
math.h의 명시적 구현(MUSL 또는 CORE-MATH)을 제공하는 것이 전반적으로 눈에 띄는 개선을 가져오지는 않았다. CB some 도구들(CBMC, ESESBMC, Pinaka)의 경우, 라이브러리 코드를 검증하는 데 드는 복잡성 때문에 성능이 오히려 저하되었다. 다른 도구들(CPAChecker, PeSCo)의 경우, 해결된 인스턴스의 수는 증가했으나, 이는 종종 잘못된 판정의 급증을 동반했다.
- 확장성 한계: 도구들은 전체 신경망 처리에 심각한 어려움을 겪었다. 강화 학습 및 확률 밀도와 같은 복잡한 카테고리에서는 해결률이 한 자릿수로 떨어졌다. 합성 네트워크의 경우에도 ESBMC와 같은 도구는 타임아웃이 발생하기 전까지 매우 작은 너비(예: 너비 4)의 인스턴스만 해결할 수 있었다.
- 역사적 발전: 2018년부터 2026년까지의 ESBMC 분석은 비단조적이지만 일반적으로 일정한 개선을 보여주었다. 2022-2023년의 주목할 만한 잘못된 판정 급증은 k-유도 알고리즘의 구현 오류로 추적되었으며, 이는 NeuroCodeBench 1.0 출시 이후 수정되었다. 2024년 NeuroCodeBench 1.0의 도입은 커뮤니티 전반에서 잘못된 판정의 급격한 감소를 이끌어냈으나, NeuroCodeBench 2.0(2025년 후반)의 영향은 더 완만했다.
의의 및 주장
본 논문은 신경망을 소프트웨어 수준에서 검증하는 것이 개념적으로는 가능하지만, 기존의 최첨단 소프트웨어 검증기들은 아직 이 작업을 효과적으로 처리할 준비가 되어 있지 않다고 주장한다. 연구는 현재의 도구들이 단일 레이어 이상을 신뢰성 있게 체크할 수 없고, 자주 잘못된 결과를 반환하며, 표준 수학 라이브러리에 대한 완전한 지원이 부족함을 강조한다.
저자들은 자신들의 연구가 검증 커뮤니티를 위한 필수적인 "현실 점검(reality check)" 역할을 한다고 주장한다. 알려진 그라운드 트루스를 갖춘 엄격한 벤치마크를 제공함으로써, 그들은 이상적인 검증과 소프트웨어 구현 사이의 간극이 현재 기존 도구들이 큰 개선 없이 메우기에는 너무 넓다는 것을 입증하였다. 저자들은 NeuroCodeBench의 초기 출시 이후 잘못된 판정이 감소한 것을 통해 NeuroCodeBench가 이미 발전을 자극했다고 상정한다. 그러나 저자들은 최악의 수치적 편차에 맞서 신경망의 전체 구현을 인증하는 것은 부동 소수점 산술에 적응된 커스텀 결정 절차와 수학 라이브러리에 대한 네이티브 지원을 필요로 하는 장기적인 과제로 남아 있다고 결론짓는다.