콘텐츠로 이동

검증이 신뢰를 대체할 때 — 수학적 확실성의 외주화와 알고리즘 판정의 정당성 구조

증명을 확인하는 사람은 누구인가

형식적 검증은 신뢰를 제거하지 않는다. 그것은 신뢰가 놓이는 위치를 이동시킨다.

이 명제를 논증하려면 수학적 확실성에 관한 지배적 통념을 먼저 충실하게 재구성해야 한다. 통념의 핵심은 단순하다. 수학적 증명은 공리와 추론 규칙에 의해 각 단계가 논리적으로 연결되므로, 원칙적으로 충분한 시간과 훈련을 갖춘 누구나 그 타당성을 직접 확인할 수 있다. 이 확인 가능성이 수학적 지식의 특별한 지위를 뒷받침한다. 권위에 기대는 것이 아니라 논리적 필연성을 따라가는 것. 수학적 확실성은 이 의미에서 투명하고, 그 투명성이 신뢰의 근거다.

이 통념이 현대 수학 실천에서 실제로 유지되는지를 두 사례가 보여준다.

1976년, 케네스 애플(Kenneth Appel)과 볼프강 하켄(Wolfgang Haken)이 사색 정리(four-colour theorem)를 증명했을 때, 수학계의 반응은 여러 방향으로 갈렸다는 것이 당시 기록이 전한다. 증명이 틀렸기 때문이 아니었다. 그 증명은 1,936개의 구성(reducible configuration)을 컴퓨터가 1,000시간 이상 점검하는 방식으로 구성되었다. 어떤 수학자도 그 전 과정을 처음부터 끝까지 직접 따라갈 수 없었다. 투명성이라는 요건 자체가 무너지고 있었다.

케플러 추측(Kepler conjecture)의 경우는 더 구조적이다. 1998년 토머스 헤일스(Thomas Hales)는 300쪽에 달하는 증명을 제출했고, 12명의 검토자가 4년에 걸쳐 검토한 끝에 "99% 정확하다"는 평가를 내렸다. 100%가 아니었다. 헤일스는 이 불확실성에 만족하지 않고 Flyspeck 프로젝트를 시작해, HOL Light와 Isabelle이라는 두 증명 보조기(proof assistant)를 이용한 형식 검증 작업을 약 11년에 걸쳐 완료했다. 2014년 8월 공식 완료가 선언되었고, 2017년 학술지 Forum of Mathematics, Pi에 게재되었다. 증명은 왜 믿을 수 있는가에서 다루는 것처럼, 이 과정 전체에서 "이해하는 주체"는 한 자리에 머물지 않았다.

신뢰가 이동하는 구조

두 사례가 드러내는 것은 다음과 같다. 검증 환경이 복잡해질수록 신뢰는 단계적으로 위치를 옮긴다.

첫 번째 이동은 개인 수학자에서 전문가 공동체로다. 현대 수학에서 어떤 증명도 단독으로 존재하지 않는다. 증명은 학술지 심사자들의 검토를 통과해야 하고, 이후에도 공동체 안에서 반복적으로 사용되고 인용되며 지속적으로 검증된다. 이 단계에서 이미 개인의 이해는 공동체의 수용 절차로 위임되어 있다.

두 번째 이동은 전문가 공동체에서 형식 시스템으로다. 형식 검증이란 증명의 각 단계를 컴퓨터가 처리할 수 있는 형식 언어로 번역하고, 증명 검증기(proof checker)가 그 논리적 정합성을 기계적으로 확인하는 과정이다. 이 단계에서 수학자가 직접 이해하는 것은 증명 전체가 아니라 형식 언어 체계의 규칙과 도구의 신뢰성이다.

세 번째 이동은 형식 시스템에서 소프트웨어, 구현, 표준, 인프라로다. HOL Light 같은 증명 보조기가 신뢰받는 이유는 작은 커널(kernel), 공개된 소스코드, 검증 가능한 설계 구조를 갖고 있기 때문이고, 그 설계 자체는 다시 다른 수준의 신뢰에 기댄다. 이 의존의 사슬은 어느 지점에서도 끊기지 않으며, 각 단계는 그 이전 단계를 검증 근거로 삼는다. 신뢰는 어떻게 검증으로 대체되는가가 사회적 신뢰 일반의 층위에서 분석하는 것처럼, 검증은 신뢰를 해소하는 것이 아니라 신뢰의 수요처를 재조직한다.

이 구조에서 수학적 확실성은 내용에 대한 직접 검토의 산물인 동시에, 점점 더 검증 인프라 안에서 특정 위치를 점유하는 것의 효과가 된다. 확실성 자체는 유지되지만, 그 확실성이 어떻게 생산되고 유통되는지의 인프라는 변했다.

알고리즘 판정과의 구조적 유사성

이 이동 구조는 알고리즘 판정 시스템에서 다시 나타난다.

알고리즘 판정이란 알고리즘이 개인에 관한 데이터를 처리해 산출한 값이, 그 개인의 사회적 자격이나 권리 배분에 영향을 미치는 판단으로 작동하는 것을 말한다. 대출 심사, 복지 수급 자격 판정, 취업 지원자 선별, 형사 재범 위험 예측이 그 사례다. 이 시스템들은 공통 구조를 가진다. 개별 판단자가 직접 설명하지 않아도, 시스템이 산출한 결과이기 때문에 받아들일 수 있다는 것.

형식 검증과 알고리즘 판정은 이 차원에서 구조적으로 유사하다. 두 영역 모두 "사람이 직접 이해하지 않아도 받아들일 수 있는 결과"를 생산하는 시스템이고, 두 영역 모두 그 수용을 위한 인프라를 구성한다. 수학에서 그 인프라는 증명 공동체, 형식 언어, 증명 검증기였다. 알고리즘 판정에서 그 인프라는 감사(audit), 성능 지표, 규제 승인 절차, 정확도 수치다.

이 구조적 유사성의 확인은 논점의 출발일 뿐이다. 계산 질서의 정당성은 어디에서 발생하는가가 제기하듯, 검증된 산출값이 어떤 조건에서 공적 판단의 지위를 얻는가는 별개의 질문이다. 두 영역이 이동 구조를 공유하더라도 다루는 문제의 종류가 다르다.

타당성과 정당성의 분기

수학적 검증이 다루는 문제는 타당성(validity)이다. 이 명제가 주어진 공리와 추론 규칙으로부터 규칙에 따라 도출되는가. 이 문제에는 인간 행위자에 대한 직접적 효과가 없다. 사색 정리가 참인지 여부는 지도의 색칠 방법에 관한 사실 문제이지, 누군가의 권리나 자격에 영향을 미치는 결정이 아니다.

알고리즘 판정이 다루는 문제는 정당성(legitimacy)이다. 이 산출값이 특정 개인의 권리, 자원 배분, 감시, 배제에 영향을 미치는 공적 판단으로 승인되어도 되는가. 이 문제에는 당사자가 있고, 이해관계가 있으며, 오류에 대한 책임과 이의제기의 가능성이 요구된다.

타당성은 형식적 정합성의 문제이고, 정당성은 사회적 승인의 문제다. 전자는 규칙 준수로 확인할 수 있지만, 후자는 규칙 준수만으로 성립하지 않는다. 정당성은 설명 가능성, 책임 귀속, 당사자 이의제기 가능성, 독립 검증, 사용된 변수의 사회적 근거를 요구한다.

알고리즘 판정이 수학적 확실성의 어휘를 차용할 때, 이 두 문제의 구분이 흐려진다. 정확도 수치, 형식 감사 통과, 규제 요건 충족은 각각 성능, 절차, 형식 요건에 관한 증거다. 그것들이 정당성의 충분조건으로 제시될 때, 검증 언어가 정당성 요구를 봉쇄하는 기제로 작동한다.

권위의 차용과 제약의 탈락

수학적 형식 검증에는 그 수용을 가능하게 하는 제약 조건들이 있다.

수학 공동체는 증명의 내용을 놓고 반박하고, 오류를 제시하고, 대안적 접근을 제안할 수 있다. 증명이 수용되는 것은 공동체의 지속적 비판적 검토를 통과했기 때문이다. Flyspeck 프로젝트가 의미 있는 이유도, 인간 검토자의 "99% 확신"을 더 강한 제도적 근거로 보완하려 했기 때문이다. 검증기의 설계 구조는 공개되고, 검증 방식은 기술적으로 재현 가능하다.

알고리즘 판정 시스템은 이 조건들을 어느 정도 상속하는가. 2014년부터 네덜란드 정부가 운용한 복지 사기 탐지 시스템 SyRI(Systeem Risico Indicatie)는 이 질문에 대한 제도적 응답을 제공한다. SyRI는 정부 데이터베이스에서 수집된 개인 정보를 결합해 사기 가능성이 높은 시민을 선별하는 알고리즘이었다. 저소득 지역과 이주 배경 주민 비율이 높은 지역을 집중적으로 대상으로 삼았으며, 위험 지표와 위험 모델의 작동 방식은 의회에도 공개되지 않았다. 2020년 2월 헤이그 지방법원은 이 시스템의 운용이 유럽인권협약 제8조(사생활 보호 권리)를 위반한다고 판결하고 즉각 중단을 명했다. 법원의 핵심 근거 중 하나는 투명성 결여였다. 시스템이 감사를 통과했더라도, 그 감사는 당사자가 이의를 제기할 수 있는 근거를 생산하지 못했다.

이것이 항소할 수 없는 정당성에서 다루는 구조다. 감사와 검증 통과가 정당성의 충분조건처럼 작동하면, 이의제기의 가능성 자체가 시스템 밖으로 밀려난다. 수학에서 형식 검증은 증명 공동체의 반박 가능성을 강화하기 위해 도입되었다. 알고리즘 판정에서 형식 감사는 그 구조적 기능이 역전될 수 있다.

검증 이후에 남는 것

검증이 신뢰를 대체한다는 언어 자체가 두 가지 서로 다른 문제를 지운다.

수학적 확실성에서 형식 검증으로의 이동은 신뢰의 재배치였고, 그 재배치는 형식 언어의 공개성·공동체의 비판 가능성·검증기 설계의 투명성이라는 제약 조건들을 수반했기 때문에 정당성을 유지했다. 알고리즘 판정도 구조적으로 동일한 이동 방식을 채택하지만, 수학적 확실성의 어휘를 차용할 때 성능·절차·형식 요건에 관한 증거가 정당성의 조건을 대체하는 방식으로 작동한다. 이들 증거 중 어느 것도 당사자 이의제기 가능성이나 책임 귀속 구조를 포함하지 않는다. 알고리즘 판정의 정당성은 검증 이후에도 설명 책임, 책임 귀속, 이의제기 가능성의 구조를 별도로 요구한다.

알고리즘 판정이 수학적 권위를 차용하는 방식의 핵심 구조적 문제는, 그 권위가 성립하기 위해 필요한 제약 조건들을 함께 상속하지 않는 데 있다.

이어 읽기

작성 정보

초안 작성: Claude · Claude Sonnet 4.6 · Low Adaptive Thinking
검토·개고: ChatGPT · GPT-5.5 Extended Thinking

참고자료

  • Appel, K. & Haken, W. (1977). Every planar map is four colorable. Illinois Journal of Mathematics, 21(3), 429–490.
  • Hales, T. et al. (2017). A formal proof of the Kepler conjecture. Forum of Mathematics, Pi, 5, e2. https://doi.org/10.1017/fmp.2017.1
  • Rechtbank Den Haag (2020). NJCM c.s. / De Staat der Nederlanden (SyRI). ECLI:NL:RBDHA:2020:1878. https://uitspraken.rechtspraak.nl/inziendocument?id=ECLI:NL:RBDHA:2020:1878
  • AlgorithmWatch (2020). How Dutch activists got an invasive fraud detection algorithm banned. https://algorithmwatch.org/en/syri-netherlands-algorithm/

인포그래픽

작성일: 2026년 5월 31일