기술 요약: CSLib – 경량 컴퓨터 과학 라이브러리

문제 제기

Lean 증명 보조 도구는 Mathlib를 통해 수학 분야에서 상당한 성공을 거두었으나, 공식화된 컴퓨터 과학(CS) 지식을 위한 포괄적이고 통합된 저장소는 현재 부재한 상태입니다. Lean 내의 기존 CS 지식 기반은 제한적이며, 이는 컴퓨터 과학 교육, 연구, 그리고 대규모 검증 시스템의 엔지니어링에 대한 광범적인 도입을 저해하고 있습니다. 나아가, 코드 생성에서의 AI 부상은 새로운 위험을 초입합니다: AI 에이전트가 의도치 않게 취약점을 도입할 수 있으며, 악의적인 행위자가 AI를 악용하여 보안 결함을 찾아낼 수도 있습니다. 형식 검증(Formal Verification)은 이러한 위험에 대한 제안된 해결책이지만, 역사적으로 그 채택은 막대한 인간의 노력(예: seL4 커널에 필요한 20인년 이상의 노력)으로 인해 제약을 받아왔습니다. 따라서 형식 검증의 장벽을 낮추고, 일상적인 명령형 코드의 검증을 지원하며, 컴퓨터 과학을 위한 AI 보조 추론에 필요한 인프라를 제공하는 프레임워크가 시급히 필요합니다.

방법론

CSLib는 이러한 격차를 해소하기 위해 두 가지 기둥(two-pillar)으로 구성된 기술적 접근 방식을 제안합니다.

기둥 1: Lean에서의 컴퓨터 과학 공식화

이 기둥은 Mathlib와 구별되면서도 상호 보완적인, 공식화된 CS 개념의 일관되고 통합된 라이브러리를 구축하는 것을 목표로 합니다.

• 모델 및 논리: CSLib는 다양한 계산 모델(결정론적, 비결정론적, 확률적, 양자, 함수형, 온라인, 인터랙티브)과 명세 표기법(시간 논리, 호어 논리, 분리 논리, 선형 논리)을 공식화할 것입니다. 순수 수학에 집중하는 Mathlib와 달리, CSLib는 레이블된 전이 시스템(labeled transition systems) 및 쌍사상(bisimulations)과 같은 CS 특유의 산출물을 대상으로 합니다.
• 알고리즘 및 자료 구조: 이 라이브러리는 표준 학부 주제(정렬, 그래프, 해시 테이블)부터 고급 분야(양자 알고리즘, 수학적 최적화)에 이르기까지 공식적으로 검증된 알고리즘과 자료 구조를 포괄할 것입니다.
• 복잡도 분석: 핵심 목표는 알고리즘 복잡도의 체계적인 공식화입니다. 본 논문은 계산이 값과 시간 비용을 함께 반환하는 모나딕 API(Writer 모나드에서 영감을 얻음)를 제안합니다. 이는 시간 복잡도를 하나의 계산 효과(computational effect)로 취급하여, 기능적 정확성과 복잡도 분석을 직교(orthogonal)하게 만들 수 있게 합니다. 현재는 수동적인 tick 주석에 의존하고 있으나, 이는 보편적인 프레임워크를 향한 가벼운 시작점 역할을 하며, 향후 명시적인 RAM 및 쿼리 모델로 진화할 계획입니다.

기둥 2: 일상적인 코드를 위한 추론 인프라

이 기둥은 Lean의 형식적 추론과 주류 명령형 프로그래밍 언어(예: Rust, C++, Python) 사이의 간극을 메웁니다.

• Boole 중간 검증 언어(IVL): CSLib는 Lean 내에 임베딩된, Boogie에서 영감을 받은 새로운 IVL인 Boole을 도입합니다. Boole은 의사코드(pseudocode)처럼 보이도록 설계되었으며, Lean 명세(사전 조건, 루프 불변량, 단언)가 삽입된 고전적인 명령형 구문을 지원합니다.
• 검증 파이프라인: 아키텍처는 다음과 같은 과정을 포함합니다:
  1. 트랜스파일링(Transpilation): 주류 언어의 코드를 Boole로 번역합니다.
  2. 조건 생성(Condition Generation): Boole 코드와 명세를 Lean 검증 조건(VCs)으로 변환합니다.
  3. 증명 자동화(Proof Automation): 이러한 VCs는 Lean 자동화(Lean-SMT를 통한 SMT 솔버, smt와 같은 '해머' так틱, 그리고 잠재적인 AI 기반 증명기 포함)를 사용하여 해결됩니다.
• 설계 원칙: 시스템은 Boole을 Lean에 깊게 임베딩함으로써 최소한의 신뢰 컴퓨팅 기반(TCB)을 우선시합니다. 검증 조건은 직관적인 Lean 목표(goals)로 생성되어, 기둥 1에서 확립된 풍부한 정의의 유니버스를 활용할 수 있게 합니다.

주요 기여

1. CSLib 프레임워크: "컴퓨터 과학을 위한 Mathlib"를 목표로 하는, Lean에서의 CS 공식화를 위한 통합된 오픈 소스 라이브러리의 도입.
2. Boole IVL: 명령형 코드를 Lean에서 검증 가능한 정리로 변환함으로써 코드 검증을 용이하게 하는 중간 언어인 Boole의 설계 및 초기 구현.
3. 복잡도 모나딕 API: Lean 내에서 알고리즘 복잡도를 공식화하는 참신한 접근 방식으로, 단일 프레임워크 내에서 기능적 정확성과 최악의 시간 경계(예: MergeSort)를 모두 증명할 수 있게 함.
4. 검증 파이프라인 아키텍처: Boole을 통해 주류 코드를 Lean 증명으로 연결하는 도구 체인의 구체적인 비전(다이얼렉트의 깊은 임베딩을 위한 Strata 및 검증 조건 생성을 위한 얕은 임베딩을 위한 Loom과 같은 기존 오픈 소스 프로젝트 활용).

결과 및 현재 상태

본 논문은 완료된 대규모 실험 결과 보고서라기보다 비전과 초기 진전을 개략적으로 설명하는 백서(white paper)를 제시합니다.

• 초기 구현: CSLib 저장소에는 이미 운영 의미론(operational semantics), 프로그램 동등성, 오토마타 모델, 선형 논리 및 기초적인 정렬/탐색 알고리즘의 초기 공식화가 포함되어 있습니다.
• 프로토타입 검증: 프로토타입 검증 조건 생성기가 시연되었습니다. 단순한 루프 예제(정수 합산)를 사용하여, 시스템은 진입 불변량(entry invariants), 루프 유지(loop maintenance) 및 단언(assertions)에 대한 Lean 검증 조건을 성공적으로 생성했습니다. 이러한 조건들은 목표를 SMT 수식으로 변환하고, 이를 해결한 뒤 Lean에 증명을 재현하는 smt так틱을 사용하여 자동으로 해결되었습니다.
• 로드맵: 프로젝트는 2026~2027년의 잠정적인 로드맵을 제시하며, 2026년 말까지 학부 수준의 알고리즘과 이론을 다루고, 2027년 말까지 상당한 규모의 실제 시스템에 대한 엔드 투 엔드(end-to-end) 검증을 달성하는 것을 목표로 합니다.

의의 및 주장

본 논문은 CSLib가 다음 두 가지 주요 방식으로 컴퓨터 과학 연구 및 엔지니어링의 지형을 근본적으로 변화시킬 것이라고 주장합니다:

1. 소프트웨어 신뢰성에 대한 실질적 영향: 검증된 컴포넌트로부터 신뢰할 수 있는 시스템을 구성적으로 도출하는 것을 가능하게 하고, 검증을 위한 AI 사용을 단순화함으로써, CSLib는 AI 기반 코드 생성 및 공격의 시대에 안전한 소프트웨어에 대한 절박한 요구를 해결합니다. 이는 전통적인 방식인 seL4의 "비용 페널티"를 넘어 형식 검증을 상업적 채택이 가능할 만큼 확장 가능하게 만드는 것을 목표로 합니다.
2. 연구 및 AI 시너지: CSLib는 21세기 CS 연구를 위한 플랫폼으로서, 수학적으로 근거 있는 발견과 기초 개념의 대규모 재사용을 가능하게 합니다. 결정적으로, CSLib는 AI 시스템이 공식화 및 정리 증명을 학습할 수 있도록 하는 고품질 데이터 저장소 역할을 합니다. 역으로, 본 논문은 AI 도구가 CSLib 자체의 개발을 가속화하여, 인간 전문가와 AI 도구가 점진적으로 더 효율적으로 검증된 지식을 생산하게 되는 "플라이휠(flywheel)" 효과를 창출할 것이라고 상정합니다.

저자들은 AI가 생성한 공식화가 버그나 인간의 이해 가능성 부족이라는 위험을 수반할 수 있지만, AI가 조언자의 역할만 수행하도록 하는 '인간 참여형(human-in-the-loop)' 코드 리뷰 프로세스를 유지함으로써 이러한 위험을 완화할 수 있다고 강조합니다. 궁극적인 목표는 형식 방법을 이론가부터 시스템 빌더에 이르기까지 광범위한 컴퓨터 과학자들이 접근할 수 있도록 민주화하는 것입니다.