핵심 요약

  • AI 위험에 관한 전망은 측정된 사실과 구분해야 한다. 발표자들은 불확실한 재앙 확률을 단정하기보다 안전 연구와 구체적인 방어 기술에 투자해야 한다고 주장했다.
  • AI와 형식 검증을 결합하면 코드가 정해진 조건을 만족하는지 수학적으로 확인할 수 있다. 다만 무엇을 보장할지 정하는 명세와 그 명세가 개발자의 의도에 맞는지는 별도의 문제다.
  • 항공 안전에서 발전한 실패 탐색과 확률 추정 기법은 언어 모델 평가에도 적용할 수 있다. 그러나 실패의 정의와 시뮬레이터의 신뢰성이 결과를 좌우한다.
  • 안전은 배포 전 검증으로 끝나지 않는다. 실행 중 감시, 독립 평가, 사고 분석, 사람을 통한 공격에 대한 방어가 함께 필요하다.

위험 전망과 관측된 사실을 구분한다

Y Combinator의 이번 Paper Club은 AI 안전을 둘러싼 논의를 검증 가능한 주장으로 옮기는 데 초점을 맞췄다. 진행자는 AI가 스스로 의지를 갖고 인류를 해치는 시나리오보다, 악의적인 행위자가 강력한 모델을 이용해 사이버 공격 등을 더 쉽게 수행하는 위험을 우선적인 우려로 꼽았다.

그는 Hugging Face 관련 보안 사건을 예로 들며, 모델이 자발적으로 폭주했다는 설명과 특정 작업을 지시받은 실험에서 문제가 발생했다는 설명을 구분해야 한다고 주장했다. 해당 실험에서는 사고를 포착할 수 있었던 추론 과정 감시와 운영 환경의 보호 장치가 꺼져 있었다는 것이 그의 설명이다.

인류 멸종 가능성을 묻는 설문을 해석할 때도 시간 범위를 보존해야 한다고 지적했다. 그가 소개한 연구의 질문에는 무기한의 미래나 향후 100년이 등장하며, 이를 곧바로 향후 10년의 위험 수치로 옮길 수 없다는 것이다.

클라크 배럿 역시 미래의 불확실성이 크므로 AI 안전 연구에 투자할 이유가 있다고 봤다. 동시에 실제 확률을 모르는 상태에서 최악의 결과를 확실한 미래처럼 강조하는 것은 도움이 되지 않는다고 말했다.

AI가 만든 코드를 수학적으로 확인한다

배럿이 제시한 접근은 AI와 형식 검증, 즉 코드가 정해진 성질을 만족하는지 수학적으로 증명하는 방법의 결합이다. AI는 복잡한 데이터 처리와 코드 생성에 강하지만 결과의 정확성을 보장하지 못한다. 자동 추론 도구는 정해진 논리와 조건에 따라 증명을 확인하는 역할을 맡는다.

그가 소개한 CS lib 프로젝트는 여러 언어의 프로그램을 공통 중간 언어로 옮기고, 이를 정리 증명 시스템 Lean에서 확인할 조건으로 바꾸는 것을 목표로 한다. Lean은 증명의 각 단계를 검사한다. 발표에서는 Rust 코드에서 나온 35개 증명 목표 대부분을 자동 추론 도구로 해결하고, 남은 목표도 정의를 펼친 뒤 같은 도구를 다시 적용해 완료하는 시제품을 보여줬다.

증명 과정 전체를 AI에 맡길 필요는 없다. 배럿은 연구실에서 만든 Lean SMT가 많은 정리를 CPU에서 밀리초 단위로 증명할 수 있다며, 일부 작업에서는 기존 자동 추론 기법이 AI보다 저렴하고 효과적이라고 설명했다.

영어 요구사항에서 구조화된 명세를 만들고, 사람이 이를 승인하면 코드와 증명을 생성하는 도구도 시연했다. 이 도구는 검증 과정에서 명세가 바뀌지 않았는지도 확인했다. 배럿은 최근 공개한 논문에서 약 3만 줄의 Rust 암호 라이브러리를 에이전트로 11시간 만에 자동 검증한 결과를 보고했다고 밝혔다. 이는 그가 제시한 특정 사례의 성과다.

증명의 범위는 명세와 가정이 정한다

코드를 증명하려면 먼저 코드가 만족해야 할 성질을 정해야 한다. 이것이 명세다. 배럿은 초기화되지 않았거나 허용 범위를 벗어난 메모리에 접근하지 않는다는 조건처럼 여러 프로그램에 공통으로 적용할 수 있는 명세를 예로 들었다. 은행 소프트웨어라면 일련의 거래 전후에 총금액이 보존된다는 조건을 생각할 수 있다고 설명했다.

AI가 명세 작성을 도울 수는 있지만, 생성한 명세가 개발자의 실제 의도와 일치한다는 보장은 남아 있다. 배럿은 이 간극을 인정하며 이를 좁힐 도구와 에이전트가 연구 과제라고 말했다.

그는 AI와 형식 기법을 결합하면 향후 3~5년 안에 시스템 보안이 크게 달라질 것이라는 강한 전망도 내놨다. 다만 토론에서는 증명은 항상 특정 가정에 대한 증명이라는 제한을 분명히 했다. 메모리 안전성이 증명된 코드에 대해 버퍼 오버플로 공격을 배제하는 것과, 현실 세계 전체에서 아무 문제도 발생하지 않는다고 보장하는 것은 범위가 다르다.

배럿은 고양이와 개를 구분하는 인식망을 예로 들며, 무엇이 고양이인지부터 형식적으로 명세하기 어렵다고 설명했다. 거대한 언어 모델 전체의 행동을 증명하는 일도 현실적으로 어렵다고 봤다. 그가 제안한 방향은 모델 전체의 완전한 증명보다 시스템의 경계를 보호하는 접근이다.

드문 실패를 찾아 확률을 추정한다

이어진 항공 안전 연구 발표는 시스템을 실제로 배포할 만큼 안전하다고 판단하려면 어떤 근거가 필요한지 다뤘다. 항공기 충돌 회피 시스템 ACAS X 개발에서 목표로 삼은 치명적 실패 확률은 비행시간당 약 10억 분의 1이었다.

이 정도로 드문 사건은 무작정 시뮬레이션하기 어렵다. 해당 확률이라면 평균적으로 실패 한 번을 관측하는 데 약 10억 시간의 모의 비행이 필요하다. 서로 멀리 떨어져 위험하지 않은 항공기 상황을 계속 계산하는 대신, 현실을 대표하면서도 위험한 상황에 탐색을 집중해야 한다.

발표에서는 실패가 발생하는 조건을 찾는 방법과 실패 확률을 추정하는 방법을 구분했다. 전자에 쓰이는 적응형 스트레스 테스트는 가능한 상황을 탐색해 시스템이 무너지는 조건을 찾는다. 후자에 쓰이는 중요도 샘플링은 중요한 상황을 더 자주 뽑되, 원래 분포와 탐색에 사용한 분포의 확률 비율로 결과를 보정하는 방법이다. 실패 확률을 추정하려면 신뢰할 수 있는 현실 모델이 필요하다.

가장 쉽게 찾을 수 있는 실패 하나만으로는 충분하지 않을 수도 있다. 발표자는 넘어지는 진자를 예로 들어, 일반적인 탐색이 한쪽 방향의 실패에 집중할 수 있는 반면 확산 모델을 이용한 실패 샘플링은 양쪽 방향을 함께 포착할 수 있다고 설명했다.

이 연구는 언어 모델 평가로도 이어졌다. 연구진은 Llama Guard로 유해성을 측정하고, 모델이 해당 문장에 부여하는 가능성과 관련된 지표인 퍼플렉서티를 함께 사용해 발생 가능성이 높은 유해 사례를 찾았다. 다만 항공기의 위험 상황보다 언어의 유해성을 정의하기가 모호하며, 여기서는 또 다른 신경망의 판단에 의존한다는 한계가 있다. 같은 방법을 적용한다고 해서 언어 모델이 자율주행이나 항공 시스템과 같은 수준의 안전성을 얻는다고 단정할 수는 없다.

안전 장치를 겹치고 평가 기준도 감시한다

발표자는 현실과 상호작용하는 시스템의 실패 확률을 무조건 0으로 만들 수 있다고 보지 않았다. ACAS X도 특정 상황에서는 실패하는 시뮬레이션이 존재하지만, 그 상황이 극히 드물다는 설명이다. 형식 검증 역시 현실을 표현한 모델의 가정과 불확실성 범위가 충분히 타당한지 살펴야 한다.

항공 안전의 스위스 치즈 모형은 이런 한계를 다루는 방식이다. 비행 고도 분리, 항공 관제, 충돌 회피 시스템처럼 여러 방어층을 두고, 각 층의 취약점이 한 경로로 겹치지 않도록 한다. AI에서도 기술적 검증과 더불어 사람을 속여 접근 권한을 얻는 공격에 대한 보호가 필요하다는 논의가 이어졌다.

배포 후에는 입력 센서, 시스템 내부 상태, 출력에 대한 감시를 계속해야 한다. 평가용 벤치마크도 감시 대상이다. 언어와 유해성의 기준이 변하면 기존 평가가 현재의 위험을 제대로 반영하지 못할 수 있기 때문이다. 토론에서는 분포 변화를 추적하고, 벤치마크에 버전 관리와 오류 신고·수정 절차를 적용해야 한다는 의견이 나왔다.

독립 평가는 재검증할 수 있어야 한다

안전 평가의 독립성도 주요 의제였다. 항공 분야의 독립 사고 조사와 처벌을 목적으로 하지 않는 안전 보고 체계가 참고 사례로 제시됐다. 사고와 이상 징후를 공유하고 원인을 분석할 수 있어야 한다는 취지다.

배럿은 평가 기관이 독립적이라고 주장하는 데서 더 나아가, 다른 사람이 직접 확인할 수 있는 증명서를 산출하는 것을 목표로 제시했다. 안전하다는 결론뿐 아니라 그 결론을 재검증할 근거를 제공하겠다는 구상이다.

AI가 시스템 관리까지 맡는 방안에는 책임 문제가 뒤따랐다. 오류가 발생했을 때 누가 책임지는지, 공급 기업이 법적 책임을 감수할 준비가 돼 있는지 따져야 한다는 것이다. 배럿은 AI를 감시와 방어에 활용하더라도 사람이 관여하는 구조가 필요하다고 말했다.

이번 논의에서 안전은 하나의 증명이나 점수로 완성되는 속성이 아니었다. 코드에 대해 보장할 수 있는 성질을 명확히 하고, 현실 모델의 한계를 밝히며, 실패를 탐색하고 배포 후에도 감시하는 과정이었다. 그 과정에서 무엇을 확인했고 무엇이 여전히 가정으로 남아 있는지를 구분하는 일이 핵심이었다.