Anthropic·Theorem, 오픈소스 퍼즈 테스트 대상의 AI 작성 증명 보고

Anthropic은 10월 22일 Theorem과의 연구를 공개하며 Claude가 오픈소스 라이브러리 123개의 퍼즈 테스트 진입점 239개에 대해 정형 보안 증명을 생성했다고 보고했다. 이 작업은 기존 테스트를 컴파일된 프로그램에 관한 수학적 명제로 바꾼 뒤 독립된 증명 검사기로 생성된 논증을 검증한다. 그 과정에서 모델은 명제의 성립을 방해하는 버그도 발견하고 수정했다.

보장은 정의된 실행 환경 안에서 적용된다. musl과 링크된 정적 단일 스레드 RISC-V 바이너리를 고정 메모리 예산이 있는 Linux 프로세스 모델에서 실행하는 조건이다. 기술 부록은 입력을 64 MiB 미만으로 정하고, Theorem의 드라이버 문서도 그 크기 이상의 파일을 거부한다고 명시한다. 어떤 운영체제 응답과 메모리 배치, 자원 조건을 포괄하는지도 정리의 전제가 결정한다.

처리 과정은 라이브러리의 기존 퍼즈 테스트 하네스를 사용한다. 하네스의 단언문은 압축과 해제의 성공 같은 속성을 표현할 수 있다. 일반 바이너리와 새니타이저 검사를 포함한 버전을 비교하고 관찰 가능한 동작을 추론한다. 부록은 오류, 중단, 프로세스 모델에 정의되지 않은 동작을 충돌에 포함한다. Claude는 Rocq에서 논증을 구성하고, Rocq 커널은 요구된 명제를 입증하는지 검사한다.

신뢰해야 하는 경계는 정형화된 기계 및 프로세스 모델, 정확한 정리 명제, 검사기 자체와 각 바이너리를 검사하는 데 필요한 보조 도구 및 환경에 집중된다. 선택한 진입점에서 도달하는 코드와 바이너리에 존재하는 검사가 적용 범위를 정한다. 결과를 실제 운영 소프트웨어에 적용할 때에는 검사 밖에 있는 속성, 모델과 배포된 하드웨어 또는 운영체제 사이의 차이가 여전히 중요하다.

코드 수정을 허용하면서 별도의 과제도 생겼다. 에이전트가 의미 있는 프로그램 동작을 제거해 충돌하지 않는다는 명제를 쉽게 증명할 수 있기 때문이다. Anthropic에 따르면 실험에서는 모든 패치에 감점을 적용하고, 변경이 어떤 입력에 영향을 주며 그 집합이 얼마나 작은지 증명하면 추가 점수를 줬다. 연구진은 이런 편법을 찾기 위해 패치를 기록하고 감사했다. 수정 후에는 명세를 다시 생성하고 모델이 수정된 프로그램의 명제를 증명하도록 했다.

공개 자료는 연구 결과의 일부다. 확인 당시 Theorem의 증명 저장소에는 25개 라이브러리의 60개 진입점이 나열됐으며 증명은 Rocq 9.2.0으로 검사했다. 저장소는 컴파일된 바이너리를 고정하고 관련 명제와 가정을 기록한다. 공개 버전에는 동작을 비교하고 지정된 오류를 배제하는 일치성 증명이 담겼다. 이 증명들은 실행이 영원히 끝나지 않는 경우도 허용할 수 있다. 종료 보장은 별도의 정리가 필요하다.

Anthropic 부록의 전문가 논의는 생성된 증명이 인간 전문가가 보통 작성하는 것보다 훨씬 장황하다고 설명한다. 에이전트는 레지스터 내용, 메모리 주소, 실행 분기를 반복해서 상세히 기술하면서도 일부 익숙한 추상화를 만들어냈다. 분석은 더 복잡한 프로그램으로 확장하기 위한 모듈 구조 개선을 미해결 문제로 다룬다. 증명의 수학적 유효성과 증명을 만들어내는 효율 및 구성 방식은 구별한다.

Theorem은 자격을 갖춘 오픈소스 프로젝트에 OSS Verify 과정을 무료로 제공하고 있다. 유지보수, 사용 범위, 라이선스, 프로젝트가 보안 경계나 다른 소프트웨어의 기반에 있는지 등을 고려해 자격을 개별 심사한다. 널리 사용되는 기반 소프트웨어를 우선하며 발견한 버그는 유지관리자에게 비공개로 보고한다. 문서는 증명 생성에 수일이 걸릴 수 있고 완료 후에도 갱신할 수 있다고 설명하며, 각 결과를 특정 프로그램 빌드와 연결한다.