Talking with Verifiers: Automatic Specification Generation for Neural Network Verification

이 논문은 자연어로 표현된 고수준의 요구사항을 자동으로 형식적 검증 쿼리로 변환하여 신경망 검증의 적용 범위와 실용성을 크게 확장하는 새로운 프레임워크를 제안합니다.

핵심

🎩 비유: "AI 검사관"과 "번역가"의 만남

상상해 보세요. 아주 똑똑한 **AI 검사관 **(Verification Tool)이 있습니다. 이 검사관은 AI 가 만든 결정이 안전한지, 해킹이나 실수로 망가지지 않았는지 수학적으로 증명하는 일을 합니다.

하지만 이 검사관은 매우 까다롭고 고집이 세요.

• "이 사진의 3 번 픽셀부터 50 번 픽셀까지 밝기를 10% 바꾸면 결과가 바뀌지 않아야 해!"라고만 이해합니다.
• "새의 부리가 가려져도 새를 제대로 알아봐야 해!" 같은 자연스러운 말은 전혀 이해하지 못합니다.

지금까지 우리가 AI 를 검증하려면, 이 까다로운 검사관에게 수학 공식처럼 딱딱한 숫자로만 말해야 했습니다. 하지만 일반인이나 전문가들은 "새의 부리"나 "차의 앞유리" 같은 의미 있는 개념으로 이야기하고 싶죠.

이 논문은 바로 이 **간극 **(Gap)을 해결하는 **새로운 번역가 **(Translator)를 소개합니다.

---

🌉 이 논문이 해결한 문제: "의미"를 "숫자"로 바꾸는 마법

저자들은 "AI 검사관"을 바꾸지 않고, 그 앞에 "번역가"를 세워두는 것이 핵심 아이디어라고 말합니다.

1. 상황: "새의 부리가 가려져도 괜찮아야 해!"

사용자가 이렇게 말합니다.

"이 사진의 새 부리가 가려져도, AI 가 여전히 '새'라고 인식해야 해."

기존 방식에서는 이 말을 어떻게 해야 할까요?

• "어떤 사진이냐?"에 따라 부리의 위치가 다릅니다.
• 그래서 사람이 일일이 "부리 위치는 (x, y) 좌표야"라고 찾아서 검사관에게 입력해야 했습니다. 이건 너무 귀찮고 실수하기 쉽죠.

2. 새로운 방식: 3 단계 자동화 프로세스

이 논문이 제안하는 시스템은 LLM(대형 언어 모델)이 3 단계를 거쳐 자동으로 해결합니다.

1. **의미 파악 **(Parser)

   • "새 부리"와 "가려짐"이라는 단어를 듣고, "아, 사용자는 부리라는 사물을 찾고, 그 부분을 가리는 실험을 하려는구나"라고 이해합니다.
   • 비유: 통역사가 "부리가 가려지면 어떡하지?"라는 말을 듣고 "오, 부리 좌표 찾아서 가리는 실험을 하라는 뜻이군!"이라고 해석하는 것.

2. **위치 찾기 **(Detector)

   • AI 가 사진을 보고 "여기! 새 부리가 여기 있네!"라고 **정확한 좌표 **(박스)를 찾아냅니다.
   • 비유: 사진 속의 부리를 찾아내서 "여기 (x, y) 좌표가 부리야!"라고 표시하는 것.

3. **검증 명령서 만들기 **(Generator)

   • 이제 검사관에게 "부리 좌표 (x, y) 를 가려도 결과가 바뀌지 않아야 해"라는 수학적인 명령을 자동으로 만들어서 전달합니다.
   • 비유: 검사관에게 "부리 좌표만 가려서 테스트해!"라고 딱 맞는 명령서를 건네주는 것.

---

📊 실제로 잘 작동했을까요? (실험 결과)

저자들은 이 시스템을 두 가지 분야에서 시험해 봤습니다.

1. **신용 점수 **(표 형태의 데이터)

   • "50 세 미만 신청자의 신용 등급은 나이와 무관해야 해"라는 말을 입력하면, 시스템이 자동으로 '나이'라는 열을 찾아서 검증합니다.
   • 결과: 거의 100% 정확도로 의도를 파악했습니다.

2. **새 사진 **(이미지 데이터)

   • "새의 부리가 가려져도 새를 알아볼 수 있어야 해"라고 입력했습니다.
   • 시스템이 사진 속 부리를 찾아내고, 그 부분만 가린 이미지를 만들어 검증했습니다.
   • 결과: 부리를 찾는 데는 약간의 실수가 있었지만 (약 55%), 여러 방법을 섞으면 83% 이상 성공했습니다. 중요한 건, 사람이 일일이 좌표를 찾을 필요 없이 자연어로 명령할 수 있게 되었다는 점입니다.

---

💡 왜 이 연구가 중요할까요?

이 연구의 핵심은 "새로운 AI 를 만드는 게 아니라, 기존 도구를 더 똑똑하게 연결하는 것"입니다.

• 기존: 전문가만 "수학 언어"로 AI 를 검증할 수 있었음. (고난이도 게임)
• 이제: 누구나 "일상 언어"로 AI 의 안전성을 검증할 수 있게 됨. (쉬운 게임)

마치 스마트폰이 등장하기 전에는 전화를 걸려면 복잡한 코드를 입력해야 했지만, 지금은 "엄마에게 전화해"라고 말하면 알아서 연결해 주는 것과 같습니다.

이 기술이 발전하면, 자율주행차나 의료 AI 같은 중요한 시스템을 개발할 때, "비 오는 날에 보행자가 잘 보이나요?" 같은 질문을 쉽게 던져서 안전성을 확인할 수 있게 될 것입니다.

🚀 결론

이 논문은 **"AI 의 안전성을 검증하는 문턱을 낮추는 번역기"**를 만들었습니다. 복잡한 수학 코드를 몰라도, 우리가 일상에서 쓰는 말로 AI 가 "새의 부리"나 "비 오는 날" 같은 상황을 안전하게 처리하는지 확인할 수 있게 해주는 혁신적인 다리를 놓은 것입니다.

기술 요약

1. 문제 정의 (Problem)

심층 신경망 (DNN) 은 자율 주행, 의료 진단 등 안전이 중요한 분야에서 광범위하게 사용되고 있으며, 이에 따라 모델의 정확성을 수학적으로 보장하는 공식 검증 (Formal Verification) 기술이 발전해 왔습니다. 그러나 기존 검증 도구들은 다음과 같은 심각한 한계를 가지고 있습니다.

• 저수준 (Low-level) 제약 조건 의존성: 기존 도구들은 입력과 출력에 대한 고정된 수치적 제약 (예: $L_p$ 노름 내의 교란, 특정 좌표의 값 변화) 으로만 명세를 표현할 수 있습니다.
• 의미론적 격차 (Semantic Gap): 실제 사용자는 "50 세 미만의 신청자에 대한 신용 결정은 변하지 않아야 한다"거나 "새의 부리가 가려져도 분류가 정확해야 한다"와 같은 고수준의 의미론적 (Semantic) 명세를 원합니다.
• 수동 변환의 비효율성: 이러한 고수준 명세를 검증 도구가 이해할 수 있는 저수준 수치 제약으로 변환하는 과정은 수동으로 수행되어야 하며, 이는 오류가 발생하기 쉽고 전문 지식이 요구되어 검증 기술의 실제 적용을 저해합니다. 특히 이미지나 오디오와 같이 비정형 데이터의 경우, 특정 객체 (예: '부리') 의 위치가 입력마다 달라 고정된 좌표로 명세화하는 것이 불가능합니다.

2. 방법론 (Methodology)

이 논문은 기존 검증 알고리즘을 변경하지 않고, **자연어 명세를 공식 검증 쿼리로 자동 변환하는 통합 레이어 (Integration Layer)**를 제안합니다. 이 파이프라인은 세 가지 주요 단계로 구성됩니다.

A. 파이프라인 구조 (Grounding Pipeline)

1. 파싱 (Parsing):
   • **LLM(대형 언어 모델)**을 사용하여 사용자의 자연어 명세 ($P$) 를 분석합니다.
   • 명세에서 **목표 객체 (Semantic Objects)**와 **연산 (Operations, 예: 가리기, 노이즈 추가)**을 추출합니다.
2. 검출 (Detection / Grounding):
   • 시각/오디오 모델을 사용하여 구체적인 입력 데이터 ($x$) 에서 파싱된 객체의 위치를 찾습니다.
   • 이미지: 오픈-어휘 (Open-vocabulary) 객체 탐지 모델 (예: Grounding DINO) 을 사용하여 텍스트로 설명된 객체의 바운딩 박스 좌표를 추출합니다.
   • 오디오: (논의 단계) 오픈-어휘 사운드 이벤트 로컬라이제이션 모델을 사용하여 시간 구간을 추출합니다.
   • 표형 데이터 (Tabular): 파싱된 속성 이름을 입력 차원 (Feature Index) 으로 매핑합니다.
3. 명세 생성 (Specification Generation):
   • 추출된 좌표/구간과 연산을 기반으로 **수치적 검증 쿼리 ($P_x$)**를 생성합니다.
   • 생성된 쿼리는 기존 검증기 (Verifier) 가 처리할 수 있는 표준 형식 (예: 특정 영역에 대한 로컬 로버스트니스) 으로 변환됩니다.
   • 최종적으로 기존 검증기에 입력되어 SAFE(안전) 또는 UNSAFE(반례 존재) 결과를 반환합니다.

B. 핵심 아이디어

• 기존 기술의 재사용: 새로운 검증 알고리즘을 개발하는 대신, LLM 과 VLM(비전 - 언어 모델) 과 같은 최신 기초 모델 (Foundation Models) 을 검증 파이프라인에 연결합니다.
• 구체화 (Grounding): 추상적인 자연어 명세를 구체적인 입력 샘플에 기반한 수치적 제약 조건으로 '구체화'하여, 기존 검증 도구가 이를 처리할 수 있게 합니다.

3. 주요 기여 (Key Contributions)

1. 사용성 중심 명세 격차의 규명: DNN 시스템의 배포에 따라 고수준 의미 명세의 필요성이 증가하고 있으나, 이를 저수준 제약으로 변환하는 수동 과정이 주요 병목 현상임을 지적했습니다.
2. 자동 명세 생성 메커니즘 제안: 자연어로 표현된 사용자 의도를 식별하고, 이를 의미론적 객체와 연산으로 매핑하여 공식 검증 명세로 변환하는 자동화 파이프라인을 설계했습니다. 이는 표형, 이미지, 오디오 등 다양한 도메인에 적용 가능합니다.
3. 실증적 적용 가능성 입증: 기존 검증 백엔드를 수정하지 않고도, 자연어 기반의 복잡한 의미 명세 (예: "새의 부리가 가려져도 분류가 정확해야 함") 를 검증할 수 있음을 실험을 통해 증명했습니다.

4. 실험 결과 (Results)

연구팀은 **Statlog(신용 평가 데이터)**와 CUB-200-2011(조류 분류 이미지) 데이터셋을 사용하여 파이프라인을 평가했습니다.

• 파싱 정확도 (Parsing Accuracy):
  • GPT-5 Mini 와 Gemini 3 Flash 를 사용하여 명세에서 객체와 동작을 추출한 결과, 85%~100% 의 높은 정확도를 달성했습니다.
  • 특히 GPT-5 Mini 는 Statlog 데이터셋에서 동작 인식 정확도 100% 를 기록했습니다.
• 객체 검출 정확도 (Object Detection):
  • 이미지 도메인에서 오픈-어휘 검출 (Grounding DINO) 을 적용한 결과, 단일 설정에서는 최대 55% 의 정확도를 보였습니다.
  • 그러나 여러 설정 (Loose/Tight 모드 등) 을 조합 (Disjunction) 했을 때, 올바른 영역을 찾은 성공률은 **83%**까지 상승했습니다. 이는 다중 모드 앙상블이 해결 과제를 극복할 수 있음을 시사합니다.
• 정성적 평가:
  • "아래쪽의 보라색 가시가 더 시끄러워지면 예측이 변할 수 있는가?"와 같은 복잡한 자연어 질문을 성공적으로 처리하여, 해당 영역 (보라색 가시) 에만 국한된 로컬 로버스트니스 검증 쿼리를 생성하고 반례를 찾아내는 것을 확인했습니다.

5. 의의 및 결론 (Significance & Conclusion)

• 검증 접근성 확대: 이 프레임워크는 공식 검증 기술의 진입 장벽을 낮추고, 비전문가도 자연어로 복잡한 안전 요구사항을 검증할 수 있게 합니다.
• 모듈형 설계: 검증 엔진 자체를 수정할 필요가 없어, 기존에 존재하는 모든 강력한 검증 도구 (Marabou, Reluplex 등) 와 즉시 호환됩니다.
• 미래 전망: 현재는 이미지와 표형 데이터에 초점을 맞추었으나, 향후 비디오 검증, 오디오 이벤트의 시간적 제약 지원, 그리고 바운딩 박스 단계를 넘어 픽셀 단위 분할 (Segmentation) 로의 정밀화 등을 통해 확장될 수 있습니다.

결론적으로, 이 논문은 자연어와 형식 검증 사이의 간극을 메우는 혁신적인 통합 레이어를 제시함으로써, DNN 검증 기술이 실제 세계의 고수준 안전 요구사항을 충족하는 데 필수적인 역할을 할 수 있음을 보여주었습니다.