Anthropic's Claude now writes code and proves it safe automatically↗ (원문, 새 창)

앤트로픽이 파트너사 티어럼(Theorem)과 함께 클로드를 활용해 기존 소프트웨어 코드의 정확성을 수학적으로 증명하는 형식 검증(formal verification)을 수행했다. 구글 OSS-Fuzz 보안 프로젝트의 123개 오픈소스 라이브러리를 대상으로 몇 주 만에 약 1억8000만 줄의 증명 코드를 생성했으며, 이 과정에서 기존 테스트로는 발견하지 못한 버그 수백 개를 찾아내고 직접 수정했다. 널리 쓰이는 PDF 리더 검증에서는 단 1주일 만에 해당 소프트웨어의 연간 평균 보고 건수만큼의 보안 버그를 발견했고, 10년 넘게 발견되지 않았던 논리적 오류도 잡아냈다. 다만 증명은 특정 프로세서 아키텍처, 단일 스레드 프로그램, 64MB 이하 입력이라는 엄격한 조건에서만 유효하며, 개별 증명에는 수억 개의 토큰이 소요될 정도로 연산 비용이 크다.

• 123개 오픈소스 라이브러리를 대상으로 몇 주 만에 약 1억8000만 줄의 수학적 증명 코드 생성
• 증명 과정에서 기존 테스트가 놓친 버그 수뿝 개 발견, 클로드가 직접 수정까지 수행
• PDF 리더 검증에서 1주일 만에 해당 소프트웨어의 연간 평균 버그 보고 건수만큼 발견, 10년 넘은 논리적 오류도 포착
• 증명은 특정 프로세서·단일 스레드·64MB 이하 입력이라는 엄격한 조건에서만 유효, 개별 증명에 수억 토큰 소요
• 오퍼스 5.5는 오퍼스 5보다 약 40% 적은 토큰으로 증명의 절반을 해결, 글리브씨·오픈SSL 등 핵심 인프라로 확장 계획