소프트웨어 엔지니어를 위한 Lean 형식 증명 완전 분석

핵심 요약

• 소프트웨어 엔지니어 입장에서 형식 증명이 무엇인지 이해하기 위해 Lean을 이용해 결정적 유한 오토마타(DFA) 이론 문제를 증명한 과정을 설명한다.
• 계산 이론 교재의 문제: 세 행의 비트 문자열(최상단 + 중간 = 최하단)에서 덧셈이 성립하는지 검증하는 언어 B가 정규언어임을 증명하는 것이었다.
• 정규언어의 폐쇄성을 이용해 B의 역순 B^R을 인식하는 DFA를 구성하면, B^R이 정규이므로 그 역순인 B도 정규임을 결론 낼 수 있다.
• DFA는 3개 상태(캐리 0, 캐리 1, 데드)를 가지며, 이진 덧셈의 캐리 메커니즘을 따른다: 현재 캐리와 두 입력 비트의 XOR로 합 비트를 검증하고, 다음 캐리를 계산한다.
• Lean 증명은 세 부분으로 구성된다: 언어 B의 명세(집합 표기법으로 정의), DFA 구현(실행 가능한 코드), 명세와 구현이 일치함을 보이는 증명이다.
• 언어를 함수로 정의하되, 반환 타입이 불린이 아니라 명제(Prop)다: 멤버십 테스트는 컴파일 타임에 타입 검사로 변환되어, 단순 런타임 계산이 아닌 증명으로 처리된다.
• Lean에서 명제의 증명은 그 명제를 타입으로 하는 항(term)을 구성하는 것과 같다: 명제가 참 ⟺ 타입이 적어도 하나의 값을 가짐, 거짓 ⟺ 증명 불가능하게 어떤 값도 가지지 않음.
• DFA 상태는 귀납 타입으로 정의되며, DecidableEq 파생(완전 동등성 검사)과 Fintype 파생(유한 상태 증명)을 통해 증명 보조 라이브러리 Mathlib과 통합된다.
• dfaStep 함수를 단위 테스트처럼 컴파일 타임 명제로 검증할 수 있다: 예시 입력에 대해 정확한 출력을 증명하는 example 구조를 사용한다.
• 정규성 증명의 핵심은 모든 단어에 대한 전역 방정식(row1 + row2 = row3)이 DFA의 단계별 처리와 동치임을 보이는 귀납적 불변식을 세우는 것이다.
• 귀납 가설은 카리인(cin)과 카리아웃(cout)을 포함하도록 확장되어야 한다: 임의의 초기 캐리로 시작해도 evalFrom의 결과와 확장된 덧셈 방정식이 동치가 되도록 정의한다.
• 확장된 불변식은 row1 + row2 + carryIn = row3 + carryOut × 2^|w|로, 이는 이진 덧셈의 정의와 일치하며 cin=cout=0일 때 원래의 언어 멤버십 테스트와 같아진다.
• 형식 증명의 이점은 복잡한 산술 논리를 단순 DFA 스텝 함수로 축약할 수 있고, Mathlib의 기존 정리(역순 폐쇄성 등)를 재사용함으로써 증명 작업량을 크게 줄일 수 있다는 점이다.