핵심 요점
- Anthropic과 파트너사 Theorem은 Claude를 사용하여 기존 소프트웨어 코드를 수학적으로 검증하고 그 정확성에 대한 형식 증명을 생성했습니다.
- 이 모델은 단 몇 주 만에 123개의 오픈소스 라이브러리에 대해 약 180 million 줄의 증명 코드를 생성했습니다. 그 과정에서 Claude는 기존 테스트에서 놓쳤던 수백 개의 버그를 발견했습니다.
- AI가 코드를 작성하고 그 코드가 올바름을 증명할 수 있다면, 소프트웨어 자동화는 큰 도약을 이룰 수 있습니다. Anthropic은 AI를 활용한 형식 검증이 표준 테스트만큼 일상적인 것이 되기를 원합니다.
Anthropic가 Claude를 사용해 기존 코드가 올바르다는 것을 수학적으로 증명했습니다. 이 접근 방식은 AI 생성 소프트웨어의 핵심 문제를 다루지만, 엄격한 실용적 한계가 따릅니다.
모든 상황에서 소프트웨어가 오류 없이 작동함을 증명하는 일은 항상 비용이 너무 많이 들었다. 전문가 팀이 필요했다. 20인년(20 person-years) 작은 운영체제 커널인 seL4를 정식으로 검증하기 위해서였고, 따라서 이 방법은 다음과 같은 극단적인 사례에만 사용되었다 에어버스 항공전자 소프트웨어.
Anthropic의 프론티어 레드 팀“, 파트너와 협력하여” 정리, 대신 Claude에게 증명 작업을 맡겼습니다. 이 모델은 단 몇 주 만에 Google의 123개 오픈소스 라이브러리의 테스트 프로그램을 활용해 약 180백만 줄의 수학적 증명 코드를 생성했습니다. OSS-Fuzz 보안 프로젝트.
Claude는 새로운 코드를 작성하는 대신, 크래시 테스트를 수학적 문제로 변환하고 컴파일된 기계 코드를 분석하며 방대한 증명을 생성함으로써 기존 소프트웨어를 검증했습니다. Rocq라는 독립적인 검증 프로그램이 이러한 증명을 자동으로 검사하며, Anthropic에 따르면 이 과정에는 사람의 검토가 거의 필요하지 않습니다. 연구진은 이를 "완전 자율적인" 증명 생성이라고 부르지만, 그 도구와 형식적 기반은 Theorem.Ad의 사람들이 구축한 것입니다.
Claude는 수년간의 테스트에서 발견되지 않았던 버그를 잡아냅니다
증명을 생성하는 동안 Claude는 수백 개의 버그를 만났고 그 버그들을 직접 수정할 수 있었습니다. 연구진에 따르면, 그중 많은 버그들이 매우 특수한 조건, 이를테면 비정상적으로 큰 입력 파일이나 특정 접근 순서에서만 나타나기 때문에 기존의 테스트에서는 간과되었을 것이라고 합니다.
예를 들어 널리 사용되는 PDF 리더를 검증하는 과정에서 팀은 단 일주일 동안 해당 소프트웨어에 대해 통상 1년 전체에 걸쳐 보고되는 것과 맞먹는 수만큼의 보안 버그를 발견했습니다. 또 다른 적용 사례에서 Claude는 10년 넘게 감지되지 않았던 논리적 오류를 잡아냈습니다. Anthropic에 따르면, 완전한 증명이 결국 실패하더라도 그 시도 자체가 실제 버그를 드러냅니다.
형식 검증이 할 수 있는 것과 할 수 없는 것
Anthropic은 "형식적으로 검증됐다"는 것이 "오류가 없다"는 의미는 아니라고 인정합니다. 이 증명은 특정 프로세서 아키텍처, 단일 스레드 프로그램, 64 MB 미만의 입력이라는 엄격한 조건에서만 성립합니다. 실제로는 이러한 라이브러리들이 서로 다른 하드웨어와 서로 다른 구성으로 실행됩니다.
컴퓨팅 비용은 상당한 수준으로, 개별 증명 하나가 수억 개의 토큰을 소모합니다. Anthropic은 프로젝트 총비용을 밝히지 않았습니다. 하지만 AI가 자신의 코드를 검증할 수 있다면 개발자들은 AI가 생성한 소프트웨어를 더 신뢰하고 검토에 드는 시간을 줄일 수 있습니다. 이는 검증뿐 아니라 전체 코딩 과정에서 비용을 절감합니다. 소규모 테스트 실행 결과 증명은 재사용 가능하며, 더 새로운 모델들은 효율성이 높아지고 있습니다: Opus 5.5는 Opus 5에 비해 약 40퍼센트 적은 토큰으로 절반의 증명을 해결했습니다.
이 프로젝트는 소프트웨어 자동화에 대한 근거를 강화합니다. AI가 코드를 작성하고 정의된 조건 하에서 그 정확성을 보장할 수 있다면, 질문은 "AI가 프로그래밍할 수 있는가?"에서 "AI가 자신이 작성한 코드가 안전하다는 것을 증명할 수 있는가?"로 바뀝니다. 그 답이 '예'라면, 그 결과는 오늘날의 코딩 도구를 훨씬 넘어설 수 있습니다.
대표적인 사례로, Anthropic은 AI를 활용한 형식 검증이 곧 표준 테스팅만큼 실용적으로 될 것으로 예상하고 있으며 Theorem의 로드맵은 이미 glibc, OpenSSL, cURL 같은 핵심 인프라를 목표로 하고 있습니다.
출처: Anthropic