6.18 형식 검증(Formal Verification)에서 불완전성 정리의 실천적 영향

1. 형식 검증의 정의와 목적

형식 검증(formal verification)은 시스템의 설계 또는 구현이 주어진 명세(specification)를 만족하는지를 수학적으로 엄밀하게 증명하는 방법론이다. 시험(testing)이 유한한 수의 실행 경로를 점검하여 오류의 존재를 탐지하는 것과 달리, 형식 검증은 가능한 모든 실행 경로에 대해 명세 충족을 보장한다. 에즈허르 데이크스트라(Edsger Dijkstra)의 유명한 경구—“시험은 오류의 존재를 보일 수 있으나, 오류의 부재를 보일 수 없다”—는 이 구분을 정확히 포착한다.

형식 검증의 대상은 하드웨어 회로, 소프트웨어 프로그램, 통신 프로토콜, 보안 정책 등 광범위하며, 항공우주, 의료기기, 원자력, 금융 시스템 등 안전 필수(safety-critical) 분야에서 특히 중요하다. 형식 검증은 시스템의 정확성에 대한 절대적 보장을 추구하며, 이 점에서 형식적 증명과 동일한 인식론적 기반 위에 서 있다.

2. 형식 검증의 주요 방법론

형식 검증은 크게 세 가지 방법론적 패러다임으로 분류된다.

**모델 검사(model checking)**는 시스템의 유한 상태 모델을 구축하고, 명세로 표현된 속성이 모든 가능한 상태에서 성립하는지를 자동으로 탐색한다. Clarke, Emerson, Sifakis가 독립적으로 개발한 이 기법은 시간 논리(temporal logic)—선형 시간 논리(LTL), 계산 트리 논리(CTL)—로 표현된 속성을 검증한다. 시스템의 상태 공간이 유한하면 검증은 원리적으로 결정 가능하나, 상태 폭발(state explosion) 문제가 실천적 제약으로 작용한다.

**연역적 검증(deductive verification)**은 프로그램의 정확성을 논리적 추론을 통해 증명한다. 호어 논리(Hoare logic)에서 프로그램의 정확성은 전조건(precondition) $P$ , 프로그램 $S$ , 후조건(postcondition) $Q$ 의 삼중 $\{P\} S \{Q\}$ 로 표현되며, 이는 “ $P$ 가 성립하는 상태에서 $S$ 를 실행하면 $Q$ 가 성립한다“를 의미한다. 연역적 검증은 이 삼중을 증명 규칙의 적용을 통해 입증한다.

**추상 해석(abstract interpretation)**은 프로그램의 구체적 의미론을 추상적 의미론으로 근사하여 분석한다. Cousot와 Cousot(1977)가 제안한 이 프레임워크에서, 프로그램 상태의 구체적 영역(concrete domain)은 추상 영역(abstract domain)으로 갈루아 연결(Galois connection)을 통해 연결되며, 추상 영역에서의 분석 결과가 구체적 영역의 속성에 대한 건전한(sound) 근사를 제공한다.

3. 불완전성 정리의 직접적 영향: 검증 대상의 명세 한계

불완전성 정리는 형식 검증에 여러 차원에서 실천적 영향을 미친다. 첫 번째 차원은 명세의 완전성에 관한 것이다.

형식 검증의 정확성은 명세의 정확성에 의존한다. 시스템이 명세를 만족함이 증명되어도, 명세 자체가 의도된 속성을 완전히 포착하지 못하면 검증의 실질적 가치가 제한된다. 불완전성 정리는 충분히 표현력 있는 형식 체계에서 모든 참인 속성을 형식적으로 기술할 수 없음을 함의한다.

구체적으로, 검증하고자 하는 시스템이 정수 산술을 수행하는 소프트웨어라면, 이 소프트웨어의 모든 가능한 정확성 속성을 단일 형식 체계 내에서 완전히 명세하는 것은 불가능하다. 항상 형식적으로 기술할 수 없는 속성이 존재하며, 이는 형식 검증이 달성할 수 있는 보장의 범위에 원리적 상한을 설정한다.

4. 라이스 정리와 프로그램 속성 검증의 결정 불가능성

라이스 정리(Rice’s theorem, 1953)는 불완전성 정리 및 정지 문제의 결정 불가능성으로부터 도출되는 결과로, 프로그램의 비자명한(nontrivial) 의미론적 속성은 모두 결정 불가능함을 증명한다. 여기서 비자명한 속성이란, 일부 프로그램은 만족하고 다른 프로그램은 만족하지 않는 속성이다.

형식적으로, 프로그램이 계산하는 함수의 속성 $\mathcal{P}$ 에 대해, 임의의 프로그램 $p$ 가 $\mathcal{P}$ 를 만족하는지 판정하는 알고리즘은 존재하지 않는다(단, $\mathcal{P}$ 가 비자명한 경우). 이 결과의 직접적 귀결로, “프로그램이 모든 입력에 대해 종료하는가”(정지 문제), “프로그램이 주어진 함수를 계산하는가”(함수 동치 문제), “프로그램이 특정 출력을 생성하지 않는가”(안전성 속성) 등의 문제는 일반적으로 결정 불가능하다.

이 결정 불가능성은 형식 검증이 모든 프로그램과 모든 속성에 대해 자동으로 완전하게 작동하는 것이 원리적으로 불가능함을 의미한다. 형식 검증 도구는 특정 범주의 프로그램과 특정 유형의 속성에 대해 효과적으로 작동하도록 설계되며, 보편적 검증 도구는 존재할 수 없다.

5. 건전성과 완전성의 교환 관계

형식 검증 도구의 설계에서 불완전성 정리의 영향은 건전성(soundness)과 완전성(completeness) 사이의 교환 관계로 구체화된다.

건전한(sound) 검증 도구는 속성이 성립한다고 보고할 때 이것이 실제로 참임을 보장한다. 즉, 거짓 긍정(false positive)은 없으나 거짓 부정(false negative)—실제로는 속성이 성립하나 검증에 실패하는 경우—이 발생할 수 있다. 완전한(complete) 검증 도구는 속성이 실제로 성립하면 반드시 이를 확인하나, 거짓 긍정이 발생할 수 있다.

라이스 정리에 의해, 건전하고 완전하며 항상 종료하는 검증 도구는 비자명한 속성에 대해 존재할 수 없다. 실천적 형식 검증 도구는 이 세 가지 속성 중 하나 이상을 포기해야 한다.

추상 해석은 건전성을 유지하면서 완전성을 포기하는 전형적 접근이다. 추상 영역에서의 과잉 근사(over-approximation)는 건전성을 보장하나, 실제로 위반이 없는 경우에도 잠재적 위반으로 보고할 수 있다(거짓 경보, false alarm). 이 거짓 경보율의 관리는 추상 해석 기반 도구의 핵심적 실천적 과제이다.

제한 모델 검사(bounded model checking)는 완전성을 포기하고 유한한 깊이까지의 실행 경로만 검사하여 종료를 보장한다. 이는 깊이 제한 내의 오류를 탐지할 수 있으나, 제한을 초과하는 경로에서의 오류는 놓칠 수 있다.

6. 인공지능 시스템 검증에서의 특수한 어려움

인공지능 시스템, 특히 심층 신경망 기반 시스템의 형식 검증은 전통적 소프트웨어 검증을 넘어서는 고유한 어려움에 직면한다.

첫째, 신경망의 명세 문제이다. 전통적 소프트웨어에서 정확성 명세는 입출력 관계에 대한 논리적 조건으로 표현되나, 신경망의 “올바른” 행동을 형식적으로 명세하는 것은 본질적으로 어렵다. 영상 분류 신경망이 “고양이“를 올바르게 인식한다는 것을 수학적으로 정의하는 문제는 의미론적 수준의 기술을 요구하며, 이는 기호 접지 문제(symbol grounding problem)와 직결된다.

둘째, 입력 공간의 차원과 규모이다. 고해상도 영상을 처리하는 신경망의 입력 공간은 $\mathbb{R}^{d}$ ( $d$ 가 수백만 이상)이며, 이 고차원 공간에서의 체계적 탐색은 계산적으로 극단적으로 비용이 높다.

셋째, 비선형성과 불투명성이다. 심층 신경망은 다수의 비선형 활성화 함수의 합성으로 구성되며, 이 합성의 전역적 행동을 형식적으로 특성화하는 것은 현재의 수학적 도구로 제한적이다.

이러한 어려움에도 불구하고, 신경망의 특정 속성—특히 적대적 견고성(adversarial robustness)—에 대한 형식 검증 연구가 진전을 이루고 있다. Katz 등(2017)의 Reluplex 알고리즘(“Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks”)은 ReLU 활성화 함수를 갖는 신경망에 대한 SMT 기반 검증 절차를 제안하였다. 이 알고리즘은 입력 영역 $\mathcal{X}_0$ 에 대해 출력이 특정 안전 영역 $\mathcal{Y}_s$ 내에 있는지를 검증한다.

$\forall x \in \mathcal{X}_0: f_\theta(x) \in \mathcal{Y}_s$

그러나 이 검증의 계산 비용은 신경망의 규모에 따라 급격히 증가하며, 현재 실용적으로 검증 가능한 신경망의 규모는 산업적으로 사용되는 모델에 비해 매우 제한적이다.

7. 신뢰할 수 있는 컴퓨팅 기반에서의 불완전성

형식 검증 체계의 신뢰성은 궁극적으로 신뢰할 수 있는 컴퓨팅 기반(trusted computing base, TCB)—검증 도구 자체, 기반 논리, 운영 체제, 하드웨어—의 정확성에 의존한다. 불완전성 정리의 제2 정리에 의해, 충분히 강력한 형식 체계는 자기 자신의 무모순성을 증명할 수 없다.

이 제약은 형식 검증 도구의 자기 검증(self-verification)에 직접적으로 적용된다. 검증 도구 $V$ 가 형식 체계 $\mathcal{F}$ 내에서 작동하면, $V$ 의 정확성을 $\mathcal{F}$ 내에서 완전히 검증하는 것은 불가능하다. 이를 해결하기 위해 형식 검증 커뮤니티는 드 브라윈 기준(de Bruijn criterion)을 채택한다. 이 기준에 따르면, 복잡한 증명 탐색 엔진이 아니라 작고 검증 가능한 증명 검사기(proof checker)만이 TCB에 포함되어야 한다. 증명 탐색 엔진이 생성한 증명은 독립적인 증명 검사기에 의해 검증되며, TCB의 크기를 최소화함으로써 신뢰성을 극대화한다.

그럼에도 증명 검사기 자체의 정확성은 궁극적으로 형식적으로 보장될 수 없으며, 이는 형식 검증 체계의 인식론적 한계를 구성한다. Milner의 LCF 전통에 기반한 증명 보조기—HOL Light, Isabelle/HOL—는 이 한계를 인식하고, 증명 커널(proof kernel)의 크기를 최소화하여 수동 감사(manual audit)의 가능성을 확보한다.

8. 실천적 대응 전략

불완전성 정리의 제약에 대해 형식 검증 분야는 여러 실천적 대응 전략을 발전시켜 왔다.

명세의 계층적 분해는 전체 시스템 명세를 검증 가능한 부분 명세들의 계층으로 분해한다. 각 부분 명세의 검증은 관리 가능한 형식 체계 내에서 수행되며, 부분 검증 결과의 합성을 통해 전체 시스템에 대한 보장을 구축한다. 이 접근은 단일 형식 체계의 불완전성을 여러 체계의 상보적 사용으로 완화한다.

**가정-보장 추론(assume-guarantee reasoning)**은 구성 요소 간의 인터페이스 조건을 명시하고, 각 구성 요소가 다른 구성 요소의 보장 하에 자신의 명세를 만족함을 개별적으로 증명한다. 이 합성적(compositional) 접근은 전체 상태 공간의 직접 탐색 없이 시스템 수준의 속성을 검증할 수 있게 한다.

**실행 시간 검증(runtime verification)**은 정적 형식 검증이 결정 불가능한 속성에 대해, 시스템의 실행 중에 명세 위반 여부를 감시하는 보완적 접근이다. 이는 완전한 사전 검증의 불가능성을 인정하고, 실행 시점의 감시를 통해 안전성을 확보하는 실용적 전략이다.

9. 불완전성 정리와 형식 검증의 공존

불완전성 정리는 형식 검증의 무용성을 함의하지 않는다. 불완전성 정리가 보이는 것은 보편적으로 완전한 검증의 불가능성이지, 특정 시스템과 특정 속성에 대한 검증의 불가능성이 아니다. 실천적 형식 검증은 검증 대상과 속성의 범위를 적절히 제한함으로써 불완전성 정리의 제약 내에서 강력한 정확성 보장을 달성한다.

이 상황은 다음과 같이 요약된다. 불완전성 정리는 “모든 프로그램의 모든 속성을 검증하는 보편적 도구“의 존재를 부정하나, “특정 프로그램의 특정 속성을 검증하는 전문화된 도구“의 유효성은 부정하지 않는다. 형식 검증의 실천은 이 구분 위에 서 있으며, 불완전성 정리의 한계를 인식하면서도 그 한계 내에서 최대한의 보장을 추구하는 방법론적 태도가 이 분야의 성숙함을 반영한다.