구글에서 선호하는 출처로 추가
앤트로픽, 오픈소스 123개 검증…239개 진입점 오류 조건 증명
서지우 기자
앤트로픽은 클로드를 활용해 오픈소스 라이브러리 123개의 테스트 진입점 239개에서 정해진 조건의 안전성을 증명했다고 밝혔다. 검증은 특정 실행 환경과 입력 범위에 한정된다.
토포AI로 이 기사 더 깊이 읽기
앤트로픽(Anthropic)이 클로드를 활용해 오픈소스 라이브러리 123개의 테스트 진입점 239개에서 정해진 조건의 안전성을 수학적으로 증명했다.
앤트로픽 프런티어 레드팀은 22일 공개한 연구에서 검증 기업 Theorem과 함께 작업했다고 밝혔다. 연구진은 기존 테스트를 검증 조건으로 바꾸고 클로드가 작성한 증명을 별도 도구로 검사했다.
검증 대상은 구글의 오픈소스 오류 탐지 프로젝트 ‘OSS-Fuzz’에 포함된 라이브러리다. 연구진은 기존 퍼즈 테스트를 ‘64MB 미만의 어떤 입력값에서도 프로그램이 비정상 종료하거나 메모리 안전성 오류 또는 검증 조건 실패를 일으키지 않는다’는 명제로 바꿨다. 클로드가 증명을 작성하고 Rocq가 이를 확인했다.
연구진은 수주 동안 클로드가 발견한 오류를 수정한 뒤 123개 라이브러리의 테스트 진입점 239개를 검증했다고 설명했다. 진입점은 프로그램의 특정 기능을 시험하기 위해 마련한 입력 경로다. 증명은 사람이 읽는 원본 코드가 아니라 컴파일된 RISC-V 명령어를 대상으로 했으며, 작성된 Rocq 증명은 약 1억8000만 줄이다.
형식 검증은 프로그램이 명시된 규칙을 지키는지 수학적으로 확인하는 방법이다. 입력값을 실행해 오류를 찾는 기존 테스트와 달리, 정한 조건에 해당하는 모든 입력값을 대상으로 명제를 증명한다. 증명을 작성하는 과정에서 기존 테스트로 발견하지 못한 오류도 나왔고, 연구진은 해당 오류를 수정한 코드에 맞춰 검증 조건을 다시 만들었다.
이번 결과는 고정된 메모리 용량을 사용하며 리눅스에서 실행되는 단일 스레드·정적 연결 RISC-V 프로그램에 한정된다. 각 라이브러리의 모든 기능이나 실제 배포 환경 전반을 검증한 것은 아니다. 앤트로픽은 증명 도구가 명제의 성립 여부는 확인하지만, 그 명제가 현실의 사용 조건을 빠짐없이 담았는지는 판단할 수 없다고 설명했다.
연구진은 별도 실험에서 클로드가 리눅스 커널의 zlib 구현을 x86 실행 파일 수준에서 검증했다고 밝혔다. 또 Rust로 작성한 파이썬 해석기를 170만개가 넘는 무작위 생성 프로그램으로 시험한 결과, CPython과 동작이 일치한 비율은 99.95%였다고 발표했다. 두 실험은 이번 123개 라이브러리의 RISC-V 검증과 대상과 방법이 다르다.
앤트로픽은 소규모 검증 과제 36개를 비교한 결과도 공개했다. 클로드 오퍼스 5.5는 과제 절반을 증명하는 데 오퍼스 5보다 약 40% 적은 토큰을 사용했다. 연구진은 증명의 일부를 공개해 다른 개발자가 확인하고 재사용할 수 있도록 했다.
Comment 0
불러오는 중…