요약
Claude가 오픈소스 라이브러리 123개의 컴파일된 코드가 메모리 오류로 죽지 않음을 증명했습니다.
앤트로픽 프런티어 레드팀이 정형 검증 회사 시어럼과 함께 낸 연구입니다. AI가 버그를 찾아 공격에 엮는 능력이 커지는 만큼, 테스트로는 얻을 수 없는 보장을 정형 검증(프로그램이 명세를 지킨다는 것을 수학으로 증명하는 방법)으로 얻자는 취지입니다.
왜 중요한가
- seL4 커널 검증에 약 20인년이 들던 일을 몇 주 만에 라이브러리 123개 규모로 해냈습니다.
- 증명은 Rocq 검사기가 확인하므로 사람이 수십만 줄짜리 증명을 직접 검토하지 않아도 됩니다.
- 저자들은 검증이 퍼징처럼 개발 과정에 기본으로 들어가는 절차가 될 것으로 봤습니다.
핵심 내용
- OSS-Fuzz의 퍼즈 테스트(무작위 입력으로 오류를 찾는 시험)를 명세로 바꿔, 64MB 미만 모든 입력에서 죽지 않음을 증명했습니다.
- 증명 대상은 소스가 아니라 RISC-V 바이너리이며, 증명은 모두 합쳐 약 1억 8천만 줄입니다.
- 그 과정에서 수년간 숨어 있던 버그 수백 개를 찾았고, Claude가 직접 고친 뒤 다시 증명했습니다.
- 증명 하나에 토큰이 수억 개씩 드는 비용이 걸림돌이지만, Opus 5.5는 Opus 5보다 토큰을 약 40% 덜 썼습니다.
- 정적 musl 바이너리를 가정해 흔히 쓰는 glibc 환경과 다르므로, 검증이 곧 무결함은 아니라고 밝혔습니다.
HN 반응
- 한 이용자가 Rust로 다시 쓴 Postgres를 C 원본과 같게 동작한다고 Lean으로 증명 중이라고 하자, 변환기 검증과 명세 자격을 묻는 반문이 이어졌습니다.
- 개발자 일자리를 잃을까 두렵다는 글에는 일자리는 늘 것이라는 답과 좋은 일자리일지는 모른다는 반론이 맞섰습니다.
회의적이신 분들께 말씀드리면, 저는 Postgres를 Rust로 다시 쓰는 작업에서 형식 검증으로 꽤 괜찮은 성과를 봤습니다. Rust와 C 코드를 둘 다 Lean으로 번역하는 컴파일러를 직접 만들었습니다. 두 함수가 Lean으로 넘어오면, LLM에게 두 함수가 똑같이 동작한다는 Lean 증명을 쓰게 합니다.
지금까지 전체 코드의 약 12%가 단일 스레드로 실행할 때 똑같이 동작한다는 것을 증명했습니다. C 코드로 따지면 약 7만 줄입니다. 이 과정에서 아주 사소한 동작 차이를 찾아냈는데, 예를 들면 플랫폼마다 부동소수점 연산 결과가 다르게 나올 수 있다는 점 같은 것입니다.
규모를 더 키울 방법을 찾고 있는 중인데, 더 키우는 데 근본적인 걸림돌이 있어 보이지는 않습니다.
모든 검증에는 명세가 필요한데, 이 경우 명세는 Postgres 구현 자체입니다. 260만 줄짜리 C 코드를 명세로 삼는 것보다는 훨씬 나은 방법이 있고, 또 있어야 한다고 생각합니다.
일반적으로 명세는 사람이 읽을 수 있어야 하고, 그러려면 SQL을 버려야 한다고 봅니다. 수천 쪽에 달하는 SQL 표준은 차치하더라도, 핵심 부분집합조차 null 같은 문제 때문에 의미론이 꼬여 있습니다.
Prela 1가 나온 주된 동기 중 하나가 더 단순한 의미론인데, 단순한데도 실제로 쓰이는 수천 개의 쿼리를 표현할 수 있고 2 심지어 둠(doom)까지 돌릴 수 있다는 것이 확인됐습니다 3.
버그까지 똑같이 맞춰야 하는 호환성이 필요할 때는 코드 자체가 최고의 명세인 경우도 있습니다.
보통은 저도 동의하지만, 코드를 이식할 때는 소스 코드가 곧 명세입니다.
> In general, the spec must be human readable, and I believe to achieve that we must do away with SQL
(> 일반적으로 명세는 사람이 읽을 수 있어야 하고, 그러려면 SQL을 버려야 한다고 봅니다)
음, Carthago delenda est(카르타고는 멸망해야 한다)인가요? 대체 왜요?
맞아요, 원래 글에서 제일 비현실적인 부분이죠.
아니, SQL은 제가 태어나기 전부터 있었고, 기계 신이 강림하지 않는 한(그래도 살아남을 것 같지만) 제가 죽고 한참 뒤에도 계속 있을 텐데요. 문명이 무너지지 않는다면 말이죠.
SQL은 문법이 풍기는 인상보다 훨씬 지적으로 일관성이 있습니다. 잘 쓰인 간결한 공개 명세가 있는 SPARQL이나, 명세는 딱히 없지만 CTE를 그렇게 어설프게 만들어 놓지 않은 Datalog에 끌리기 쉽고, 트리거 같은 기능을 보면 속이 울렁거리기도 하죠. 하지만 SQL이 그렇게까지 나쁘지는 않습니다. Postgres 같은 방언은 JSON도 꽤 잘 지원하고요.
SPARQL은 멋지지만 꽤 제한적이에요. 예를 들어 BFS나 DFS 같은 흔한 그래프 연산은 SPARQL로 구현할 수 없는데, SQL은 물론 할 수 있죠(딱히 권하고 싶지는 않지만요). 이걸 알았을 때 꽤 당황했어요. 그러니까 SQL이 SPARQL보다 표현력이 엄밀히 더 높다는 얘기가 되거든요!
시맨틱 웹에는 SPARQL 2.0이 절실하지만, 그런 건 나오지 않을 겁니다. 표준화 과정에서 커뮤니티가 지쳐 나가떨어졌다는 이유가 가장 크죠. 저는 문서 데이터베이스에서 흔히 쓰는, 순서가 있는 컬렉션을 표현하는 기능에 관심이 많습니다. 시맨틱 웹에서 제 작업의 결실이 (주로) OWL로 ISO 20022 금융 메시지 표준 같은 복잡한 문서 스키마를 표현하는 방법을 알아낸 것이었거든요. 그리고 거기서는 순서가 중요합니다!
(> Rust와 C 코드를 둘 다 Lean으로 번역하는 컴파일러를 직접 만들었습니다)
그 컴파일러가 올바른지는 어떻게 검증하나요? 그러려면 적어도 Lean으로 쓴 C와 Rust 양쪽의 형식 의미론이 필요할 텐데, 둘 다 헤라클레스급 대공사처럼 들리네요.
(> 그 컴파일러가 올바른지는 어떻게 검증하나요?)
아직 안 했습니다. 제 주된 목표는 최대한 많은 버그를 찾는 것이었습니다. 컴파일러가 틀려서 버그가 빠져나갈 가능성은 여전히 있지만, 꽤 많은 버그가 계속 나오고 있으니 해볼 만한 가치가 있다고 생각합니다.
Aeneas 같은 검증된 Rust 검증 도구 체인을 쓰는 건 고려해 보셨나요?
수정: 평소에 이런 말은 잘 안 하는데, 제 질문이 왜 비추천을 받고 있죠? 이런 질문은 하면 안 되는 건가요?
Rust 검증 도구 체인으로는 부모 댓글 작성자의 코드가 C 코드와 똑같이 동작하는지 알 수 없습니다.
제가 알기로는 Aeneas는 Rust의 안전한 부분집합만 지원합니다. 저는 Rust 전체를 지원하는 것이 필요했습니다.
https://github.com/AeneasVerif/aeneas 에는 이렇게 적혀 있습니다.
"Aeneas currently functionalizes a subset of safe Rust, and we are in the process of extending the functional model with reasoning based on separation logic to support unsafe code and concurrent code."
("Aeneas는 현재 안전한 Rust의 일부분을 함수형으로 변환하며, 안전하지 않은 코드와 동시성 코드를 지원하도록 분리 논리 기반 추론으로 함수형 모델을 확장하는 중입니다.")
(> 적어도 C의 형식 의미론이 필요할 텐데)
https://en.wikipedia.org/wiki/CompCert
(> Lean으로 쓴 C와 Rust 양쪽의 형식 의미론, 둘 다 헤라클레스급 대공사처럼 들리네요)
고대 아테네식으로 가자면, 플라톤의 메텍시스(참여)가 아마 더 어울리겠네요.
Rust|C 양쪽을 다루는 그 Lean 컴파일러는 rustc나 clang을 포크한 건가요, 아니면 다른 방식인가요? 12%면 꽤 희망적인 수치네요. 저는 정적 분석으로 핵심 동작을 싸고 현실적으로 증명할 수 있는 세상이 오길 아직도 기대하고 있습니다. LLM과 프로그래밍 언어 이론(PLT)이 만나는 영역은 아직 덜 탐구된 것 같다는 느낌이 듭니다.
그나저나 pgrust는 정말 대단합니다.
감사합니다!
C와 Rust를 둘 다 지원하려고 여러 방법을 시도했습니다. LLVM 바이트코드를 써 봤는데, 너무 저수준이라 증명이 거대해졌습니다.
CBMC의 중간 표현인 "GOTO Programs"를 Lean으로 변환하는 것도 시도했습니다. CBMC는 C를 지원하고 Kani가 Rust 지원을 더해 주니 해볼 만하다고 생각했죠. 하지만 Kani의 Rust-GOTO 변환이 코드 크기를 엄청나게 부풀리는 바람에 접어야 했습니다.
결국 GOTO Programs와 MIR(Rust의 IR)을 둘 다 제가 직접 만든 IR로 변환하는 방식으로 정했습니다. 이 IR은 두 언어를 모두 변환할 만큼 저수준이면서도, 코드를 비교적 간결하게 유지할 만큼 고수준입니다. 그다음 IR에 단순화 패스를 돌리고 Lean으로 컴파일합니다.
https://news.ycombinator.com/item?id=50205816 에서는 다른 의견인 것 같은데요.
저는 서른다섯인데, 저들 뜻대로 되면 저는 끝장입니다. 저는 트레이드 쪽으로는 안 갈 겁니다. 프로그래밍이 너무 좋아서 스물일곱에 건설업을 그만뒀거든요. 건설업에서 일할 때는 거의 매일 죽고 싶었습니다. 너무 괴로워서 이십 대를 술로 날려 보냈고요. 지금은 몇 년째 술을 끊었는데, 전적으로 프로그래밍 덕분입니다. 제가 하는 일을 진짜로 좋아하게 됐으니까요. 그런데 이 회사는 여러 방식으로 그걸 저에게서 빼앗고 있습니다.
저는 이 전환에 제 인생의 많은 부분과 전 재산을 쏟아부었습니다. 그런데 지금은 매일같이 전기 기사나 되라는 소리를 듣고 있습니다. 앤트로픽이 어떻게든 정지 문제(halting problem)를 풀겠다고 주장하기 때문이죠. 사실 주장한 걸 실제로 해낼 필요도 없습니다. 업계의 20%만 설득하면 됩니다. 그러면 저 같은 사람들은 은퇴할 때까지 일할 기회조차 얻지 못할 겁니다.
그들이 성공하리라고는 정말 생각하지 않습니다. 하지만 만약 성공한다면, 저는 공공 도서관에서 코딩하는 노숙자가 될 겁니다. 다시 처음부터 시작하지는 않을 거니까요.
이 일로 전체적으로는 일자리가 더 많이 생길 거라고 생각하는 사람이 많습니다. 저도 어느 정도는 동의합니다. 다만 우리의 일상 업무가 너무 많이 바뀌었습니다. 풀면서 보람을 느끼던 문제들은 이제 LLM에게 넘어갔지만, 동시에 제가 만들고 싶은 것은 더 쉽고 빠르게 만들 수 있게 됐습니다. 분명 얻는 것과 잃는 것이 있습니다. 저는 긍정적으로 지내려고 노력하고 있습니다.
(> 이 일로 전체적으로는 일자리가 더 많이 생길 거라고 생각하는 사람이 많습니다.)
"일자리"와 "좋은 일자리"(먹고살 수 있고 심지어 잘살 수 있는 수준)를 꼭 구분하세요. 쥐꼬리만 한 급여를 주는 일자리야 소가 돌아올 때까지도 계속 만들어 낼 수 있으니까요.
저는 (전체적으로) 중위 임금의 두 배를 주는 일자리가 많이 생길 거라고 봅니다.
그중 일부가 2021년에는 중위 임금의 3~5배를 줬을 일자리였다는 사실이 AI에 대한 통렬한 고발이 되지는 않습니다. 중위 임금의 4배를 벌 수 있었는데 이제 2배만 버는 일부 사람들에게는 불편한 일이겠지만요.
네, LLM이 일자리를 전체적으로 늘릴지 없앨지를 두고 업계에서는 의견이 엇갈립니다. 겉보기에 가장 미덕이라 할 만한 점은 개발자가 소프트웨어를 더 빨리 만들 수 있게 된다는 것입니다.
저는 제 일상의 할 일을 관리하고 실생활의 삶의 질을 높여 주는 도구를 몇 개 만들었는데, 제가 만든 것 중 상당수는 그와 비슷한 걸 더 빨리 더 많이 만들려고 만든 것들이에요... 그러면 스스로 묻게 되죠. 대체 뭘 위해서? ㅋㅋ
맞아요, 저도 AI로 짧은 클립 편집을 자동화하는 앱을 만들었는데, 직접 코딩했다면 한참 걸렸을 거예요. 좋긴 한데, 이런 걸 해 주는 도구가 있는데 소프트웨어 회사가 왜 굳이 나를 뽑고 계속 쓰겠느냐는 의문이 들기도 하죠.
LLM 시대에 '개발자'를 정의해 보세요.
누구에게 묻느냐에 따라 다를 것 같아요. 프롬프트를 쓸 수 있으면 만들 수 있으니까요, 그렇죠? 제가 보기에 개발자는 AI를 활용해서, 시스템 설계나 아키텍처 구상, 버그 찾기 같은 일을 직접 할 때보다 더 효율적으로, 심지어 전문 개발자보다 훨씬 빠르게 해내는 사람이에요.
저도 이 LLM 열풍이 마냥 반갑지는 않습니다. 하지만 프로그래밍 일자리가 전부 사라지는 건 여전히 상상하기 어렵습니다. 그동안 아무리 발전했다고 해도, 비개발자가 제 일을 하는 모습은 정말 상상이 안 됩니다.
opus 5.5가 빌어먹을 천재 같고 코드를 굳이 확인할 필요도 못 느낄 정도인데도, PM이 제 업무 대부분을 넘겨받는 건 상상조차 안 돼요. 어림도 없습니다.