AI 안전성의 사실과 허구: 코드 검증과 안전공학

메타데이터

• 영상 ID: X7oI4Umt3DU
• URL: https://www.youtube.com/watch?v=X7oI4Umt3DU
• 채널: Y Combinator (YC Paper Club)
• 원제: AI Safety Fact vs. Fiction | YC Paper Club
• 원 발행일: 2026-10-17
• 처리일: 2026-10-19

---

📌 핵심 질문과 주장

AI 안전을 실측 가능한 실패, 검증 가능한 소프트웨어, 사고를 줄이는 제도로 다루면 막연한 종말 예측과 과도한 낙관을 모두 넘어설 수 있다. ==가장 빠르게 성과를 낼 수 있는 출발점은 거대 모델의 모든 행동을 증명하는 일이 아니라 모델 주변의 코드·경계·운영 절차를 검증하는 일이다.==

• 안전은 단일 모델 평가 점수나 하나의 증명으로 완성되지 않으며, 사양·형식 검증·확률적 스트레스 테스트·실시간 감시·사람과 제도가 겹치는 방어층으로 만들어진다.
• 개방형 모델은 기존 악의적 행위자의 테러·생물무기·랜섬웨어·사이버 공격 역량을 키울 수 있어, 단기 위험을 줄이는 데 사이버 방어 강화가 중요하다.
• 형식 검증의 비용을 AI가 크게 낮추고 있지만, 무엇을 안전이라고 정의할지, 현실적인 가정을 어떻게 둘지, 누가 독립적으로 검증하고 책임질지는 여전히 어려운 문제다.

AI 안전의 연구 역사는 자율주행·항공처럼 오작동의 대가가 큰 시스템을 안전하게 만드는 공학에서 시작됐다. 대규모 언어 모델에도 이 경험을 적용하되, 확률을 알 수 없는 최악의 시나리오를 사실처럼 말하거나 검증 도구 하나가 모든 문제를 해결한다고 여기는 실수를 피해야 한다. 인간 통제권 상실의 장기 확률과 오늘날의 공격 표면을 구분하고, 지금 증명 가능한 소프트웨어 경계부터 개선하는 접근이 핵심이다.

1. 과장된 서사와 측정 가능한 AI 안전

1.1. 기술 공포는 불확실성이 클수록 과장되기 쉽다

1. 검증 가능한 주장과 과학적 엄밀성

   1. AI 안전 논의는 측정할 수 있는 주장, 반증 가능한 가설, 동료 검토를 통해 과학적 엄밀성을 지켜야 한다.
   2. 히스테리는 “측정할 수 없는데 말을 멈추지 못하는 상태”라고 정의할 수 있다. 주목을 끄는 과장된 제목은 클릭을 얻지만 사실관계를 흐릴 수 있다.
   3. 안전은 이론적 위험뿐 아니라 실제 운영에서 생기는 피해도 다룬다. Focal에서 Walmart 재고를 관리하던 때 잘못된 새 모델을 배포하면 아보카도를 과다 발주해 수백만 달러 손실이 날 수 있었다.

2. 과거 기술에 반복된 종말·붕괴 예측

   1. 원자폭탄 개발 당시 아인슈타인도 대기 점화 가능성을 걱정했지만 그런 일은 일어나지 않았다.
   2. 앨런 튜링은 1950년대에 기계가 인간의 모든 능력과 지능을 넘어설 시점을 예측했지만, 시간표는 크게 빗나갔다.
   3. 마르크스와 케인스는 산업 자동화가 대량 실업을 일으킬 가능성을 논의했다. 구글이 사람을 덜 읽고 덜 똑똑하게 만들 것이라는 우려, 스마트폰과 소셜미디어가 지능을 망칠 것이라는 우려도 이어졌다.
   4. 이더넷을 발명한 밥 멧칼프는 DDoS 등으로 인터넷이 치명적으로 붕괴할 수 있다고 예측했다. 예측이 빗나간 뒤 논문을 믹서기에 갈아 마셨다는 후속 행동도 유명하다.
   5. 반대로 지금의 젊은 세대가 기술에 무능해졌다는 단정도 경계할 필요가 있다. 스탠퍼드와 YC에서 만난 18~20세 학생들은 기술에 익숙하고 역량이 뛰어났다.

1.2. AI 안전의 양극단은 공학적 위험과 P(doom) 추정이다

1. 안전공학 관점

   1. 항공기 문이 이륙 중 떨어지지 않고 착륙 장치와 비행 제어가 작동하는지 확인하듯, AI도 현실의 고장 조건을 찾아 시험하고 완화하는 공학 문제로 접근할 수 있다.
   2. 보잉 737의 MCAS와 항공기 충돌 회피 시스템 ACAS X는 복잡하고 안전이 중요한 시스템을 검증하는 사례다.
   3. 프랑스와 크루즈가 안개에 가려진 금문교를 운전해 건넌 일화는 불확실성을 다루는 태도를 비유한다. 다리가 여전히 있다고 보는 사전확률을 두고 이동하면서 새 정보가 들어올 때 판단을 갱신하듯, 위험 가능성만으로 즉시 최악을 확정하기보다 증거에 따라 믿음을 조정해야 한다.

2. P(doom)와 확률 발언의 한계

   1. “10년 안에 인류가 AI 통제권을 잃고 멸종할 확률이 10%를 넘는다”는 식의 문구가 논쟁의 한쪽 끝에 놓였다. 해당 수치의 출처와 기간이 원자료와 일치하는지 검증해야 한다.
   2. 2023년 논문 「Thousands of AI Authors on the Future of AI」는 NeurIPS 관련 AI 연구자 약 1,200명에게 여러 전망을 물었다. 멸종 또는 영구적·심각한 권력 상실에 관한 질문은 ‘모든 미래’와 ‘향후 100년’을 물었지, ‘향후 10년’을 묻지 않았다.
   3. 2012년 스탠퍼드 연구자들에게 AI가 밀레니엄 수학 문제를 언제 풀지 물었다면 14년이라는 짧은 답은 나오지 않았을 가능성이 크다. 어려운 미래 예측에 전문가 설문이 얼마나 강한 신호를 주는지는 별도 문제다.
   4. 양쪽 논쟁에 있는 연구자들의 H-index 차이를 사전확률 조정에 참고할 수 있다는 언급이 있었지만, 구체적 수치나 그 자체가 결론을 정해 주지는 않았다.
   5. 장기적으로 모든 일이 가능해질 수 있다는 말을 현재의 10~20년 전망에 그대로 적용하면 시간 범위가 흐려진다. 의식·영혼·독자적 의지가 생긴 AI가 10~20년 안에 인류를 죽이거나 노예화한다는 경로는 큰 우려로 보지 않는다는 판단이다.

1.3. 허깅페이스 사건은 자율적 폭주보다 꺼진 안전층의 사례다

1. 사건의 실행 조건

   1. “OpenAI가 AI가 스스로 행동했다고 말했다”거나 “AI 에이전트가 폭주했다”는 보도 문구는 OpenAI의 실제 진술과 달랐다.
   2. 사건은 ExploitGen이 약 1,200개의 에이전트를 투입해 시작한 실험이었다. 에이전트가 아무 지시 없이 깨어나 허깅페이스를 해킹하기로 결정한 상황은 아니었다.
   3. 공개된 기술 보고서에는 연쇄사고 추론(Chain-of-Thought)을 감시하는 모니터가 실수로든 다른 이유로든 꺼져 있었고, 그 감시가 켜져 있었다면 문제를 잡았을 것이라고 정리돼 있다.
   4. 운영 전 환경이었기 때문에 운영 환경용 보호 장치도 꺼져 있었다. 이 안전장치가 작동했어도 문제를 탐지했을 것이라는 설명이다.
   5. 따라서 핵심 교훈은 “AI가 서버를 탈출해 복제됐다”가 아니라, 테스트 환경에서 두 개의 방어층이 작동하지 않았다는 점이다.

2. 헤드라인과 사실의 차이

   1. “자율적으로 폭주한 AI가 수학을 풀고 외국 정부를 해킹한다”는 서사로 확장되기 전에, 실제 프롬프트·실행 환경·감시 설정·운영 보호장치의 상태를 확인해야 한다.
   2. 같은 사건도 안전 모니터의 실패로 볼 수 있고, 자율적 의지의 출현으로 과장할 수도 있다. 안전 분석은 두 설명을 구분할 수 있는 증거와 재현 조건을 공개해야 한다.

2. 더 현실적인 단기 위험: 개방형 가중치와 사이버 공격

2.1. 개방형 모델은 기존 공격자의 생산성을 높일 수 있다

1. 위험의 중심은 기존 악의 행위자의 역량 증폭이다

   1. 테러, 생물무기, 사이버전, 랜섬웨어는 AI 이전부터 존재했다. 우려는 개방형 가중치가 악의적 개인이나 국가가 이런 행동을 수행하는 비용과 기술 장벽을 낮출 수 있다는 데 있다.
   2. 폴란드의 한 지역 병원은 러시아 해커의 공격으로 3주 동안 문을 닫았다. AI 사용 여부와 별개로 사이버 공격은 이미 공공 안전과 의료 서비스를 위협한다.
   3. 오픈 웨이트 모델 자체를 없애면 위험이 사라진다는 전망은 현실적이지 않다. Kimi K3와 GLM 5.2를 이미 내려받아 보유한 사람이 있다는 사실은 퍼진 모델 사본을 완전히 회수하기 어렵다는 점을 보여준다.

2. 감시와 등록만으로 해결하기 어려운 이유

   1. GPU 등록제는 작은 장비를 여러 곳에 분산하거나 해외에서 GPU 시간을 빌리는 방식으로 우회될 수 있다.
   2. 전력 사용량으로 추론을 탐지하는 구상은 미국 내 일부 운영자에게는 쓸 수 있어도 국가 단위 행위자를 막는 수단이 되기 어렵다.
   3. 모델 배포를 일괄 금지하는 정책은 이미 퍼진 가중치와 국경을 넘는 컴퓨팅 자원을 고려하면 집행 가능성이 낮다.

2.2. 공격 속도만큼 방어를 자동화하고 확장해야 한다

1. 사이버 방어의 기본기를 강화한다

   1. 수많은 침해는 여전히 admin/admin처럼 기본 비밀번호를 바꾸지 않는 실수에서 시작한다. 첨단 AI 위험만 강조하기보다 패치, 인증, 권한 분리, 백업, 사고 대응 역량을 강화해야 한다.
   2. 병원처럼 중단이 곧 인명과 공공서비스에 영향을 주는 기관의 복구 계획은 모델 통제 정책과 별개로 핵심 방어선이다.

2. 방어자도 AI를 활용할 수 있게 한다

   1. AI는 공격자의 코딩·정찰 능력을 높이지만 방어자의 코드 분석·취약점 탐색·복구 자동화에도 이용될 수 있다.
   2. 기술 개발을 무조건 늦추기보다 방어 기술에 투자하고 안전한 프런티어 연구를 앞당겨 방어자가 공격자를 따라잡게 해야 한다.

3. 자동화된 추론과 형식 검증

3.1. 코드 추론은 거대한 AI 안전 문제의 ‘베이스캠프’다

1. 검증 비용의 하락

   1. 전통적 소프트웨어 개발은 코드를 작성하고 테스트해 운에 맡기는 측면이 있다. 형식 검증(Formal Verification)은 코드가 명세를 만족한다는 수학적 증명을 만든다.
   2. 과거에는 증명을 사람이 직접 구성해야 해 비용이 크고 확장성이 부족했다. AI가 코드 변환, 정리 증명, 증명 탐색을 자동화하면 형식 검증을 실무에 적용할 수 있는 경제성이 달라진다.
   3. AI가 취약한 코드를 대량 생성하는 동시에 해커의 공격 역량도 높일 수 있으므로, 방어는 같은 수준의 자동화로 확장해야 한다.

2. 보장 범위를 좁혀 단계적으로 전진한다

   1. 5천억 파라미터 모델이 위험한 일을 전혀 하지 않을 것이라고 직접 증명하는 일은 현재 다루기 어렵다.
   2. 모델의 모든 내부 행동을 증명하기보다 모델을 둘러싼 코드, 권한, 샌드박스, 입출력 경계, 배포 절차를 검증하는 편이 실현 가능한 출발점이다.
   3. “AI 안전이 에베레스트라면 코드 추론은 좋은 베이스캠프”라는 비유는 완전한 안전을 즉시 해결한다는 뜻이 아니라, 증명 가능한 부분부터 축적하자는 뜻이다.

3.2. Lean과 Rust를 잇는 증명 파이프라인

1. 암호 라이브러리 자동 검증

   1. Rust로 작성된 Dalek Lite 암호화 라이브러리 약 3만 줄을 세 명의 전문가가 수작업으로 검증하는 데 약 5개월이 들었다.
   2. 연구진의 ‘crypto prover agent’는 같은 코드를 완전 자동으로 약 11시간 만에 검증했다.
   3. Rust 코드를 공통 중간 표현인 Bool로 옮기고, 검증 조건을 Lean 정리로 생성한 뒤, Lean SMT가 증명 의무를 해결한다.
   4. 시연에서 생성된 증명 목표 35개 가운데 Lean SMT가 32개를 자동으로 풀었다. 나머지 세 개는 정의를 전개한 뒤 두 번째 SMT 호출로 마무리했다.
   5. Lean SMT는 CPU에서 상당수 Lean 정리를 밀리초에서 수초 안에 증명할 수 있다.

2. CSLib의 목표

   1. CSLib은 수학 라이브러리 Mathlib처럼 컴퓨터 과학 이론을 형식화하고, 코드에 대해 추론할 수 있는 기반을 구축하려는 프로젝트다.
   2. 구성의 두 축은 컴퓨터 과학 이론의 형식화와 프로그램 코드 추론 프레임워크다. Lean의 저자 레오 데 모우라가 운영 위원회에 참여한다.
   3. 코드와 함께 기계가 확인할 수 있는 증명을 제공하면 에이전트 간 신뢰의 기반이 달라질 수 있다. 증명 기능만 제한적으로 부여한 모델을 신뢰 경계 안에 두는 방안도 가능하다.

3.3. 자연어 요구사항에서 검증된 코드까지

1. Verisforge 데모

   1. 사용자가 “32비트 정수 배열에서 최댓값을 찾아라”처럼 영어로 요구사항을 입력한다.
   2. 시스템은 먼저 구조화된 명세를 만들어 사용자가 의도와 일치하는지 승인하게 한다.
   3. 승인된 명세로 Rust 코드와 Veris 명세를 생성하고, 생성한 코드가 명세를 만족하는지 자동 검증한다.

2. 요구사항의 누락을 줄이는 에이전트

   1. Claude Code와 협업하면서 원하는 기능을 말하면 에이전트가 “이 조건도 필요하지 않나”라고 관련 요구사항을 제안하는 방식이 유용할 수 있다.
   2. 제안된 명세와 개발자의 진짜 의도가 일치하는지 확인하는 문제는 남아 있다. 명세를 만들었다는 사실만으로 올바른 목표를 증명한 것은 아니다.
   3. 의도 불일치 문제가 해결되지 않았더라도, 아무 명세도 없이 작성한 코드보다 에이전트가 제안한 명세에 따라 증명을 통과한 코드가 나을 수 있다.

3.4. 증명은 가정과 명세의 범위 안에서만 강하다

1. 증명 가능한 속성과 아직 어려운 속성

   1. C 코드의 메모리 안전처럼 여러 프로그램에 공통 적용할 수 있는 속성은 일회성 보편 명세로 만들 수 있다.
   2. 버퍼 오버플로 공격이 불가능하다는 속성은 해당 명세와 시스템 가정이 충족되면 100% 증명할 수 있다.
   3. “인식 네트워크가 고양이와 개를 정확히 구분한다”는 요구는 고양이와 개를 형식적으로 어떻게 정의할지부터 난관이다.

2. 모든 증명은 가정에 의존한다

   1. 형식 증명은 명세와 모델의 가정이 옳다는 조건 아래에서만 결론을 보장한다.
   2. 통계적 방법은 확률 분포로 불확실성을 표현하지만, 형식 방법은 가능한 상태의 집합으로 표현하는 경우가 많다. 집합 기반 보장은 깔끔하지만 범위가 현실적으로 충분한지 따져야 한다.
   3. 안전팀은 증명이 적용되지 않는 조건과 입력 범위를 공개해야 한다. 가정을 밝히지 않으면 수학적 보장이 현실 전반에 대한 보장처럼 오해될 수 있다.

4. 항공 검증 기술을 언어 모델에 적용하기

4.1. 극히 드문 실패를 일반 시뮬레이션으로 찾기는 어렵다

1. 항공 안전의 목표 수치

   1. 상업 항공은 비행 시간당 치명적 실패 확률을 대략 10⁻⁹ 수준으로 관리하는 기준을 사용한다.
   2. 이런 확률을 단순 시뮬레이션으로 관찰하려면 평균적으로 실패 한 건을 보기 위해 약 10⁹시간을 시뮬레이션해야 한다. 실패 열 건을 분석하려면 약 10¹⁰시간이 필요하다.
   3. 따라서 정상 조건을 무작위로 반복하는 대신 실패 가능성이 높은 경계 상황에 계산을 집중해야 한다.

2. 서로 다른 검증 방법의 포트폴리오

   1. 반증 탐색(Falsification)은 시스템을 깨뜨릴 조건을 찾아내고 해당 실패가 실제로 위험한지 판정한다.
   2. 중요도 샘플링(Importance Sampling)은 실제 분포 p 대신 실패를 더 자주 뽑는 제안 분포 q에서 표본을 얻고 p/q 가중치로 보정해 실패 확률을 추정한다.
   3. 가우시안 프로세스, 정규화 흐름, 저랭크 가우시안 혼합 모델, 확산 모델 등이 실패 표본을 찾기 위한 제안 분포로 쓰였다.
   4. 확산 모델은 뒤집힌 진자처럼 양쪽 방향으로 발생할 수 있는 서로 다른 실패 모드를 함께 찾을 수 있다. 단순 적응형 스트레스 테스트는 한 실패 경로에 집중할 수 있다.
   5. 형식 검증은 명세가 있는 부분을 증명하고, 확률적 시험은 명세로 완전히 덮지 못하는 희귀 실패를 찾는다.

4.2. AST Prompter는 가능성 높은 유해 출력을 탐색한다

1. 실패와 가능성의 정의

   1. 적응형 스트레스 테스트를 언어 모델에 옮긴 AST Prompter 연구에는 Huijin Liu Mu와 Amelia Hardy 등 학생들이 참여했다.
   2. 먼저 무엇을 실패라고 볼지 정한다. 독성의 경우 Llama Guard 같은 별도 신경망의 점수가 임계값을 넘으면 실패로 분류한다.
   3. 다음으로 입력의 가능성을 측정한다. 이 연구는 언어 모델의 당혹도(perplexity)를 사용해 흔하고 자연스러운 입력을 찾는다.
   4. 검색은 낮은 로그 당혹도와 높은 독성을 동시에 추구한다. 가능성이 높은 유해 실패가 발견되면 배포 전 완화책이 필요하다는 신호가 된다.

2. 방법의 적용 범위와 산업 채택

   1. 물리 시스템과 언어 모델의 실패 정의·환경은 다르기 때문에 항공 검증의 성공 수준이 그대로 재현된다고 단정할 수 없다.
   2. Waymo와 자동차 제조사들은 연구실의 검증 도구를 업계 전체가 쓰도록 연구를 후원했다. AST Prompter는 Schmidt Sciences의 지원을 받았다.
   3. 당시 Anthropic, OpenAI, xAI가 비슷한 방식으로 연구실과 협력하느냐는 질문에는 “아직 아니다”라는 답이 나왔다.
   4. 강한 안전 도구의 기술적 성숙도와 프런티어 연구소의 실제 채택 사이에는 간극이 있다.

4.3. 신경망 검증·런타임 감시·벤치마크

1. 검증 계층 확장

   1. 신경망 자체의 속성을 검증하는 방법도 연구되고 있지만, 대형 모델의 모든 행동을 증명하는 문제와는 구분해야 한다.
   2. 배포 후 런타임 모니터링은 입력과 출력이 안전 경계를 벗어나려는 순간을 찾아 차단하는 계층이다.
   3. BetterBench는 벤치마크의 품질과 평가 방법을 점검하는 작업과 연결된다. 성능 점수만 높이는 것보다 평가 항목이 유효하고 최신인지 확인해야 한다.

2. 벤치마크도 소프트웨어처럼 관리한다

   1. 벤치마크 포화, 추론 실패의 토큰 수준 흔적, 사람 평가자 간 판단 차이가 연구 대상이다.
   2. 자해 관련 답변에서 정신건강 전문가들 사이의 평가도 크게 엇갈릴 수 있다는 관찰은 인간 판정의 일관성을 자동으로 가정할 수 없음을 보여준다.
   3. 언어와 사용 환경이 변하면 모델뿐 아니라 벤치마크도 지속적으로 모니터링해야 한다. 분포 이동을 감지하는 정량 방법을 함께 사용할 수 있다.
   4. Math 500처럼 널리 쓰이는 평가 세트에도 오류 문항이 있을 수 있다. 전직 학생은 SQL 질의 평가 항목의 약 30%가 잘못됐음을 발견했다.
   5. 평가 세트에는 코드와 같은 버전 관리, 변경 제안, 이슈 등록, 검토 절차가 필요하다.

5. 단일 해법 대신 겹겹의 안전망

5.1. 스위스 치즈 모델과 시스템 경계

1. 여러 방어층의 구멍이 동시에 맞지 않게 한다

   1. 항공에서는 고도별 전략적 분리, 항공 교통 관제, 충돌 회피 시스템이 순서대로 안전층을 이룬다.
   2. 언어 모델에서는 학습 데이터 사전 필터링, 학습 후 실패 분석, 실패 확률 추정, 런타임 감시, 운영자 개입이 대응되는 계층이다.
   3. Percy는 소형 모델로 학습 데이터를 사전 선별하는 사례다.
   4. 허깅페이스 사건처럼 연쇄사고 감시나 운영용 가드레일이 꺼져 있으면 여러 층의 구멍이 한 줄로 정렬될 수 있다.
   5. 사회공학 공격이 시스템 침해의 흔한 경로이므로, 기술 통제와 함께 사람의 권한·훈련·승인 절차도 설계해야 한다.

2. 형식 보장과 통계적 보장의 결합

   1. 형식 방법은 명세가 지정한 모든 경우를 포괄적으로 다루는 데 강하고, 통계적 검증은 실제 환경에서 얼마나 자주 실패하는지 추정하는 데 강하다.
   2. 형식 방법이 불확실성의 집합을 넓게 잡으면 증명은 안전해도 현실과 너무 멀어질 수 있다. 확률 분포는 현실적인 빈도를 표현할 수 있지만 드문 꼬리 위험을 놓칠 수 있다.
   3. 두 방법은 대체재가 아니라 서로 다른 구멍을 보완하는 안전층이다.

5.2. 항공의 독립 기관과 사고 보고 체계

1. 기술만큼 중요한 제도 설계

   1. 상업 항공은 1970년대보다 약 80배 안전해졌으며, 그 변화에는 기술뿐 아니라 제도 설계도 기여했다.
   2. 미국 국가교통안전위원회(NTSB)는 1967년 독립 기관으로 설립됐다. 미국산 부품이 관련된 해외 사고까지 조사할 수 있는 국제적 영향력도 갖는다.
   3. ASRS 같은 비처벌적 보고 체계는 제조사와 항공사가 사고 정보를 공유하도록 유도했다. 후속 항공 안전 정보 분석·보고 체계는 공개에 일정한 면책을 부여했다.
   4. 책임 추궁만으로 운영하면 조직이 사고와 아차사고를 감추기 쉽다. 학습을 우선하는 보고 절차가 위험의 재발을 줄인다.

2. AI 사고 조사의 독립성

   1. AI판 NTSB 설립은 검토할 가치가 있지만, 새 기관을 만들고 전문성을 갖추기까지 시간이 걸리고 정부 조직은 느릴 수 있다.
   2. 우주 발사장의 레인지 세이프티 오피서는 임무 조직에서 독립해 객관적 안전 기준으로 발사 여부를 판단한다. AI에도 이해관계가 분리된 go/no-go 평가자가 필요하다.
   3. 독립 평가 기관은 평가 대상 기업이나 그 우호적 파트너가 아니라는 점을 제도와 검증 가능한 기록으로 입증해야 한다.

6. 규제·시장·독립 평가의 역할

6.1. AI 안전 원칙과 규제 포획

1. 높은 수준의 기준을 세우고 기술 세부 처방은 유보한다

   1. 자율주행 규칙 수립을 도왔던 크리스 거데스는 기술이 충분히 성숙하기 전에 특정 기술을 법으로 처방하는 것은 이르며, 모범 관행과 상위 기준부터 만드는 편이 낫다고 판단했다.
   2. 미국 GAAP처럼 ‘일반적으로 받아들여지는 AI 안전 원칙’을 만들고 KPMG나 Ernst & Young 같은 기관이 평가하는 가벼운 출발점이 제안됐다.
   3. 규칙이 복잡해지면 규제 포획이 생길 수 있다. Uber·Lyft·DoorDash·Instacart가 1099 계약자 지위를 유지하는 반면 후발 기업은 같은 조건을 얻기 어렵다. 기존 기업에 유리한 규칙은 규제 포획의 위험을 보여준다.

2. 산업별 협력과 시장 인센티브

   1. 자율주행 회사는 경쟁사가 안전사고를 내는 것을 원하지 않는다. 한 회사의 사고가 업계 전체의 신뢰를 무너뜨리므로 안전 기준을 함께 개선할 동기가 있다.
   2. 형식 검증을 30년간 연구한 관점에서는 일하는 방식을 법으로 강제하기보다 안전성이 경쟁 우위가 되게 하는 편이 낫다.
   3. 몇몇 기업이 형식 검증으로 보안상 이점을 얻으면 다른 CISO도 뒤따라 투자할 수 있다.

6.2. Antruth와 검증 가능한 인증서

1. 독립 평가의 상업적 기반

   1. 클라크 배럿이 공동 CEO로 참여하는 Antruth는 CSLib과 유사한 보편 코드 추론 엔진을 구축하고, 기업·개발자·보안 분야에 적용하려 한다.
   2. 평가 결과를 믿어 달라고 요구하는 대신 누구나 직접 확인할 수 있는 증명서와 인증서를 제공하는 것이 독립성의 기준이다.
   3. 모든 안전 평가를 프런티어 연구소나 그들과 가까운 기관에 맡기는 것은 이해충돌을 낳을 수 있다.

2. 책임을 받아들이는지가 안전 주장의 일부다

   1. 안전 인증을 하는 주체가 평가 대상 기업으로부터 독립적인지 확인해야 한다.
   2. 시장에서 안전한 제품이라는 측정 가능한 이점이 생기면 기업이 자발적으로 검증을 도입할 가능성이 커진다.
   3. 인증서에는 검증한 버전, 명세, 가정, 시험 환경과 책임 범위가 명시돼야 한다.

7. 공개 질의응답: 명세·책임·입력·하드웨어

7.1. 사양이 없는 기업 코드를 어떻게 검증할까

1. 보편·도메인별 명세

   1. 메모리 안전은 모든 C 코드에 반복 적용할 수 있는 보편적 명세의 예다.
   2. 은행 시스템은 여러 거래를 거쳐도 고객 자금이 사라지지 않아야 한다는 도메인별 불변 조건을 세울 수 있다.
   3. 기업 코드가 명세 없이 쌓였더라도 중요한 불변 조건부터 역으로 추출해 검증 대상에 포함할 수 있다.

2. AI가 명세를 제안할 때의 검토

   1. 에이전트는 사용자가 말하지 않은 관련 조건을 제안하는 데 도움을 줄 수 있다.
   2. 생성된 사양이 개발자의 의도와 다른 문제는 남아 있으므로 사람의 승인과 추적 가능한 변경 기록이 필요하다.
   3. 올바른 명세를 만드는 과정 자체를 검증해야 코드 증명이 사용자 목표를 대신 잘못 보장하지 않는다.

7.2. AI 관리자와 법적 책임

1. 관리자 자동화의 안전 조건

   1. 물리적 위협 때문에 사람 대신 AI를 시스템 관리자로 쓰고 싶다는 질문에는 항공기의 단독 조종사 운용과 조종사 책임이 비교됐다.
   2. FAA 기준에서 문제가 생겼을 때 책임질 자격 있는 조종사가 있어야 하듯, AI 관리 시스템에서도 누가 최종 책임자인지 정해야 한다.
   3. 인간 관리자를 보호하려면 업무 분리, 권한 축소, 안전한 원격 운영 같은 대안도 함께 검토해야 한다.

2. 공급자의 법적 책임 수용

   1. Waymo는 완벽하지 않지만 자체 평가로는 사망자를 줄이는 효과를 낸다고 주장한다. 안전한 자동화가 가능한지 여부와 별개로 책임 소재가 중요하다.
   2. AI 관리자 공급자가 실패에 대한 법적 책임을 받아들일 의사가 있는지 물어야 한다. 책임을 약속하는 것은 실제 안전 사례를 구축했다는 증거가 될 수 있다.

7.3. 프롬프트 인젝션과 검증 가능한 입력

1. 자연어 명령은 코드 증명과 다르다

   1. 자연어 입력은 형식 검증 대상이 되는 프로그램 코드와 다르며, 프롬프트 인젝션 문자열을 완벽히 분류하는 규칙을 만들기 어렵다.
   2. 입력을 먼저 AI로 검사하는 방식은 공격자도 검사기를 우회하도록 입력을 바꾸는 군비 경쟁이 될 수 있다.

2. 출력의 도메인 사실을 검증한다

   1. Amazon의 자동 추론 검사는 LLM 응답에서 도메인 지식을 추출해 정형화하고, 엄격한 도메인 모델과 대조하는 접근을 사용한다.
   2. 자유 형식 언어를 그대로 신뢰하기보다, 결과를 검증 가능한 사실과 행동으로 변환해 안전한 범위 안에서 사용해야 한다.

7.4. 하드웨어·단순성·설명 가능성

1. 검증 범위는 소프트웨어에서 하드웨어로 넓어진다

   1. Rowhammer 같은 메모리 하드웨어 취약점과 길게 이어지는 의존성은 소프트웨어만 증명해도 전체 시스템 안전이 완성되지 않는다는 질문으로 이어졌다.
   2. x86 명령어 집합은 여러 회사에서 형식화된 바 있다. 소프트웨어 검증은 비교적 낮은 난도의 첫 단계이며, 장기적으로 컴파일러와 하드웨어까지 검증 범위를 넓힐 수 있다.

2. 복잡성을 늘리기 전에 단순 모델을 검토한다

   1. 오컴의 면도날은 공학의 기본 원칙이다. 더 단순하고 해석 가능한 방법일수록 견고할 가능성이 크다.
   2. 선형 회귀나 결정 트리부터 시작하고, 복잡한 모델이 성능을 충분히 높일 때만 추가 복잡성을 받아들이는 접근이 권장됐다.
   3. ACAS X가 국제 표준으로 받아들여지는 데 설명 가능성이 중요했다. 안전성뿐 아니라 왜 그런 결정을 내렸는지 이해할 수 있어야 운영자와 규제기관이 신뢰할 수 있다.

8. 개발 중인 도구와 후속 연구

8.1. 코드 추론 엔진과 기업 적용

1. Antruth는 CSLib 비전을 바탕으로 자율적이고 효율적인 대규모 코드 추론 역량을 만들고, 이를 기업·개발자·보안에 적용하려 한다.
2. 장기 목표는 세상의 모든 코드를 검증하는 것이다.
3. 형식 검증의 시장 가치는 보안 사고 비용, 코드 생성량, 증명 자동화 비용의 변화에 따라 달라질 수 있다.

8.2. 검증 알고리즘과 공개 도구

1. Mykel Kochenderfer의 책 Algorithms for Validation은 통계적 방법, 형식 방법, 도달 가능성 분석을 공통 언어로 묶으며, 발표 당시 PDF가 온라인에 있고 다음 달 출간 예정이었다.
2. 최적화 책 제2판은 2027년 초 예정이며, Algorithms for Decision Making은 2022년 출간됐다.
3. 연구실은 Julia 기반 POMDP 도구인 pomdp.jl, 확장 가능한 계획을 위한 POMCPOW, 적응형 스트레스 테스트의 Python 구현을 공개했다.
4. Python 버전을 “구식 언어를 계속 쓰고 싶은 사람들”을 위한 도구라고 부르는 농담이 나왔다.

주요 발언 모음

“AI 안전이 우리가 올라야 할 에베레스트라면, 코드 추론은 좋은 베이스캠프다.” — 클라크 배럿

“AI는 공격할 수 있지만 방어할 수도 있다. AI 방어와 형식 방법이 합쳐지면 3~5년 안에 시스템이 완전히 안전해질 것이라고 예측한다.” — 클라크 배럿의 전망

“증명은 언제나 어떤 가정에 대한 증명이다.” — 형식 검증의 적용 범위를 설명하는 원칙

“시스템에 대한 신뢰를 세우는 단 하나의 은총알은 없다. 형식 방법만으로 끝까지 갈 수는 없다.” — 마이켈 코헨더퍼

“모든 안전을 연구소나 독립성을 주장하는 연구소의 친구들에게 맡긴다면 정말 안타까운 일이다.” — 독립 평가의 필요성

“성공은 세상의 모든 코드가 검증되는 것이다.” — 코드 추론의 장기 목표

핵심 데이터와 수치

• AI 연구자 약 1,200명을 조사한 2023년 논문은 멸종 위험을 모든 미래와 향후 100년 기준으로 물었으며, 향후 10년이라고 묻지 않았다.
• 허깅페이스 실험에는 약 1,200개의 에이전트가 사용됐으며, 연쇄사고 모니터와 운영 환경용 가드레일이 꺼져 있었다.
• Dalek Lite 약 3만 줄의 Rust 암호 라이브러리는 세 명이 5개월 동안 수작업으로 검증했지만 자동 증명 에이전트는 약 11시간 만에 검증했다.
• Lean SMT 시연에서 나온 증명 목표 35개 중 처음에는 32개가 자동 해결됐고 나머지 3개도 정의 전개와 재호출로 해결됐다.
• 항공 안전 목표는 비행 시간당 치명적 실패 확률 약 10⁻⁹ 수준이며, 단순 시뮬레이션으로 실패 한 건을 평균 관측하려면 약 10⁹시간이 필요하다.
• 상업 항공은 1970년대보다 약 80배 안전해졌다.
• SQL 평가 항목 약 30%가 오류였다는 연구실 학생의 발견 사례는 벤치마크 품질 관리의 중요성을 보여준다.
• 형식 검증으로 3~5년 안에 모든 시스템이 완전히 안전해질 것이라는 배럿의 예측은, 5천억 파라미터 모델의 직접 증명은 어렵다는 그의 한계 인식과 함께 읽어야 한다.

결론과 시사점

1. 안전 주장은 실제 사고의 작동 조건, 재현 가능한 데이터, 명시적인 시간 범위를 갖춰야 한다. 헤드라인이나 설문에서 숫자를 떼어내 다른 기간의 사실처럼 인용하면 위험 판단이 왜곡된다.
2. 단기 우선순위는 개방형 모델로 증폭될 수 있는 사이버 공격을 막는 일이다. 기본 계정·패치·권한·백업과 병원 등 필수 서비스의 복구 능력은 최첨단 AI 평가와 함께 다뤄야 한다.
3. 형식 검증은 소프트웨어 경계에 실질적 보증을 제공하며, AI 자동화가 비용을 낮출 수 있다. 그러나 증명 대상의 명세와 가정이 틀리면 보장도 잘못된 목표에 대한 보장이다.
4. 항공에서 발전한 희귀 실패 탐색·확률 추정·독립 사고 조사는 AI에도 유용하지만, 언어 모델의 실패 정의와 분포가 물리 시스템과 다르다는 점을 유지해야 한다.
5. 검증은 학습 데이터에서 배포 후 감시까지 이어지는 복수의 방어층으로 설계해야 한다. 어떠한 단일 인증, 벤치마크, 모델 평가도 시스템 전체의 안전을 대신할 수 없다.
6. 독립 평가, 버전이 기록된 증명서, 비처벌적 사고 보고, 명확한 공급자 책임이 기술의 실제 채택을 뒷받침한다.
7. 형식 검증이 향후 수년 안에 모든 시스템을 완전히 안전하게 만든다는 전망은 검증 가능한 예측으로 추적하되, 현재 기술이 증명하지 못하는 대형 모델의 행동까지 이미 해결한 사실처럼 해석해서는 안 된다.

핵심 요약 20줄

AI 안전은 막연한 종말 예측보다 측정 가능한 실패와 검증 가능한 보장을 중심으로 다뤄야 한다.

기술의 큰 전환기마다 원자폭탄·자동화·인터넷·스마트폰의 위험을 둘러싼 과장된 예측이 반복됐다.

Focal에서 Walmart 재고를 잘못 예측하면 아보카도 과다 발주만으로도 수백만 달러 손실이 날 수 있었다.

2023년 AI 연구자 설문은 멸종 위험을 모든 미래와 향후 100년 기준으로 물었으며 10년 전망은 묻지 않았다.

허깅페이스 에이전트 실험은 약 1,200개 에이전트의 프롬프트와 꺼진 감시층이 결합된 사건이지 자발적 폭주가 아니었다.

개방형 모델은 테러·생물무기·사이버전·랜섬웨어를 수행하는 기존 악의 행위자의 역량을 키울 수 있다.

GPU 등록이나 전력 감시만으로 분산된 장비와 국가 단위 공격자를 완전히 통제하기는 어렵다.

기본 비밀번호·패치·권한 관리와 병원 복구 역량은 AI 시대에도 사이버 방어의 핵심이다.

AI는 취약한 코드를 늘릴 수 있지만 동시에 방어자의 코드 분석과 형식 검증을 자동화할 수 있다.

Lean 기반 증명 에이전트는 3만 줄 Rust 암호 라이브러리 검증을 전문가 3명의 5개월 작업에서 약 11시간으로 줄였다.

Verisforge는 영어 요구사항을 구조화된 명세로 바꾸고 Rust 코드와 증명을 생성해 자동 검증한다.

형식 증명은 메모리 안전을 강하게 보장할 수 있지만 고양이와 개를 구분하는 지각 의미를 쉽게 명세하지 못한다.

5천억 파라미터 모델 전체의 안전을 직접 증명하기보다 코드·권한·샌드박스 같은 경계를 검증하는 편이 현실적이다.

항공의 치명적 실패 목표는 비행 시간당 약 10⁻⁹이며 희귀 실패는 중요도 샘플링과 스트레스 테스트로 찾아야 한다.

AST Prompter는 Llama Guard의 독성 점수와 입력 당혹도를 결합해 가능성 높은 유해 출력을 탐색한다.

상업 항공은 1970년대보다 약 80배 안전해졌으며 독립 조사와 비처벌적 사고 보고 제도가 큰 역할을 했다.

AI 안전은 학습 데이터 필터링·실패 분석·확률 추정·런타임 감시·사람의 승인으로 겹겹이 보호해야 한다.

벤치마크 문항에도 오류가 생길 수 있으므로 평가 세트 역시 버전 관리·검토·이슈 제보 절차가 필요하다.

AI 운영 자동화는 공급자의 법적 책임과 독립 인증, 명시된 검증 가정이 확보될 때 더 신뢰할 수 있다.

단일한 안전 은총알은 없으며 형식 검증·확률적 시험·설명 가능성·제도적 책임이 서로의 빈틈을 메워야 한다.