🤖 machine learning

Lookahead Branching for Neural Network Verification

이 논문은 기존의 분기 한정 검증기(branch-and-bound verifiers)를 개선하기 위해 분기 결정(branching decisions)을 향상시키고 추가적인 렘마(lemmas)를 생성함으로써 일관된 속도 향상과 최대 57% 더 많은 인스턴스 해결을 이끌어내는 신경망 검증을 위한 일반적인 룩어헤드 분기 전략(lookahead branching strategy)을 소개한다.

원저자: Liam Davis, Duo Zhou, Huan Zhang, Guy Katz, Clark Barrett, Haoze Wu

게시일 2026-07-21

📖 5 분 읽기🧠 심층 분석

CC BY 4.0

원저자: Liam Davis, Duo Zhou, Huan Zhang, Guy Katz, Clark Barrett, Haoze Wu

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

우리의 자동차, 의료 기기, 보안 시스템의 '두뇌'가 뉴럴 네트워크라고 불리는 거대하고 복잡한 수학적 웹으로 만들어진 세상을 상상해 보십시오. 이 디지털 두뇌들은 얼굴을 인식하거나 날씨를 예측하는 데 매우 뛰어나지만, 동시에 이해하기가 매우 까다롭기로 유명합니다. 이들은 엄격하게 작성된 규칙을 따르는 것이 아니라 데이터 속에서 패턴을 찾아내며 학습하기 때문에, 상황이 이상하게 흘러갈 때 반드시 실수를 할지 아닐지를 확신하기 어렵습니다. 이는 안전 문제에서 큰 문제가 됩니다. 만약 자율주행차의 두뇌가 잘못된 추측을 한다면 사람들이 다칠 수 있기 있기 때문입니다. 그래서 한 과학자 그룹은 이러한 네트워크가 어떤 입력값이 들어오더라도 항상 올바르게 작동한다는 것을 수학적으로 증명하는 방법을 연구해 왔습니다. 이 과정은 마치 탐정이 모든 가능한 단서들을 하나하나 확인하며 거대한 미스터리를 풀려고 노력하는 것과 같습니다. 탐정은 미스터리를 점점 더 작은 조각들로 나누고, 각 조각이 모순(버그)으로 이어지는지 아니면 안전한 결과로 이어지는지 확인해야 합니다. 문제는 가능한 단서가 너무 많아서 하나씩 모두 확인하는 데 우주의 나이보다 더 긴 시간이 걸릴 수도 있다는 점입니다. 따라서 탐정은 전체 퍼즐을 빠르게 풀 수 있는 최선의 선택을 하기 위해 다음에 어떤 단서를 확인할지 결정하는 스마트한 전략이 필요합니다.

이 논문은 그 탐정에게 제공할 '룩어헤드 브랜칭(Lookahead Branching, 앞을 내다보는 분기)'이라는 영리한 새로운 전략을 소개합니다. 연구진은 두 가지 서로 다른 유형의 검증 도구(Marabou와 α-β-CROWN이라 불리는 것)를 사용하여, 단순히 현재 일어나는 일에 기반해 다음에 어떤 단서를 확인할지 추측하는 대신, 몇 단계 앞을 시뮬레이션해야 한다는 것을 발견했습니다. 체스를 두는 상황을 상상해 보십시오. 일반적인 플레이어는 현재 판을 보고 지금 당장 좋아 보이는 수를 고를 것입니다. 하지만 그랜드마스터는 "내가 여기로 움직이면, 상대방은 저기로 움직일 것이고, 그러면 나는 다시 저기로 움직일 수 있다..."라고 생각할 것입니다. 저자들은 뉴럴 네트워크 검증기도 이와 똑같이 해야 한다고 제안합니다. 즉, 결정을 내리기 전에 여러 경로를 따라갔을 때 어떤 일이 벌어질지 잠시 동안 "꿈을 꾸듯" 시뮬레이션해 보아야 한다는 것입니다. 연구진은 이처럼 미래의 단계들을 시뮬레이션하기 위해 약간의 시간을 더 투자함으로써, 검증기가 더 나은 선택을 할 수 있고, 결과적으로 더 빠른 해결책을 얻으며 이전보다 더 많은 문제를 해결할 수 있다는 것을 발견했습니다. 실험 결과, 이 접근 방식은 도구들이 최대 57% 더 많은 사례를 해결하도록 도왔으며, 특히 가장 어려운 문제들에서 성능을 크게 향상시켰습니다.

이 논문의 핵심은 어떻게 이 "꿈꾸기"를 효율적으로 수행하느냐에 있습니다. 연구진은 어떤 검증 도구에도 추가할 수 있는 일반적인 레시피를 만들었습니다. 그 과정은 다음과 같습니다. 도구가 문제를 분할(split)해야 할 때, 단순히 하나의 옵션만을 선택하는 것이 아닙니다. 대신, 몇 가지 유망한 후보들을 뽑아 각각의 후보로 분할했을 때를 시뮬레이션합니다. 그리고 '룩어헤드 깊이(lookahead depth)'만큼 앞을 내다보며 문제가 어떻게 변하는지 관찰합니다. 만약 어떤 분할이 많은 혼란스러운 부분들을 갑자기 명확하게 만든다면(예를 들어, '불안정'했던 뉴런이 갑자기 '고정'되는 경우), 그 분할은 높은 점수를 받게 됩니다. 그런 다음 도구는 가장 높은 점수를 받은 분할을 선택합니다.

저자들은 또한 이 시뮬레이션이 단순히 최선의 경로를 선택하기 위한 것뿐만 아니라, 새로운 사실을 찾아내는 역할도 한다는 것을 발견했습니다. 때때로 분할을 시뮬레이션하는 과정에서, 도구는 공식적으로 분할을 수행하기도 전에 특정 네트워크 부분이 반드시 특정한 상태에 있어야 한다는 것을 깨닫기도 합니다. 이를 통해 도구는 해당 부분들을 즉시 "고정"할 수 있으며, 이는 방대한 양의 불필요한 작업을 줄여줍니다. 논문은 이 방법이 표준 컴퓨터 프로세서에서 실행되는 도구(Marabou)와 강력한 그래픽 카드를 사용하는 도구(α-β-CROWN)라는 두 가지 매우 다른 유형의 검증 도구 모두에서 잘 작동함을 보여줍니다.

실험에서 팀은 손글씨 숫자를 인식하는 단순한 네트워크부터 컴퓨터 비전에 사용되는 복잡한 네트워크에 이르기까지 다양한 뉴럴 네트워크를 대상으로 이 방법을 테스트했습니다. Marabou 도구의 경우, 룩어헤드를 사용하는 것이 더 많은 문제를 해결하는 데 도움이 되었고 어려운 케이스에 소요되는 시간을 줄여주었습니다. 예를 들어, NN4Sys라고 불리는 특정 벤치마크 세트에서 룩어헤드를 사용한 도구가 사용하지 않았을 때보다 더 많은 사례를 해결했습니다. 매우 빠른 것으로 알려진 α-β-CROWN 도구에서도 룩어헤드 전략은 여전히 해결 시간을 단축시켰으며, 기존 방식이 놓쳤던 몇 가지 추가적인 문제들을 해결해 냈습니다. 연구진은 룩어헤드를 설정하는 데 아주 약간의 추가 시간이 걸리기는 하지만, 나중에 잘못된 경로에 시간을 낭비하는 것을 방지해주기 때문에 그 보상이 매우 크다고 언급했습니다.

그러나 이 논문은 이것이 모든 것을 즉시 해결하는 마법의 탄환은 아니라는 점을 주의 깊게 지적합니다. "룩어헤드" 과정은 계산 비용이 많이 드는 작업, 즉 앞을 내달려 생각하기 위해 더 많은 컴퓨터 전력을 사용해야 하는 작업입니다. 저자들은 이 방법이 결정이 미래에 가장 큰 영향을 미치는 검색의 맨 처음에 사용될 때 가장 효과적이라는 것을 발견했습니다. 만약 모든 단계마다 룩어헤드를 사용하려고 한다면, 앞을 내다보는 데 드는 비용이 이득보다 커질 수 있습니다. 또한 그들은 얼마나 많은 단계를 앞을 내다볼 것인지, 그리고 얼마나 많은 후보를 시뮬레이션할 것인지와 같은 다양한 설정을 테스트했으며, 적절한 깊이(두 단계 앞을 내다보는 것)가 가장 어려운 문제들에 효과적이라는 것을 발견했습니다.

이 논문은 우리가 왜 빠른 로컬 정보만을 사용하여 결정을 내려야 하는지에 대한 생각에 명시적으로 반박합니다. 빠른 휴리스틱(경험 법칙)은 속도 면에서는 좋지만, 종종 더 큰 그림을 놓치고 검증기를 막다른 길로 인도할 수 있습니다. 저자들은 분할의 결과를 시뮬레이션하기 위해 초기에 약간의 노력을 더 투자함으로써 전체적인 검증 과정이 훨씬 더 효율적이 된다는 것을 보여줍니다. 또한 그들은 자신들의 방법이 분기하는 법을 배우기 위해 인공지능을 사용하는 것과는 다르다는 점을 명확히 합니다. 과거의 데이터로 모델을 훈련시키는 대신, 그들의 방법은 실시간으로 최선의 수를 결정하기 위해 수학적 시뮬레이션을 사용합니다.

궁극적으로, 이 논문은 "룩어헤드 브랜칭"이 다양한 검증 도구에 삽입되어 도구들을 더 똑똑하고 빠르게 만들 수 있는 강력하고 일반적인 전략임을 시사합니다. 이것은 기존 도구를 대체하는 것이 아니라 강화하는 것이며, 이를 통해 더 어려운 안전 필수 문제들을 더 높은 확신을 가지고 다룰 수 있게 해줍니다. 결과는 가장 어려운 검증 작업에 있어서, 앞을 내다보는 데 시간을 투자하는 것이 추가적인 계산 비용을 감수할 만큼 가치가 있으며, 우리의 AI 시스템을 더 견고하고 신뢰할 수 있게 만드는 길임을 보여줍니다.

기술 요약: 신경망 검증을 위한 룩어헤드 브랜칭 (Lookahead Branching)

문제 정의

심층 신경망(DNN)이 안전이 필수적인 영역에 점점 더 많이 배치됨에 따라, 그 동작을 추론하기 위한 확장 가능한 정형 검증 기술이 필요해지고 있습니다. 최첨단 완전 검증 도구들은 분기 및 한계 결정(Branch-and-Bound, BaB) 프레임워크에 의존합니다. 이 접근 방식은 비선형 활성화 함수(예: ReLU)에 대해 재귀적으로 분기하고, 그 결과로 생성된 하위 문제들을 불완전한 검증기(incomplete verifiers)를 사용하여 분석하는 과정을 포함합니다.

BaB의 효율성은 브랜칭 휴리스틱(branching heuristic), 즉 어떤 불안정한 뉴런을 다음에 분기할지 선택하는 전략에 크게 좌우됩니다. 특히 탐색 트리의 상단에서 잘못된 선택을 하면 중복된 검증 노력이 발생하고 실행 시간이 증가할 수 있습니다. 최근의 **필터링된 스마트 브랜칭(Filtered Smart Branching, FSB)**과 같은 휴리스틱은 단일 레벨의 브랜칭을 시뮬레이션함으로써 성능을 개선했지만, 여러 레벨의 탐색 트리에 걸친 결정의 연쇄적인 효과를 포착하는 데는 종종 실패합니다. 기존의 대부분의 방법은 변수 경계(variable bounds)와 같은 국소적 정보(local information)를 활용하여 속도를 우선시하며, 이로 인해 장기적인 영향을 평가하지 못해 비효적인 브랜칭을 초래할 위험이 커집니다.

방법론

저자들은 결정적인 브랜칭 결정을 체계적으로 개선하기 위해, 정형 기법(SAT/SMT) 및 혼합 정수 선형 계획법(MILP)에서 채택된 일반적인 룩어헤드 브랜칭(Lookahead Branching) 전략을 제안합니다. 핵심 아이디어는 결정을 내리기 전에 후보 뉴런들에 대한 잠재적 분기를 시뮬레이션하여 그 다운스트림 효과를 측정하는 것입니다.

룩어헤드 템플릿

저자들은 조정 가능한 몇 가지 매개변수를 가진 템플릿 알고리즘(알고리즘 1)을 제시합니다:

사전 선택 전략 (Preselect Strategy): 계산 오버헤드를 완화하기 위해, 시뮬레이션을 수행할 불안정한 뉴런의 하위 집합을 선택합니다. 전략은 다음과 같습니다:
- 극성 기반 (Polarity-based): 경계 민감도(bound sensitivity)를 기준으로 활성화 상태가 가장 불확실한 뉴런을 선택합니다 (Marabou에서 사용됨).
- 점수 기반 (Score-based): BaBSR와 같은 기존 휴리스틱을 기반으로 상위 순위의 뉴한을 선택합니다 ( $\alpha$ - $\beta$ -CROWN에서 사용됨).
룩어헤드 깊이 ( $d$ ): 시뮬레이션할 재귀적 분기의 횟수입니다. 저자들은 MILP의 강력한 브랜칭(strong branching) 문헌에 착안하여, 특히 탐색 트리의 상단에서 깊이-2 룩어헤드를 조사합니다.
스코어링 함수 (Scoring Functions): 시뮬레이션된 브랜치의 품질을 평가하는 지표입니다:
- 뉴런 고정 기반 (Neuron-fixing-based): 경계 전파(bound propagation) 후에 이전에 불안정했던 뉴런이 얼마나 많은 '페이즈 고정(phase-fixed)' 상태(활성 또는 비활성)가 되었는지 계산합니다. 이는 두 브랜치 모두에서 많은 뉴런을 고정하는 균형 잡힌 분기를 선호합니다.
- 경계 감소 기반 (Bound-reduction-based): 변수 경계의 감소량 또는 결정 임계값(decision thresholds)으로의 근접도를 측정합니다.
페이즈 고정 (Phase Fixing): 룩어헤드의 핵심 결과물은 시뮬레이션 중에 변수 경계를 조이는 능력입니다. 만약 시뮬레이션된 분기가 특정 뉴런의 경계를 엄격하게 양수 또는 음수로 보장한다면, 해당 뉴런의 페이즈는 "고정"됩니다. 이러한 결과는 유효한 렘마(lemma)를 도출하거나 탐색 공간을 제거하는 데 사용될 수 있습니다.

인스턴스화 (Instantiations)

이 방법은 두 가지 서로 다른 BaB 기반 검증기에 인스턴스화되었습니다:

Marabou: CPU 기반 SMT 검증기입니다. 저자들은 극성 기반 사전 선택 전략, 깊이-2 룩어헤드, 그리고 뉴런 고정 지표를 사용합니다. 여기서는 페이즈 고정이 활성화됩니다.
$\alpha$ - $\beta$ -CROWN: GPU 가속 경계 전파 검증기입니다. 저자들은 사전 선택을 위해 BaBSR을, 깊이-2 룩어헤드를, 경계 감소 지표를 사용합니다. 여기서는 $\alpha$ -CROWN의 적응형 ReLU 규칙이 사전 활성화 경계가 타이트해질 때 경계를 느슨하게 만들 수 있으므로, 페이즈 고정 로직을 사용하지 않습니다 (즉, 페이즈 고정이 사용되지 않음).

주요 기여

일반 프레임워크: 본 논문은 사전 선택, 깊이, 평가 지표를 매개변수화하여 모든 브랜치 앤 바운드 검증기에 룩어헤드를 통합할 수 있는 일반적인 레시피를 정의합니다.
FSB의 통합: 저자들은 현재 최첨단 휴리스틱인 필터링된 스마트 브랜칭(FSB)이 룩어헤드 전략(구체적으로는 BaBSR을 기본 휴리스틱으로 하는 깊이-1 룩어헤드)의 특수한 인스턴스로 볼 수 있음을 입증합니다.
렘마 생성: 룩어헤드 과정은 브랜칭 결정을 개선하는 것 외에도, 강화된 경계와 같이 추가적인 정보를 생성하여 탐색 공간을 더욱 효과적으로 제거할 수 있는 유효한 렘마를 도출할 수 있게 합니다.
경험적 검증: 이 방법은 두 가지 근본적으로 다른 솔버 패러다임(SMT 기반 및 GPU 경계 전파 기반)에서 구현 및 평가되어 광범위한 적용 가능성을 보여줍니다.

결과

저자들은 여러 벤치마크(NAP, NN4Sys, MNIST, CIFAR, TinyImageNet)에 대해 기존 휴리스틱(BaBSR, Pseudo-Impact, FSB)과 룩어헤드 브랜칭을 비교 평가했습니다.

Marabou: 룩어헤드 브랜칭은 BaBSR 및 Pseudo-Impact 휴리스틱 모두에서 해결된 인스턴스 수를 실질적으로 증가시켰습니다. NAP 벤치마크에서 룩어헤드는 BaBSR의 30개 대비 최대 47개의 인스턴스를 해결했습니다. 오버헤드로 인해 쉬운 인스턴스의 속도가 느려질 수 있지만, 개선된 브랜킹 품질이 어려운 인스턴스에서 우위를 점하여 상당한 속도 향상을 이끌어냅니다.
$\alpha$ - $\beta$ -CROWN: 룩어헤드는 FSB보다 일관되게 우수한 성능을 보였습니다. 전체 BaB가 필요한 UNSAT 인스턴스에서 룩어헤드는 15.4%에서 24.3% 사이의 속도 향상을 달お성했으며, FSB가 해결할 수 없었던 고유한 인스턴스들도 해결했습니다.
종합: 룩어헤드 통합은 검증 시간의 일관된 단축과 함께 평가된 도구 전반에서 최대 57% 더 많은 해결된 인스턴스를 기록했습니다.

의의 및 주장

본 논문은 룩어헤드 브랜칭이 완전한 신경망 검증 성능을 높이기 위한 범용적인 전략이라고 주장합니다. (특히 탐색 트리의 상단에서) 중요한 브랜칭 결정에 추가적인 계산을 투자함으로써, 이 방법은 국소적 휴리스틱이 놓치는 연쇄적인 효과를 포착합니다.

저자들은 이 연구를 "빠른" 결정을 내리는 것을 넘어, 국소적 정보에 기반한 결정을 체계적으로 연구한 작업으로 규정합니다. 저자들은 설계 공간이 매우 방대함(더 깊은 시뮬레이션이나 후기 단계의 주기적 호출 포함)을 언급하면서도, 현재의 결과가 제한적인 룩어헤드(깊이-2)만으로도 상당한 성능 이득을 얻을 수 있음을 입증한다고 밝힙s니다. 또한, 학습 기반 휴리스틱이 룩어헤드 템플릿 내에서 사전 선택 전략으로서 기능할 수 있음을 시사하며 이 작업을 보완합니다.

결론적으로, 룩어헤드 브랜칭은 SMT 기반 및 GPU 가속 검증기 모두의 성능을 효과적으로 개선하며, 이는 안전이 중요한 DNN 검증에서 검증 시간을 단축하고 해결 가능한 인스턴스 수를 늘리는 견고한 기술임을 보여줍니다.