2026-11-05 · 출처：Unite AI p4
Theorem과 함께 진행된 Anthropic의 10월 22일 연구는 AI가 발견한 버그가 또 하나의 테스트 통과가 아니라 '수정됐다'는 수학적 증명과 함께 나가는 워크플로를 가리킨다.
239개의 퍼징 테스트 진입점, 각각이 이제 기계 검증된 형식 증명으로 뒷받침된다. 2026년 10월 22일 Anthropic이 발표한 연구의 헤드라인 주장이다. Claude가 123개 오픈소스 라이브러리에서 뽑은 코드에 대해 보안 속성의 증명을 만들어낸 작업을 기술한다.
이 작업은 Theorem과의 협업이며 범위가 특이하다. 증명은 RISC-V 어셈블리 코드 수준, 즉 메모리 안전성 버그가 실제로 사는 계층에서 작동한다. Anthropic에 따르면 Claude는 결함을 찾는 데서 멈추지 않았다. 모델은 발견한 버그를 패치한 뒤, 64 MB 미만의 모든 입력과 모델링된 모든 리눅스 조건에서 수리된 프로그램이 언제나 정상적으로 종료한다는 증명을 만들어냈다. 메모리 안전성 오류나 어서션 실패를 단 한 번도 일으키지 않는다는 증명이다.
중요성이 자리하는 곳은 테스트와 증명의 구분이다. 퍼징 테스트는 프로그램에 수많은 입력을 넣어 우연히 발견한 것을 보고한다. 시도해 보지 않은 입력에서 프로그램이 무엇을 하는지는 절대 말할 수 없다. 반면 기계 검증된 증명은 형식 명세에 대비해 기계적으로 검증되며, 명세가 기술하는 입력 공간 전체를 커버한다. 여기서는 64 MB 상한 미만의 모든 입력과 모델링된 리눅스 환경이다. 주장이 명시된 그대로 성립한다면, 239개 진입점 각각은 어떤 양의 무작위 테스트도 공급할 수 없는 더 강한 보장을 갖는다.
어셈블리 수준에서 작업하면 기준은 한층 더 올라간다. 소스 코드에 대한 추론은 컴파일 과정에서 유입되는 결함을 놓칠 수 있다. RISC-V 어셈블리에서 속성을 증명한다는 것은 보장이 프로세서가 실제로 실행할 명령어에 붙는다는 뜻이다.
관련된 123개 라이브러리의 메인테이너들에게, 발표된 결과는 하나의 폐쇄 루프를 그린다. 발견, 패치, 검증된 증명이 단일 워크플로 안에서 이어지는 루프다. 그 루프가 평범한 소프트웨어 유지보수의 속도와 비용으로 돌아갈 수 있는지가 Anthropic의 수치가 열어둔 질문이자, 기계 검증 보안 증명이 특별한 일이 아니라 일상이 되는지를 결정할 질문이다.
태그: Anthropic · Claude · Theorem · Formal Verification · Memory Safety · RISC-V
萬安算交所 AIXX · AIXX · 검증된 컴퓨트 거래소 · 현물 홀 입장