🤖 machine learning

The Complexity of Verifying Feedforward Neural Networks in Quantised Settings

본 논문은 선형 및 비트 벡터 명세 하에서 고정 산술 정밀도를 갖는 네트워크에 대해 검증이 여전히 NP-완전임을 보여주면서 동적 양자화 네트워크에 대한 비트 벡터 명세 하에서 새로운 상한을 제시함으로써 양자화된 환경에서 순방향 신경망 검증을 위한 계산 복잡도 지형을 확립한다.

원저자: Eric Alsmann, Martin Lange, Marco Sälzer

게시일 2026-05-29

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Eric Alsmann, Martin Lange, Marco Sälzer

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

매우 똑똑한 로봇 (순방향 신경망) 이 사진에서 고양이를 인식하거나 자율주행차를 조종하는 것처럼 결정을 내린다고 상상해 보세요. 이 로봇을 실제 세계에 풀어놓기 전에, 위험한 실수를 하지 않을 것이라는 것을 100% 확신해야 합니다. 이 과정을 **검증 (verification)**이라고 합니다.

오랫동안 과학자들은 이 로봇들을 완벽한 무한 정밀도의 수학으로 만들어졌다고 가정하며 검증해 왔습니다 (원자 크기까지 영원히 측정할 수 있는 자를 사용하는 것과 같습니다). 하지만 실제 세계에서는 컴퓨터가 완벽하지 않습니다. 컴퓨터는 **양자화된 산술 (quantized arithmetic)**을 사용하는데, 이는 밀리미터마다 표시만 있는 자를 사용하는 것과 같습니다. 무언가를 반올림해야 하며, 때로는 공간이 부족해집니다 (오버플로우).

이 논문은 다음과 같은 큰 질문을 던집니다: "완벽한 수학"에서 "실제 세계의 반올림된 수학"으로 전환하면 로봇이 안전한지 증명하는 것이 훨씬 더 어려워질까요?

다음은 일상적인 비유를 사용한 그들의 발견 사항에 대한 요약입니다:

1. 세 가지 유형의 로봇

저자들은 이러한 로봇이 구축되는 세 가지 다른 방식을 살펴보았습니다:

이상적인 로봇 (Rational FNN): 완벽한 무한 정밀도의 수학으로 구축됨.
양자화 전 로봇 (Quantised FNN): 처음부터 "밀리미터 자" (유한 폭 수학) 를 사용하여 구축됨.
변환된 로봇 (Dynamically Quantised): 이미 훈련된 후 "밀리미터 자"를 사용하도록 강제된 완벽한 로봇.

2. 두 가지 유형의 안전 규칙

로봇이 안전한지 확인하기 위해 규칙을 부여합니다. 논문은 두 가지 유형의 규칙집을 살펴봅니다:

선형 규칙 (LP): 단순하고 직선적인 규칙입니다. "속도가 50 미만이면 안전합니다"라고 적힌 교통 표지판과 같습니다. 이러한 규칙은 매끄럽고 볼록한 형태로 시각화하기 쉽습니다.
비트 벡터 규칙 (BV): 복잡하고 "비트 단위"의 규칙입니다. 컴퓨터 두뇌 내부의 특정 스위치를 확인하는 보안 시스템과 같습니다. "비트 3 이 켜져 있고 비트 7 이 꺼져 있지만 비트 2 가 켜져 있으면 문제가 됩니다." 이러한 규칙은 매우 거칠고 복잡하며 비선형적인 형태를 설명할 수 있습니다.

3. 주요 발견 사항: 더 어려운가요?

시나리오 A: 단순한 규칙 (선형 제약 조건)

결과: 아니요, 더 어렵지 않습니다.
로봇이 완벽한지 아니면 "밀리미터 자"를 사용하는지, 그리고 규칙이 단순한지 복잡한지에 상관없이 안전성을 확인하는 것은 여전히 NP-complete입니다.

비유: 거대하고 지저분한 서랍에서 특정 열쇠를 찾으려 한다고 상상해 보세요. 열쇠가 금 (완벽한 수학) 으로 만들어졌든 플라스틱 (반올림된 수학) 으로 만들어졌든, 서랍이 정리되어 있든 혼란스러워 있든, 열쇠를 찾는 난이도는 변하지 않습니다. 여전히 "어려운" 문제이지만, 이전과 동일한 수준의 어려움입니다.
이것이 중요한 이유: 이는 실제 세계의 로봇을 검증하기 위해 완전히 새로운 초강력 컴퓨터를 발명할 필요가 없다는 것을 의미합니다. 완벽한 수학에 이미 사용 중인 도구들을 실제 세계 수학에 맞게 조정하면 기하급수적으로 느려지지 않습니다.

시나리오 B: 복잡한 규칙 (비트 벡터 제약 조건)

결과: 로봇의 "두뇌" 크기에 따라 다릅니다.

로봇이 처음부터 "밀리미터 자"로 구축된 경우: 안전성 확인은 여전히 NP-complete입니다 (이전과 동일한 난이도).
완벽한 로봇을 가져와서 "밀리미터 자"를 사용하도록 강제하는 경우 (동적 양자화): 이것이 훨씬 더 어려워집니다. PSPACE-complete로 급상승합니다.
- 비유: 완벽한 레시피 (완벽한 로봇) 가 있다고 가정해 보세요. 이제 제한된 냄비와 프라이팬 세트가 있는 작은 주방 (유한 폭 산술) 에서 이를 요리해야 합니다. 처음부터 제한된 냄비를 사용하면 괜찮습니다. 하지만 완벽한 레시피를 요리하는 동안 제한된 주방으로 번역하려고 하면, 일이 잘못될 수 있는 가능한 경우의 수가 폭발적으로 늘어납니다. (크기가 다른 숫자들을 정렬하는 것과 같은) 모든 것을 확인하는 데 필요한 메모리는 "만일" 시나리오를 너무 많이 추적해야 하므로 엄청나게 커집니다.

4. 부동 소수점의 수수께끼

논문은 또한 **부동 소수점 숫자 (컴퓨터가 3.14 와 같은 소수를 처리하는 표준 방식)**를 살펴보았습니다.

고정 지수: 숫자의 범위가 고정되어 있는 경우 (최대 길이가 고정된 자와 같음), 난이도는 관리 가능한 수준 (PSPACE) 으로 유지됩니다.
일반 부동 소수점: 범위가 극적으로 변할 수 있는 경우, 난이도는 더 높아질 수 있습니다 (NEXPTIME).
비유: 부동 소수점 수학에서 숫자는 매우 작거나 매우 클 수 있습니다. 이를 더하려면 컴퓨터가 먼저 이를 "정렬"해야 합니다 (소수점을 맞추는 것과 같습니다). 숫자의 크기가 극도로 다르면 컴퓨터는 이 정렬을 수행하기 위해 엄청난 양의 데이터를 버퍼해야 합니다. 저자들은 이 "정렬" 단계가 문제를 훨씬 더 어렵게 만드는 원인임을 발견했습니다.

요약

이 논문은 본질적으로 다음과 같이 말합니다:

좋은 소식: 가장 일반적인 안전 확인 (선형 규칙) 의 경우, 실제 세계의 반올림된 수학으로 전환해도 작업이 불가능해지지 않습니다. 여전히 이론적 완벽한 수학과 동일한 수준의 난이도입니다.
나쁜 소식: 완벽한 로봇에 매우 복잡하고 비트 단위의 규칙을 적용하면서 반올림된 수학을 강제하는 경우, 작업이 훨씬 더 어려워집니다 (PSPACE).
미지의 영역: 범위가 극단적인 표준 부동 소수점 수학을 사용하는 경우, 작업이 더 어려울 수 있지만 저자들은 아직 100% 확신하지는 못합니다. 그들은 적어도 "PSPACE" 수준만큼 어렵다는 것만 알고 있습니다.

간단히 말해: 양자화 (반올림) 는 단순한 규칙에 대한 검증을 무너뜨리지 않지만, 복잡하고 동적인 시나리오에서는 계산 비용을 훨씬 더 크게 만듭니다.

기술적 요약: 양자화된 환경에서 순방향 신경망 검증의 복잡성

문제 제기

본 논문은 양자화된 환경에서 순방향 신경망 (FNN) 을 형식적으로 검증하는 계산 복잡성을 조사한다. 실수 연산 (유리수 가중치) 으로 작동하는 FNN 에 대한 도달 가능성 문제가 NP-완전임이 확립되어 있지만, 실제 구현은 유한 폭 연산 (예: 64 비트 부동소수점 또는 고정소수점 숫자) 에 의존한다. 이러한 전환은 반올림, 오버플로우, 언더플로우와 같은 양자화 효과를 도입한다.

저자들은 이해의 잠재적 격차를 다루고 있다: 이상화된 실수 연산에서 이산적이고 유한 폭인 연산으로의 이동이 검증의 계산 복잡성을 증가시키는가? 또한, 그들은 복잡성이 다음에 따라 어떻게 변화하는지 검토한다:

명세 형식: 선형 프로그래밍 (LP) 제약 조건 versus 비트-벡터 (BV) 논리 (비선형, 비트 단위 추론을 허용).
네트워크 정의: FNN 이 정확한 유리수 가중치 (유리수 FNN) 로 정의되는지 아니면 사전 양자화된 가중치 (양자화 FNN) 로 정의되는지.
매개변수 인코딩: 연산의 비트 폭이 입력의 일부로 1 진법 (하드웨어 레지스터 크기에 현실적) 이나 2 진법 (10 진법 명세에 현실적) 으로 주어지는지.

방법론

저자들은 연산 유형과 명세 언어에 따라 변하는 5 가지 서로 다른 도달 가능성 결정 문제를 REACH로 형식화한다:

REACHQ(LP): LP 명세를 가진 유리수 FNN (표준 설정).
REACHF(LP): LP 명세를 가진 양자화 FNN (가중치가 이미 유한 폭 연산에 있음).
REACHF(BV): 비트-벡터 명세를 가진 양자화 FNN.
REACH(F, LP): LP 명세를 가진 유리수 FNN (목표 유한 폭 연산 $F$ 가 입력의 일부인 동적 양자화).
REACH(F, BV): 동적 양자화와 비트-벡터 명세를 가진 유리수 FNN.

분석적 접근:

복잡성 하한: 저자들은 NP-난해성과 PSPACE-난해성을 확립하기 위해 알려진 어려운 문제들 (예: 3SAT) 로부터의 환원을 활용한다. 그들은 ReLU 활성화 함수를 사용하여 FNN 에 부울 논리를 인코딩하는 데 사용되는 표준 "가제트 (gadgets)"가 작은 정수와 $1/2$ 와 같은 분수를 표현할 수 있는 연산이 제공되는 한 유한 폭 연산 하에서도 유효함을 보여준다.
복잡성 상한:
- LP 명세의 경우, 저자들은 선형 프로그래밍에서 해의 크기에 대한 다항식 경계 (정리 1) 에 의존하여 증거 (입력 벡터) 를 추측하고 다항식 시간에 검증할 수 있음을 보인다.
- 동적 양자화를 가진 BV 명세의 경우, 저자들은 **축약된 비결정적 유한 오토마타 (NFA)**를 활용한다. 그들은 양자화 FNN 의 입력 - 출력 관계와 명세 공식을 나타내는 오토마타를 구성한다. 이러한 오토마타의 상태 공간은 기하급수적으로 크지만 축약된 방식으로 간결하게 기술된다.
- 그들은 고정소수점과 부동소수점 연산을 구분한다. 부동소수점의 경우, 일반적인 연산은 지수 차이에 의존하는 정렬 시프트를 필요로 한다. 지수 폭이 무제한 (2 진법으로 주어짐) 인 경우, 정렬 버퍼 크기가 기하급수적으로 되어 PSPACE 상한을 깨뜨릴 수 있다. 따라서 그들은 지수 폭이 일정한 경우로 PSPACE 상한 증명 범위를 제한한다.

주요 기여 및 결과

본 논문은 텍스트의 표 1 에 요약된 포괄적인 복잡성 지형을 확립한다:

1. 선형 프로그래밍 (LP) 명세

REACHQ(LP): Sälzer 와 Lange(2021) 를 인용하여 NP-완전임이 재확인됨.
REACHF(LP): NP-완전임이 증명됨. 저자들은 사전 양자화된 가중치를 사용하더라도 증거의 입력 크기가 네트워크 크기에 대해 다항식적이므로 문제가 NP 에 머무른다고 보여준다.
REACH(F, LP): NP-완전임이 증명됨. 비트 폭 매개변수가 입력의 일부 (동적 양자화) 일지라도 문제는 NP-완전으로 남는다. 저자들은 비트 폭이 1 진법이든 2 진법이든 상관없이 증거의 크기가 입력 크기에 대해 다항식적으로 제한된다고 주장한다.

2. 비트-벡터 (BV) 명세

REACHF(BV): NP-완전임이 증명됨. 이미 양자화된 네트워크의 경우 비트-벡터 논리의 사용이 NP 를 넘어 복잡성을 증가시키지 않는다.
REACH(F, BV) (고정소수점 및 일정한 지수 폭을 가진 부동소수점): PSPACE-완전임이 증명됨.
- 하한: Henzinger 등 (2021) 이 이전에 확립한 PSPACE-난해성 결과와 일치함.
- 상한: 저자들은 축약된 NFA 의 비공집합성 문제로 문제를 환원함으로써 첫 번째 일치하는 PSPACE 상한을 제공한다.
REACH(F, BV) (일반 부동소수점): 문제는 PSPACE-난해이며 NEXPTIME 내에 있음.
- 저자들은 지수 폭이 가변적이고 2 진법으로 주어지는 일반 부동소수점 연산의 경우, 덧셈/곱셈의 정렬 단계가 지수 차이에 의존하는 버퍼 크기를 필요로 한다고 지적한다. 이는 다항식 기술 크기를 가진 축약된 NFA 의 구축을 방해하여 정확한 상한을 열어두고 있다 (현재 NEXPTIME).

중요성 및 주장

본 논문은 Henzinger 등 (2021) 의 결과를 특히 다루며 양자화 FNN 검증의 복잡성에 관한 "광범위한 오해"를 해결한다고 주장한다.

복잡성 동인 명확화: 저자들은 이전 연구에서 관찰된 NP 에서 PSPACE 로의 도약이 양자화 자체에 의해 발생하지 않고, 동적 양자화(연산이 입력의 일부인 경우) 와 비트-벡터 명세의 사용의 조합에 의해 발생한다고 주장한다. 표준 선형 명세의 경우 양자화는 복잡성 클래스를 증가시키지 않으며 NP-완전으로 남는다.
도구의 실현 가능성: 결과는 기존 실수 솔버에 비해 점근적 오버헤드 없이 선형 명세를 사용하는 양자화 FNN 을 위한 건전한 검증 도구를 개발하는 것이 가능함을 시사한다. 둘 다 NP-완전이기 때문이다.
BV 에 대한 상한: 본 논문은 고정소수점 및 제한된 지수 부동소수점 연산에 대해 PSPACE-완전성을 확립함으로써 BV 명세를 가진 동적 양자화 검증의 알려진 PSPACE-난해성을 보완한다.
미해결 문제: 저자들은 무제한 지수를 가진 일반 부동소수점 연산의 경우 정렬 요구 사항이 문제를 PSPACE 를 넘어 (NEXPTIME 으로) 밀어낼 수 있으며, 일치하는 하한을 증명할 수 있는지 여부는 여전히 미해결 문제라고 겸손하게 지적한다.

결론적으로, 본 논문은 동적으로 양자화된 네트워크에 대한 비트-벡터 명세가 PSPACE 복잡성을 도입하지만, 양자화된 네트워크에 대한 선형 제약 조건의 표준 사례는 유리수 경우의 NP-완전성을 유지한다는 엄격한 분류를 제공한다.