Anthropic: Claude는 대규모 형식 검증 오픈 소스 라이브러리입니다
인공지능 회사 Anthropic의 Frontier Red Team은 10월 22일 연구를 발표하며 대형 언어 모델이 더 큰 규모에서 자동으로 형식 증명을 작성할 수 있다고 밝혔습니다. 팀은 Theorem과 협력하여 Claude를 사용해 RISC-V 어셈블리 레벨에서 100개 이상의 실제 오픈 소스 라이브러리에 대한 안전 속성을 증명했으며, 이는 AI를 사용하여 어셈블리 레벨에서 생산 소프트웨어에 대해 대규모 형식 검증을 수행한 것으로 알려진 최초의 사례라고 합니다. 증명 작성 과정에서 수년간 발견되지 않았던 취약점도 발견되었습니다.실험은 Google OSS-Fuzz에 이미 존재하는 컴파일 가능한 퍼즈 테스트를 사양으로 변환했습니다: 단일 스레드 정적 바이너리, 고정 메모리 예산, RISC-V CPU 및 Linux 등의 가정 하에, 64MB 미만의 임의 입력에 대해 프로그램은 정상적으로 종료되어야 하며 메모리 안전 오류나 단언 실패를 유발하지 않아야 합니다. 몇 주 내에 Claude는 발견된 문제를 수정한 후 123개의 OSS-Fuzz 라이브러리 중 239개의 진입점에 대해 위의 속성을 증명했습니다. 증명은 컴파일된 RISC-V 명령어를 대상으로 하며, 약 1.8억 줄의 Rocq로 이루어져 있으며 Rocq 커널에 의해 검증됩니다. 페이지는 이것이 이러한 라이브러리에 취약점이 없다는 것을 의미하지 않으며, 남은 문제는 신뢰할 수 있는 구성 요소나 증명 범위 밖에 있을 수 있다고 언급했습니다.페이지는 또한 팀이 Claude에게 RFC 1950을 형식화하도록 하였고, x86 바이너리 레벨에서 Linux 커널의 zlib 구현이 해당 사양을 준수함을 증명했다고 밝혔습니다; Rust로 작성된 Python의 대규모 하위 집합을 커버하는 인터프리터는 170만 개 이상의 무작위 생성 프로그램과 CPython 행동이 일치하는 비율이 99.95%였습니다. 36개의 소규모 검증 작업에서 Opus 5.5는 필요한 토큰의 절반이 Opus 5보다 약 40% 적다고 증명했습니다. 팀은 또한 증명이 단일 스레드, 정적 링크된 RISC-V 바이너리를 대상으로 하며, 증명 검증기가 사양이 현실에 부합하는지 판단할 수 없다고 지적했습니다.
