LLM이 훨씬 더 큰 규모의 소프트웨어 정형 검증을 가능하게 하고 있음

Anthropic과 Theorem은 Claude로 오픈소스 라이브러리 123개의 퍼징 진입점 239개를 정형 검증함. 발견한 버그를 수정한 뒤, 특정 실행 환경과 입력 크기 조건에서 컴파일된 코드가 충돌하지 않음을 증명함 기존 퍼즈 테스트를 명세로 변환하고 RISC-V 바이너리 수준에서 증명하는 방식임. Claude가 작성한 증명은 Rocq가 검사하므로, 방대한 증명 코드를 사람이 모두 검토할 필요는 없음 증명을 시도하는 과정에서 수백 개의 버그를 발견함. 큰 입력이나 드문 호출 순서가 필요한 메모리 오류뿐 아니라, 충돌을 일으키지 않는 논리 오류도 찾아냄 정형 검증이 버그 부재를 뜻하지는 않음. 보장은 명세와 머신 모델의 정확성에 의존하며, 이번 검증은 단일 스레드 정적 RISC-V 바이너리와 64MB 미만 입력 등으로 범위가 제한됨 증명 생성에는 막대한 토큰이 들지만, 모델 개선과 증명 재사용으로 비용을 줄일 수 있었음. 소규모 평가에서 Opus 5.5는 Opus 5보다 약 40% 적은 토큰으로 과제 절반을 증명했고, 공유 작업 공간은 토큰 사용량을 17% 줄임 정형 검증의 비용 장벽과 이번 실험 충분히 테스트된 소프트웨어에도 버그가 남아 있으며, AI는 이를 찾고 사소해 보이는 버그들을 심각한 공격으로 연결하는 능력을 높이고 있음 수십억 대 기기에서 실행되는 Linux 커널에서도 최근 1,000개가 넘는 취약점이 공개됨 정형 검증(formal verification) 은 코드를 수학적 모델로 옮기고, 정의된 보안 규칙을 항상 지키는지 증명하는 방식임 증명 실패는 규칙을 위반할 수 있는 버그의 단서가 될 수 있음 실패 원인을 제거하고 증명을 반복하면, 해당 규칙을 위반하는 버그가 없다는 보장을 얻을 수 있음 기존에는 전문 인력과 시간이 많이 필요해 적용 범위가 제한됐음 seL4 커널 구현에는 2인년이 들었지만 정형 검증에는 20인년이 필요했음 Airbus 항공전자 코드처럼 안전이 특히 중요한 분야에서 주로 실용성을 확보했음 Anthropic과 Theorem의 실험은 프로덕션 소프트웨어의 어셈블리 수준 정형 검증에 AI를 대규모로 적용함 연구진이 아는 한 이런 규모의 시도는 처음임 모든 버그를 제거한 것은 아니지만, 실제 코드에 유용한 보안 속성을 자율적으로 증명할 수 있음을 보여줌 기존 테스트를 증명 가능한 명세로 바꾸기 정확성을 증명하려면 먼저 명세로 정확성의 의미를 정의해야 함 PNG 디코더는 RFC 2...