Anthropic이 소프트웨어 버그를 '수학적으로' 근절하겠다고 나섰다 — Project Glasswing의 야심과 현실

소프트웨어 버그는 불편함을 넘어 목숨을 앗아가기도 합니다. 항공기 제어 시스템, 의료기기 펌웨어, 원전 관제 소프트웨어에서 발생하는 결함은 곧 재앙으로 이어집니다. Anthropic이 이 문제에 AI를 들이밀겠다고 선언했습니다. 이름은 Project Glasswing. “크리티컬 소프트웨어에서 버그를 수학적으로 제거하겠다"는 목표를 내걸었는데요. 과연 이게 가능한 일일까요?

형식 검증이란 무엇인가

일반적인 소프트웨어 테스트는 “이런 입력을 넣으면 이런 결과가 나오는지” 확인하는 방식입니다. 문제는 가능한 입력의 조합이 사실상 무한하다는 점입니다. 테스트는 버그의 존재를 증명할 수 있지만, 버그의 부재를 증명할 수는 없습니다.

형식 검증(Formal Verification)은 접근법이 근본적으로 다릅니다. 코드가 특정 명세를 반드시 만족한다는 것을 수학적 증명으로 보장합니다. “모든 경우에 이 코드는 올바르게 동작한다"를 논리적으로 증명하는 것이죠. 항공우주 분야에서는 이미 DO-178C 같은 인증 표준에서 형식 검증 기법을 권장하고 있고, 마이크로프로세서 설계에서도 Intel이 Pentium FDIV 버그 사건 이후로 형식 검증을 적극 도입하고 있습니다.

그런데 왜 모든 소프트웨어에 형식 검증을 적용하지 않을까요? 답은 간단합니다. 엄청나게 어렵고, 엄청나게 비싸기 때문입니다.

Project Glasswing이 풀려는 문제

형식 검증의 가장 큰 병목은 인간 전문가의 작업량입니다. 수학적 증명을 작성하려면 Coq, Isabelle, Lean 같은 증명 보조 도구를 다루는 고도로 전문화된 인력이 필요합니다. 업계에서 자주 인용되는 수치가 있습니다. 검증된 코드 한 줄을 만드는 데 드는 비용이 일반 코드의 10~30배에 달한다는 것입니다. 실제로 호주에서 완전히 형식 검증된 마이크로커널 seL4의 경우, 약 8,700줄의 C 코드를 검증하는 데 연인원 수십 명이 수년을 투입했습니다.

Anthropic의 Project Glasswing은 바로 이 병목을 AI로 돌파하겠다는 구상입니다. 핵심 아이디어는 세 가지로 요약됩니다.

첫째, AI가 코드를 분석해 형식 명세(specification)를 자동으로 생성합니다. 둘째, 그 명세에 대한 수학적 증명을 AI가 탐색하고 작성합니다. 셋째, 인간 전문가는 AI가 생성한 증명을 검토하고 최종 승인하는 역할로 전환됩니다.

왜 Anthropic인가

AI 기업이 형식 검증에 뛰어드는 것이 의외로 보일 수 있지만, Anthropic의 맥락에서는 상당히 자연스러운 행보입니다.

Anthropic은 설립 초기부터 AI 안전(AI Safety)을 핵심 정체성으로 내세워 왔습니다. Constitutional AI, RLHF 개선, 모델 평가 프레임워크 등 안전 관련 연구에 지속적으로 투자해 왔죠. Project Glasswing은 이 안전 철학의 연장선입니다. AI 모델 자체의 안전성을 넘어, AI가 탑재되는 크리티컬 시스템 전반의 신뢰성을 높이겠다는 것입니다.

또한 대규모 언어 모델이 수학적 추론에서 점점 더 강해지고 있다는 점도 배경이 됩니다. Lean 4 같은 증명 보조 도구에서 AI가 증명 단계를 제안하는 연구는 이미 활발히 진행되어 왔습니다. DeepMind의 AlphaProof가 국제수학올림피아드 문제를 형식적으로 증명하는 데 성공한 사례도 있었고요. Anthropic은 이런 흐름을 크리티컬 소프트웨어라는 실전 영역으로 가져오려는 것입니다.

현실과의 거리 — 넘어야 할 산들

비전은 매력적이지만, 현실의 장벽은 만만치 않습니다.

명세 자체가 어렵습니다. 코드를 증명하려면 먼저 “이 코드가 무엇을 해야 하는가"를 수학적으로 정의해야 합니다. 하지만 실제 소프트웨어의 요구사항은 모호하고, 암묵적이며, 종종 모순됩니다. AI가 코드에서 명세를 추출할 수 있다 해도, 그 명세가 진짜 의도를 반영하는지 판단하는 것은 여전히 인간의 몫입니다.

스케일 문제가 있습니다. seL4처럼 작고 잘 정의된 커널과 달리, 실제 산업용 소프트웨어는 수백만 줄 규모입니다. 레거시 코드, 서드파티 라이브러리, 하드웨어 의존적인 부분까지 포함하면 검증 범위를 어디까지 잡을지부터 난제입니다.

AI가 생성한 증명의 신뢰성 문제도 있습니다. 형식 검증의 장점은 증명이 기계적으로 검사 가능하다는 것이므로, AI가 만든 증명이 올바른지는 검증할 수 있습니다. 그러나 AI가 증명을 찾지 못한 경우 — 이것이 버그의 존재를 의미하는지, 단순히 AI의 능력 한계인지 구분하기 어렵습니다.

그래도 방향은 맞다

비관적으로 들릴 수 있지만, 중요한 것은 방향입니다.

현재 크리티컬 소프트웨어의 품질 보증은 대부분 방대한 테스트 수트와 코드 리뷰에 의존하고 있습니다. NASA의 경우 코드 1,000줄당 약 0.1개의 결함률을 목표로 하지만, 이것도 완전한 무결함과는 거리가 있습니다. 형식 검증이 아무리 부분적으로 적용되더라도, 기존 접근법으로는 잡지 못하는 결함 범주를 줄일 수 있다면 그것만으로도 의미가 큽니다.

특히 AI가 형식 검증의 진입 장벽을 크게 낮춰서 더 많은 조직이 크리티컬 코드에 부분적으로나마 형식 검증을 적용할 수 있게 된다면, 소프트웨어 산업 전체의 안전 수준이 한 단계 올라갈 수 있습니다.

Anthropic의 Project Glasswing이 당장 모든 버그를 근절할 수 있을까요? 솔직히 어렵습니다. 하지만 “AI로 형식 검증을 민주화한다"는 방향 설정 자체는 이 업계에서 오랫동안 꿈꿔왔던 것이기도 합니다. 중요한 건 이 프로젝트가 실제로 어떤 규모의 소프트웨어에서, 어떤 수준의 검증을 달성하느냐일 텐데요. 여러분은 AI가 만든 수학적 증명을 믿고 비행기에 탈 수 있으신가요?