Julia 코드 일부를 Lean으로 형식화해 분석한 결과, Base에서 버그 약 400건이 발견됐다. MilesCranmer 계정의 연구자는 이 가운데 중복 여부와 실제 영향 가능성을 확인해 75건을 Julia 저장소에 보고했으며, 분석 범위는 Base 전체가 아니라 일부 파일과 표준 라이브러리다.
프로젝트 저장소에는 설명과 Lean 코드, 발견된 버그 목록이 공개돼 있다. 이 방식은 Julia 함수의 동작을 Lean 모델로 옮기고, 문서의 약속이나 불변 조건을 정리해 증명하거나 반례를 찾는다. 반례는 실제 Julia 스크립트로 같은 동작이 재현돼야 발견 사례로 인정했다. 예를 들어 정수 범위의 역순을 만들 때 최솟값의 부호 반전이 고정 폭 정수에서 그대로 되돌아가 원소 수가 달라지는 문제가 보고됐다.
연구자는 Lean 모델을 실제 Julia와 비교하는 차등 테스트를 먼저 수행했다고 밝혔다. 정수 핵심 부분은 Int8·UInt8의 656,896개 전체 사례와 대조했고, Float64 모델은 236,954개 연산을 비교했다. 증명 빌드에는 미완성 증명이나 추가 공리를 막는 검사도 두었지만, 형식 검증 결과는 Lean 모델에 대한 증명이지 Julia 코드에서 자동 생성된 증명은 아니다. 모델 범위도 base/ 약 90개 파일의 일부와 몇몇 표준 라이브러리에 한정된다.
약 5,000달러 상당의 API 사용량이 들었으며, 대부분 Claude Opus 5.5와 OpenAI의 Daybreak Blue를 사용했다고 연구자는 설명했다. 발견한 버그 중 일부는 경계 사례에 그치거나 의도된 동작인지 불분명해 보고하지 않았다. 메모리 안전성 분석은 아직 끝나지 않았고, C 런타임 형식화도 약 10% 진행된 상태라 저장소에 공개되지 않았다.
자신의 Julia 패키지에 적용하려는 경우 저장소의 DynamicExpressions.jl 모델을 참고해 작은 핵심 모듈부터 시작하고, 에이전트가 증명을 시도하기 전에 차등 테스트와 감사 절차를 마련하라고 권했다.
댓글 (0)
로그인하면 이 기사에 내 생각을 남길 수 있어요