AI 에이전트가 CPython을 Lean으로 옮겨 61만 줄 증명 작성, 파이썬 버그 418건 적발
- Opus 5.5가 CPython 3.15.2 함수를 한 줄씩 Lean으로 옮겨 613,318줄과 정리·보조정리 18,898개를 만들었고, 매 빌드마다 Lean 검사기가 전체를 확인함. 검토까지 통과한 함수는 4,071개로 CPython 전체의 16%임.
- 증명 작업 중 418건의 버그 보고가 나왔고, 그중 약 55건은 평범한 파이썬 코드만으로 인터프리터를 크래시시키거나 메모리를 손상시킬 수 있는 것임.
- 함수마다 복사, 테스트, 증명, 검토 4단계를 거치며 테스트는 최소 5만 개 입력으로 실제 파이썬과 결과를 비교하고, 작성에 참여하지 않은 두 번째 에이전트가 '깨진 버전도 통과할 수 있는 증명인가'를 따져 검토 통과분만 인정함.
- 첫 시도는 함수마다 증명을 하나씩 붙이는 넓이 위주였는데 검토 결과 절반 미만이 유효했고 한 파일은 21%만 남았음. '반환하면 0 이상'처럼 참이지만 고장 난 구현도 통과하는 명제가 원인이었음.
- 부분별 진행률은 문법 규칙 100%, 내장 타입 35%, 파서 31%, C 모듈 19%, 인터프리터 코어 10%, 표준 라이브러리 9%임.
Hacker News opinions
Julia 표준 라이브러리에도 똑같은 방식으로 적용한 사례가 있더라. 이 글 프롬프트에도 julia-in-lean 언급이 들어 있다고 함.
이 버그 헌팅 방식 진짜 유망한데 문제는 상시화임. 사람이랑 에이전트 작업이 많이 들어가서 테스트 스위트에 그냥 못 넣어. 결국 언어 차원에서 코드와 Lean 증명이 따로 놀지 않게 opt-in 속성으로 넣고 테스트 때만 검사하는 쪽으로 가야 할 듯. 컴파일러 검사랑 비슷한데 더 표현력 있고 더 비싼 셈이지.
그럴 바엔 그냥 Lean으로 짜면 되지 않나. 두 언어 문제도 같이 해결되고.
418건밖에? 나는 1만 건쯤 나올 줄 알았는데. 참고로 전문 파이썬 프로그래머임.
아직 전체 커버리지가 아니라서 그런 거임.
번역 단계를 없애거나 그냥 파싱으로 대체할 방법은 없나?
원리적으로는 가능함. dict나 int 같은 파이썬 원시 타입이 이미 Lean에 정의돼 있으니, 파이썬 코드에 증명을 주석으로 달면 자동으로 Lean으로 바꿀 수 있을 거임.
AI가 쓴 글을 인용한다고? 난 사양함.
AI가 쓴 글 읽는 사람이 있긴 한가. 진지하게 묻는 거임.
Lean 코드가 C를 한 줄씩 베낀 건데 어떻게 버그인지 의도된 동작인지 구분하나? 증명이 성립하려면 이상한 가정이 필요하고 그 가정이 곧 버그 트리거 조건임. 모든 수가 2^32 미만이라는 공리가 필요하다면 그 위 입력에서 뭐가 터지는지 보면 됨.
Frama-C로 ACSL 주석 다는 게 토큰을 더 잘 쓰는 방법 아닌가. 실제 런타임을 검증하고 수정도 업스트림에 바로 넣을 수 있는데.
몇 가지 헷갈림. 한 줄씩 옮겼는데 어떻게 두 구현 결과가 달라지나? 그리고 3단계의 '항상 참이어야 하는 것'은 LLM이 찍는 건가?
찍는다고 볼 수 있는데 소스 우선순위가 있음. C와 파이썬 쌍, 빠른 경로와 느린 경로, 왕복 변환처럼 구현이 자기 자신과 어긋나는 지점, 크래시 없음 같은 자명한 불변식, 문서 문장 순으로 씀.
두 구현이 다르면 Lean 번역이 틀린 거라 그런 건 증명에 못 씀. 근데 흥미로운 명제를 어떻게 골랐는지는 글에 자세히 없음. 이 접근의 핵심인데 말이지.