Lean, 검증된 증명 커널 네 개 추가
원제 Lean now ships with verified kernels
129 포인트댓글 44
Key Point
Lean 증명 보조기의 핵심인 커널에 버그가 증명을 검증하지 못하는 치명적 문제를 여러 커널로 재검증해 해결하는 방식이 도입되었고, 특히 형식적으로 증명된 Lean 기반 커널의 등장으로 신뢰성이 크게 강화되는 시점이다.
핵심 요약
- Lean v4.35.0부터 lake check 명령으로 개발 환경을 leanchecker(공식 커널)로 재검증할 수 있으며, 프로세스는 샌드박스에서 실행된다.
- nanoda, lean4lean, con-leche, con-ron 네 개의 추가 커널을 탑재했고, lake check --paranoid로 모든 커널로 증명을 재검증할 수 있다.
- con-leche는 Lean으로 작성되고 일관성이 증명된 첫 번째 커널이며, Claude(Fable과 Opus)가 구현하고 Joachim Breitner가 감독했다.
- 일관성 증명은 집합론 모델을 따르며 커널 구현의 프로그래밍 오류라는 전체 종류의 버그를 제거한다.
- con-leche는 공식 커널의 0.69배 명령어로 Mathlib 전체를 약 100초에 8개 스레드로 검증한다.
- con-ron은 AI가 con-leche를 Rust로 변환하고 Aeneas 도구로 Rust 버전이 con-leche의 검증 알고리즘을 정제함을 증명했다.
- con-leche의 형식적 증명이 있으므로, 남은 오류는 Lean의 컴파일러나 런타임에 있을 가능성이 높으며, con-leche와 con-ron 둘 다로 검증하면 이런 버그로부터 높은 수준의 보호를 얻는다.
- lean4lean의 검증은 앞으로 몇 개월 안에 완료될 예정이다.
- Arthur Adjedj는 커널 개선 계획(이슈 #14977)을 진행 중이며 여러 PR을 제출했다.
- 현재 문제는 규모 확장성으로, Anthropic의 FLT는 1300만 줄, Mathlib는 250만 줄, Tau Ceti는 300만 줄을 초과했고, 커뮤니티는 10억 줄 이상의 수학 라이브러리를 제안하고 있다.
- 이 규모에는 이진 내보내기 형식과 외부 커널의 점진적 검증이 필요하며, Lean FRO에서 이 문제들을 해결 중이다.