기술 요약: VNN-LIB 2.0: 신경망 검증의 엄밀한 기초

문제 제기

신경망 검증 커뮤니티는 솔버와 상위 수준 도구 간의 상호 운용성을 촉진하기 위해 VNN-LIB 표준 (버전 1.0) 에 점점 더 의존해 왔습니다. 그러나 버전 1.0 은 엄밀한 형식적 기초로 기능하는 것을 방해하는 네 가지 치명적인 결함을 안고 있습니다:

1. 형식적 구문 부재: 버전 1.0 은 쿼리 언어 구문을 형식적으로 정의하지 않아, 서로 다른 솔버들이 상호 호환되지 않는 구현을 하도록 유도합니다.
2. 제한된 표현력: 해당 표준은 단일 입력과 단일 출력을 가진 단일 네트워크를 가정합니다. 이는 여러 네트워크, 여러 입력/출력, 또는 은닉 레이어 접근을 본질적으로 지원하지 못하므로, 사용자들이 모델을 인위적으로 병합하게 만들어 검증된 산물과 배포된 모델 간의 관계를 모호하게 만듭니다.
3. 타입 시스템 부재: 숫자 유형 (예: 부동 소수점 대 실수) 을 지정할 메커니즘이 없어, 솔버들이 유한 정밀도 산술을 실수 값으로 취급할 때 모호성과 잠재적인 비정합성 (unsoundness) 이 발생합니다.
4. 의미론 부재: 해당 표준은 형식적 의미론을 갖추지 못해, 솔버, 쿼리 생성기, 또는 변환의 정확성을 형식적으로 증명하는 것이 불가능하며, 증명 서명 (proof certificates) 개발을 저해합니다.

SMT-LIB 와 같은 표준과 구별되는 VNN-LIB 의 고유한 과제는 쿼리가 자체적으로 완결되지 않고 (외부 신경망 모델, 일반적으로 ONNX 형식) 의 속성을 지정한다는 점입니다. ONNX 자체는 형식적 의미론이 부재하며 계속 진화하고 있으므로, 엄밀한 VNN-LIB 표준을 정의하려면 특정 ONNX 버전으로부터 쿼리 언어를 분리하면서도 호환성을 유지해야 합니다.

방법론

저자들은 이러한 과제들을 해결하기 위해 VNN-LIB 2.0 의 이론적 기초를 개발합니다. 핵심 방법론적 혁신은 **네트워크 이론 ($\Psi$)**의 도입입니다.

1. 네트워크 이론 추상화

저자들은 VNN-LIB 를 정의하기 위해 신경망 모델 형식에서 요구되는 최소한의 구문, 타입 판정, 그리고 의미론을 포착하는 추상적 명세로서 "네트워크 이론"을 정의합니다.

• 분리 (Decoupling): $\Psi$는 인터페이스 역할을 합니다. $\Psi$의 구체적인 구현 (예: ONNX v1.20.0 용) 은 요소 유형, 텐서 표현, 모델 구조, 그리고 노드 출력 참조에 대한 구체적인 정의를 제공합니다.
• 모듈성: VNN-LIB 2.0 은 추상적인 $\Psi$에 상대적으로 정의됩니다. 이는 ONNX 가 진화하더라도 표준이 안정적으로 유지되도록 합니다. 새로운 ONNX 버전에서는 VNN-LIB 표준 자체가 아닌 $\Psi$의 인스턴스화만 업데이트하면 됩니다.
• 형식화: 구문, 타입, 의미론을 포함한 전체 표준은 내부 일관성을 보장하고 모호성을 배제하기 위해 Agda 상호작용 증명기에서 기계화되었습니다.

2. 형식적 구문과 표현력

네트워크 이론을 바탕으로 저자들은 표현력을 크게 확장하는 VNN-LIB 2.0 의 형식적 문법을 정의합니다:

• 여러 네트워크: 쿼리는 여러 네트워크를 선언할 수 있어, 교사 - 학생 검증이나 인코더 - 디코더 아키텍처와 같은 시나리오를 지원합니다.
• 네트워크 동등성: 해당 표준은 equal-to(정확히 동일한 모델 파일 참조) 와 isomorphic-to(동일한 그래프 구조를 가지지만 가중치는 다를 수 있는 모델 참조) 선언을 도입합니다. 이를 통해 솔버는 네트워크 복사본 간에 추론 (예: 변수 경계) 을 공유할 수 있습니다.
• 은닉 노드: declare-hidden 구성은 중간 레이어 출력에 대한 제약을 허용하여, 인코딩이나 어텐션 메커니즘에 대한 추론에 필수적입니다.
• 다차원 I/O: 다중 모달 네트워크를 수용하기 위해 임의의 개수의 입력과 출력을 지원합니다.

3. 타입 시스템과 의미론

• 타이핑: 형식적 타입 시스템은 숫자적 정합성 (numeric soundness) 을 강제합니다. 이는 산술 연산과 비교가 호환되는 유형 (예: 명시적 강제 변환 규칙 없이 float32와 int32를 혼합하는 것을 방지) 으로 수행되도록 보장합니다. 타입 시스템은 하부 네트워크 이론 $\Psi$가 제공하는 판정에 의존합니다.
• 의미론: 쿼리의 의미론은 수학적 만족 가능성 문제로 정의됩니다. 모델 집합 $M$($\Psi$에서 인스턴스화됨) 과 입력 할당 $X$가 주어졌을 때, 의미론은 모든 단언이 참으로 평가되는 할당이 존재하는지 결정합니다.
• 실수 값 쿼리: 모델을 실수 ($\mathbb{R}$) 상의 함수로 취급하는 기존 솔버를 수용하기 위해, 해당 표준은 "실수 값 쿼리" 메커니즘을 도입합니다. 구별되는 real 유형을 사용하여 쿼리 작성자는 솔버가 부동 소수점 부정확성으로 인한 잠재적 비정합성을 인정하고 모델을 $\mathbb{R}$ 상에서 해석하도록 명시적으로 승인합니다. 이는 기본 이론에서 파생된 특정 네트워크 이론 $\Psi_{\mathbb{R}}$을 구성함으로써 달성됩니다.

주요 기여

1. 네트워크 이론 ($\Psi$): 모델 형식에서 요구되는 최소 의미론 인터페이스를 정의하는 새로운 추상화를 도입하여, VNN-LIB 가 특정 ONNX 버전과 독립적으로 정의되도록 합니다.
2. 형식적 구문과 문법: 여러 네트워크, 은닉 레이어, 그리고 복잡한 입력/출력 구조를 지원하는 VNN-LIB 2.0 을 위한 정밀한 문맥 자유 문법.
3. 형식적 타입 시스템: 네트워크 이론에 상대적인 숫자 유형 정합성을 강제하는 타이핑 시스템으로, 숫자 표현의 모호성을 해결합니다.
4. 형식적 의미론: 네트워크 이론에 의해 매개변수화된 쿼리 의미론의 엄밀한 수학적 정의로, VNN-LIB 를 소비하거나 생성하는 도구의 정확성에 대한 형식적 증명을 가능하게 합니다.
5. 기계화: 전체 표준이 Agda 에서 형식화되어, 표준 참조 구현과 기계 검증 증명의 기초를 제공합니다.
6. 실수 값 확장: 정합성 필요성과 현재 솔버 능력의 현실 사이의 균형을 맞추기 위해 파생된 네트워크 이론을 통한 실수 값 분석 지원에 대한 모듈식 접근.

결과 및 검증

• 내부 일관성: Agda 형식화는 구문, 타이핑, 의미론의 내부 일관성을 검증하여, 버전 1.0 에 존재하던 모호성이 없는 표준임을 보장합니다.
• 표현력 시연: 논문은 네트워크 이론 $\Psi$의 간단한 변환이 실수 값 쿼리를 위한 완전한 인스턴스를 산출하는 방법을 보여주어, 추상화의 유연성을 입증합니다.
• 커뮤니티 채택: 해당 표준은 검증 커뮤니티로부터 긍정적인 피드백을 받았습니다. 주요 솔버 팀들이 VNN-LIB 2.0 지원을 약속했으며, 새로운 표준은 VNN-COMP 2026 대회에서 사용될 예정입니다.
• 도구 지원: 저자들은 Agda 형식화와 함께 새로운 표준을 준수하는 파서와 타입 체커를 구현한 고성능 C++ 라이브러리 (Python 및 Julia 바인딩 포함) 를 공개했습니다.

중요성

이 논문은 VNN-LIB 2.0 이 신뢰할 수 있는 신경망 검증을 위한 강건하고 엄밀한 기초를 제공한다고 주장합니다. 그 중요성은 두 가지 보완적 영역에 있습니다:

1. 실용적 상호 운용성: 표현력 (여러 네트워크, 은닉 노드) 을 확장하고 구문을 표준화함으로써, 커뮤니티가 richer 속성을 통일된 방식으로 지정하고 검증할 수 있게 하여, 더 나은 벤치마킹과 도구 비교를 촉진합니다.
2. 이론적 엄밀성: 형식적 의미론과 타입 시스템을 제공함으로써 도구와 솔버 간의 "엄밀한 계약"을 수립합니다. 이는 도구 자체 (솔버, 최적화기, 증명 체커) 의 형식적 검증을 가능하게 하며, 숫자적 정합성 (예: 실수 값과 부동 소수점 의미론 구분) 과 관련된 미묘한 문제를 해결합니다.

저자들은 이 작업이 이론적이지만 구체적인 결과를 가져온다고 강조합니다: 즉, 쿼리의 모호하지 않은 해석을 보장하고, 기술적 문제를 해결할 언어를 제공하며, 미래의 형식적으로 검증된 증명 서명을 위한 기초를 마련합니다.