Lean에 검증된 커널이 함께 배포됩니다

AI 요약

Lean은 증명 커널의 취약점을 발견한 뒤 정식 커널을 보강하고, 여러 커널로 개발 내용을 다시 검사하는 도구를 배포합니다. Lean v4.35.0의 lake check는 개발 내용을 내보내 leanchecker로 재검사합니다. leanchecker는 주변 기능을 덜어낸 정식 Lean 커널입니다. 검사 과정은 샌드박스에서 실행하며, lake check --inadvisably-no-sandbox로 샌드박스를 끌 수 있습니다.

여러 커널로 재검사

Lean 배포판에는 기존 커널 외에 nanoda, lean4lean, con-leche, con-ron이 포함됩니다. lake check --paranoid는 이 커널들을 모두 사용해 개발 내용을 재검사하고, 메모리 손상을 조용히 잘못된 결과로 넘기지 않고 검사된 중단으로 처리하는 메모리 할당기를 적용한 정식 커널 변형도 실행합니다. 서로 다른 커널이 같은 오류를 공유할 가능성을 낮춰 증명 검사의 신뢰도를 높이는 방식입니다.

Lean으로 작성하고 일관성을 증명한 커널

con-leche는 Lean으로 작성한 첫 커널이며, 일관성 증명을 갖췄습니다. 여기서 일관성이란 con-leche가 받아들이는 모든 환경에 집합론적 모델이 존재한다는 뜻입니다. 증명은 Lean 타입 이론의 모델을 다룬 Mario Carneiro의 접근을 따릅니다. 이 증명 자체는 정식 Lean 커널이 검사하며, 모델에 사용한 집합론의 일관성을 가정합니다. 따라서 커널 구현의 프로그래밍 오류가 만드는 버그 유형을 제거한다고 설명합니다.

성능 측정에서 con-leche는 Mathlib 전체 내보내기 검증에 정식 커널이 실행한 명령어 수의 0.69배를 사용합니다. 8개 스레드로 전체 라이브러리를 약 100초 만에 검사합니다. 글은 성능 저하 없이 구현 오류 범주를 줄였다고 설명합니다.

Rust로 구현 경로를 분리한 con-ron

con-leche에도 컴파일러와 런타임, 큰 정수 라이브러리에서 생기는 오류가 남을 수 있습니다. 이를 줄이려고 Joachim Breitner는 AI를 이용해 con-leche를 Rust로 옮겼고, Aeneas로 Rust 구현이 con-leche의 검사 알고리즘을 따르는지 Lean에서 증명했습니다. 이 커널을 con-ron이라고 부릅니다. 두 구현이 서로 다른 언어의 컴파일러와 런타임을 거치므로 한쪽 구현 환경의 오류가 다른 쪽에도 똑같이 나타날 가능성이 낮다는 설명입니다.

lean4lean의 검증은 앞으로 몇 달 안에 끝날 것으로 예상합니다. 이 커널은 정식 C++ 커널의 구현을 매우 가깝게 따릅니다. Lean FRO는 커널을 단순화하는 개편도 진행합니다. Arthur Adjedj가 개편안을 구현하고 Joachim이 검토하며 con-leche와 증명도 함께 갱신합니다.

대규모 개발의 검사 비용

외부 커널 검사 방식은 대규모 프로젝트에서 확장성이 부족합니다. 글은 Anthropic의 FLT가 1,300만 줄 이상, Mathlib이 250만 줄, Tau Ceti가 300만 줄 이상이라고 밝힙니다. General Courtade-Kumar 정리 저장소는 5,000만 줄을 넘었고, Lean 커뮤니티에서는 10억 줄을 넘는 수학 라이브러리 제안도 나오고 있습니다. Lean FRO는 이런 규모에 맞춰 바이너리 내보내기 형식과 외부 검사기의 증분 검사를 개발 과제로 꼽습니다. 사용자는 현재 lake check --paranoid로 프로젝트를 검사하고 커널 간 불일치를 Lean FRO에 보고할 수 있습니다.

Hacker News 반응

• @s_Hogg — 이 제안은 결국 검사기를 계속 검사하는 구조 아닌가요?
  • @measurablefunc — 여러 검사기가 모두 같은 버그를 가질 가능성은 낮습니다. 결과를 더 많은 커널로 검사할수록 증명과 코드가 일관되고 올바를 가능성이 높아집니다. 커널의 정확성에 필요한 집합론적 가정은 남습니다.
• @sinuhe69 — 여기서 "검증됨"은 누군가 커널을 형식적으로 검증했다는 뜻인가요, 아니면 서로 다른 커널이 교차 검사한다는 뜻인가요?
  • @erichocean — 둘 다입니다.
• @cloudbonsai — Lean으로 커널을 구현하고 일관성을 증명했습니다. 컴파일러와 런타임 오류 가능성을 줄이려고 코드를 Rust로 옮긴 뒤 다른 검증 도구로 결과를 확인했습니다. Lean4 검증 프로젝트도 진행 중입니다.
  • @xiaoyu2006 — 그런데 순환 논증 아닌가요? 결국 괴델의 불완전성 정리에 걸리지 않나요?
  • @voxl — con-leche는 집합론을 가정합니다. 다만 커널이 Lean의 모든 기능을 포함하지는 않고 단순화도 진행 중입니다. 그래도 Lean은 현재 가장 신뢰할 만한 증명 보조기 중 하나일 겁니다.
• @runningmike — "AI가 소프트웨어의 취약점을 잘 찾는다"는 표현은 아닙니다. AI는 코드 약점을 찾을 수 있습니다. 취약점은 모두 약점이지만 모든 약점이 취약점은 아닙니다.
• @dwroberts — con-leche와 con-ron이 서로 다른 런타임을 써도 임의 정밀도 산술 구현을 공유하는 버그가 있을 수 있지 않을까요? 다른 소프트웨어에서도 이미 문제를 겪었을 거라고 기대할 수는 있겠지만요.

원문: Leo de Moura / 번역·요약: Trawling