AI가 CPython을 Lean으로 재작성해 418개의 버그를 찾아냈다
Formalizing CPython
AI 에이전트가 CPython의 내부를 한 줄씩 Lean으로 옮겨 61만 3,318줄의 코드와 1만 8,898개의 정리를 만들었다. 각 복사본은 실제 Python과 수만 개의 입력으로 대조 테스트를 거치고, 작성하지 않은 다른 에이전트가 검증해야만 인정된다. 이 과정에서 418건의 버그 리포트가 나왔고, 그중 약 55건은 일반 Python 코드만으로 인터프리터를 크래시시키거나 메모리를 손상시킬 수 있는 심각한 문제다.
가장 어려웠던 것은 AI 에이전트가 증명을 작성하게 하는 일이 아니었다. 의미 있는 증명을 작성하게 하는 일이었다.
HN 토론
54- debugnik
토큰을 ACSL 애노테이션을 추가해 Frama-C로 CPython을 검증하는 데 쓰는 게 더 생산적이지 않을까? AI가 번역한 것이 아니라 실제 런타임을 검증하게 될 테고, 수정 사항은 바로 업스트림에 기여할 수도 있을 텐데.
- anewhnaccount2
Julia 표준 라이브러리에도 같은 접근 방식: https://discourse.julialang.org/t/formalizing-julia-in-lean-...
- jakobnissen
이 버그 사냥 접근 방식은 정말 유망하다고 생각한다(당연히 - 버그를 엄청 많이 찾아내니까). 장기적인 문제는 이런 버그 사냥을 어떻게 일상적으로, 예를 들어 테스트 스위트의 일부로 수행할 수 있느냐다. 이 사람들이 택한 접근 방식은 Julia 쪽 사람들이 했을 때와 같은 방식인데, 인간과 AI 에이전트 양쪽의 작업이 많이 필요하기 때문에 사실상 자동화가 어렵다.
더 장기적으로는 코드와 Lean 증명이 따로 놀지 않도록 언어에 내장되어야 한다고 본다. 즉, 코드와 함께 작성되는 옵트인 속성(property)이 있고, 그것이 테스트 스위트에서 검사되는 식이다. 일반적인 컴파일러 검사와 매우 비슷하지만, 더 표현력이 좋고 비용이 크며, 테스트 시점에만 수행된다는 점이 다르다.
- tomtom1337
몇 가지 점이 혼란스러운데, 누군가 명확히 해주면 좋겠다!
- Lean으로의 재작성이 줄 단위로 이루어진다면, 어떻게 두 구현이 결과에서 다를 수 있나(2단계)?
- 이 접근 방식은 3단계에서 "항상 참이어야 하는 것"을 어떻게 아는가(LLM이 "추측"하는 지능인가)?
- erfgh
AI가 쓴 글을 읽는 사람이 있나? 진지한 질문이다.