Claude가 오픈소스 123개 라이브러리의 어셈블리 코드 보안 속성을 형식 증명함

appendix 보니까 에이전트 증명이 레지스터 값이랑 주소 구분까지 다 풀어서 쓰더라. 사람 증명 엔지니어라면 바로 추상화로 뽑았을 거임. 프로그램이 커지면 이 장황한 스타일이 벽이 될 듯함.

증명 쓰는 건 결국 니치 언어로 코드 짜는 거임. 모듈화 잘하도록 학습시키면 일반 프로그래밍 실력도 같이 올라갈 것 같음. Creusot나 Flux 같은 Rust 검증 도구도 자연스럽게 쓰게 될 듯.

수학자들이 LLM은 인간 수학의 convex hull 바깥으로 못 나간다고 하던데, 내 느낌엔 LLM은 보간은 잘하고 외삽은 못함. 내 아이디어 증명은 잘 만들어도 새로운 발상은 내가 설명해줘야 나오더라.

그 결론엔 동의 안 함. 어려운 문제로 강화학습 돌리면 에이전트가 증명 전략을 알아서 바꿀 수도 있음.

수학은 분포 밖 일반화가 병목이라 한계가 뚜렷한데, 소프트웨어 검증은 병목이 규모라서 convex hull 얘기가 있어도 기존 소프트웨어 대부분은 검증할 수 있을 듯함.

Anthropic이 이런 말 하는 게 좀 이상함. 내 Claude는 시키지 않으면 형식 검증 안 하고 상태를 그냥 가정해버림. 스크립트로 검증하면 금방일 텐데.

그래서 unit test도 사람이 쓰면 별로고 AI가 쓰면 더 별로임. 자기가 짠 코드를 자기가 테스트하니까 당연히 통과함.

형식 검증하려면 모델이 실제 코드랑 맞아야 하는 거 아님? 엉뚱한 걸 증명했을 수도 있지 않나.

언어 모델 있으면 소스 수준 증명은 가능하고, 명령어셋까지 모델링하면 바이너리에 직접 증명도 됨. 그럼 남는 가정은 하드웨어가 모델대로 돈다는 것뿐임.

맞음. 소스를 Lean으로 옮긴 표현이 실제 코드랑 눈에 띄게든 미묘하게든 어긋날 수 있음.