Anthropic, Claude로 기존 코드의 정확성을 수학적으로 증명하는 작업 공개

검증 대상은 Google의 OSS-Fuzz에 포함된 123개 오픈소스 라이브러리의 테스트 프로그램이다. Claude는 새 코드를 작성하지 않고, 퍼즈 테스트(크래시 테스트)를 수학적 문제로 변환한 뒤 컴파일된 기계어를 분석해 증명을 만들었다. 증명의 정당성은 독립된 검증 프로그램 Rocq가 자동으로 확인하며, 사람 검토자는 거의 필요하지 않다고 한다. 연구자들은 이를 완전 자율적 증명 생성이라고 부르지만, 도구와 형식적 기반은 Theorem의 사람들이 구축한 것이다.

배경으로, 소프트웨어 형식 검증은 종래 매우 비용이 많이 들었다. 소형 OS 커널 seL4의 검증만 해도 전문가 팀이 20인년이 걸렸고, Airbus의 항공전자 소프트웨어 같은 극단적인 사례에 한정되었다.

증명 작성 과정에서 Claude는 수백 건의 버그를 마주했고 스스로 수정했다. 대용량 입력 파일이나 특정 접근 순서처럼 제한된 조건에서만 나타나기 때문에 일반 테스트에서는 놓치기 쉽다고 연구자들은 설명했다. 널리 쓰이는 PDF 리더의 검증에서는 1주일 만에 보통 1년치에 해당하는 수의 보안 버그가 발견되었다. 10년 넘게 알려지지 않았던 논리 오류도 검출되었다. 증명이 최종적으로 실패하더라도 시도 자체가 실제 버그를 드러낸다고 한다.

한계도 명시되어 있다. 형식 검증을 마쳤다는 것이 오류가 없다는 뜻은 아니며, 증명은 특정 프로세서 아키텍처, 단일 스레드, 64MB 미만 입력이라는 조건에서만 성립한다. 개별 증명에는 수억 토큰이 필요하며 총비용은 공개되지 않았다. 소규모 시험에서는 증명을 재사용할 수 있다는 것이 확인되었고, Opus 5.5는 Opus 5보다 약 40% 적은 토큰으로 증명의 절반을 풀었다. Anthropic은 AI에 의한 형식 검증이 머지않아 일반 테스트와 같은 수준으로 실용화될 것으로 보고 있으며, Theorem은 glibc, OpenSSL, cURL 등 핵심 인프라도 대상으로 삼고 있다.