DSLean: Lean 4 와 외부 DSL 간의 타입 정확성 있는 상호 운용성을 위한 프레임워크

이 논문은 인터랙티브 정리 증명기 (ITP) 인 Lean 4 와 외부 자동화 도구 간의 상호 운용성을 간소화하기 위해 DSLean이라는 새로운 프레임워크를 제안합니다. DSLean 은 Lean 표현과 외부 도메인 특화 언어 (DSL) 간의 양방향 번역을 자동화하여, 메타 레벨 구현 세부 사항을 추상화하고 타입이 올바른 Lean 표현을 보장합니다.

1. 문제 정의 (Problem)

인터랙티브 증명기에서 외부 자동화 (예: SMT 솔버, 컴퓨터 대수 시스템) 를 활용하여 증명을 보조하거나 재구성하는 것은 일반적이지만, 이를 구현하는 과정은 다음과 같은 이유로 매우 번거롭고 복잡합니다.

• 수동 번역의 어려움: Lean 의 내부 표현과 외부 DSL 간의 번역을 위해 매번 맞춤형 (bespoke) 중간 구조를 개발해야 합니다.
• 메타 레벨 코드의 복잡성: 외부 도구에서 나온 원시 데이터를 Lean 표현식으로 변환하려면, 파싱, 구체적 구문 트리 (CST) 에서 추상 구문 트리 (AST) 로의 확장 (elaboration), 그리고 Lean 표현식 재구성 등을 수행하는 메타 레벨 코드를 직접 작성해야 합니다.
• 유지보수 및 접근성: 이러한 코드는 특정 응용 프로그램에 종속적이며, Lean 메타 프로그래밍에 대한 깊은 전문 지식을 요구하여 유지보수가 어렵습니다.
• 타입 안전성 부재: 외부 도구와의 통신 과정에서 타입 오류가 발생할 수 있으며, 이를 검증하는 메커니즘이 부족합니다.

2. 방법론 (Methodology)

DSLean 은 Lean 4 내에서 완전히 구현되었으며, Lean 의 네이티브 파서와 메타변수 통일 (metavariable unification) 알고리즘을 활용합니다.

2.1 핵심 설계 원칙

1. 타입 유도 (Type Induction): DSL 사용자에게 타입 제약을 명시하게 하는 대신, Lean 의 타입 시스템이 외부 구문에 대한 타입 제약을 유도하도록 합니다. 패턴 매칭 및 재구성 단계에서 타입 정확성을 검증하여 복잡한 언어 명세를 지원합니다.
2. 왕복 일관성 (Round-trip Consistency): Lean 표현을 외부 DSL 로 변환했다가 다시 Lean 으로 되돌렸을 때, 정의적 동치 (definitional equality) 를 기준으로 동일한 객체가 되도록 설계합니다.
3. 사용자 친화성: 파싱, 확장 (elaboration), 우선순위 설정, 타입 클래스 합성, 다형성 처리 등 복잡한 메타 프로그래밍 세부 사항을 자동으로 처리하여 사용자는 언어 명세만 작성하면 됩니다.

2.2 번역 프로세스

• Lean → 외부 DSL:
  • 사용자가 정의한 등가 규칙 (equivalence) 을 기반으로 Lean 표현식을 외부 패턴과 부분적으로 매칭합니다.
  • 메타변수 (metavariables) 를 사용하여 아직 결정되지 않은 하위 표현식을 처리하며, 정의적 동치 검사를 통해 매칭을 확인합니다.
  • 바인더 (binder) 내부의 자유 변수를 바인딩된 변수로 변환하는 등의 처리를 수행합니다.
• 외부 DSL → Lean:
  • 파싱 (Parsing): Lean 의 네이티브 파서 (Pratt 파서 기반) 를 사용하여 외부 구문을 중간 데이터 구조로 파싱합니다.
  • 확장 (Elaboration): 파싱된 구조를 Lean 의 메타변수 통일 알고리즘을 사용하여 점진적으로 Lean 표현식으로 확장합니다. 이 과정에서 타입 추론이 지연된 경우 (예: 전술) 를 처리하고, 타입이 올바른지 검증합니다.

2.3 주요 기능

• 양방향 및 단방향 지원: 완전한 역변환이 불가능한 경우에도 한 방향으로만 매핑을 정의할 수 있습니다.
• 다형성 및 지연 확장: Lean 과 유사한 수준의 다형성을 지원하며, 타입에 의존하는 값의 확장을 지연시켜 처리합니다.
• 구문 조정: 연산자의 결합 방향 (associativity) 과 우선순위 (precedence) 를 자동으로 결정하거나 사용자가 수동으로 조정할 수 있습니다.

3. 주요 기여 (Key Contributions)

1. DSLean 프레임워크 개발: Lean 4 와 임의의 외부 DSL 간 양방향 번역을 위한 완전한 프레임워크를 구현했습니다.
2. 간소화된 구현: 복잡한 메타 프로그래밍 코드를 추상화하여, 약 300 줄의 코드만으로 복잡한 자동화 전술을 구현할 수 있게 했습니다.
3. 세 가지 새로운 자동화 전술 구현 및 검증:
   • gappa: Gappa [6] 구간 산술 솔버와 연동하여 실수 범위에 대한 증명을 수행합니다. Rocq(Rocq) 구문으로 작성된 증명 인증서를 Lean 으로 번역합니다.
   • desolve: SageMath [27] 컴퓨터 대수 시스템과 연동하여 상미분 방정식 (ODE) 의 일반 해를 구하고 Lean 으로 재구성합니다.
   • lean_m2: Macaulay2 [8] 패키지와 통신하여 링 이상 (ring ideal) 소속성 및 그뢰브너 기저 (Gröbner bases) 문제를 해결합니다.

4. 결과 (Results)

• 코드 효율성: 기존에 수천 줄의 맞춤형 코드가 필요했던 번역 로직을 DSLean 을 사용하여 약 300 줄 이하로 단축했습니다. 예를 들어, lean_m2 전술의 구현 코드는 DSLean 도입 후 5 배 감소했습니다.
• 기능성:
  • gappa 전술은 실수 구간 계산에 대한 비자명한 증명을 자동으로 수행합니다.
  • desolve 전술은 다양한 미분 방정식에 대한 해를 SageMath 를 통해 구하고 Lean 에서 검증 가능한 형태로 제공합니다.
  • lean_m2 전술은 다항식 환, 몫 환 (quotient rings) 등 기존 polyrith 전술보다 더 넓은 범위의 이상 소속성 문제를 해결합니다.
• 유연성: Rocq, SageMath, Macaulay2 등 서로 다른 외부 도구와의 연동을 성공적으로 시연했습니다.

5. 의의 및 결론 (Significance)

• 접근성 향상: Lean 메타 프로그래밍의 높은 진입 장벽을 낮추어, 외부 자동화 도구를 Lean 에 통합하는 과정을 단순화했습니다.
• 확장성: DSLean 은 특정 도메인에 국한되지 않으며, 프로그램 검증, 자연어 번역, 다른 형식적 시스템과의 연동 등 다양한 분야에서 활용 가능합니다.
• 신뢰성: 외부 솔버의 결과를 Lean 내에서 타입이 올바르게 검증된 표현식으로 변환함으로써, "신뢰할 수 있는 오라클 (trusted oracle)"로서의 역할을 수행할 수 있는 기반을 마련했습니다.
• 미래 전망: 부동소수점 산술, ODE 이론의 기초 정리 등 Lean 에 아직 충분히 정립되지 않은 분야에서도 DSLean 을 통해 자동화 도구를 구축할 수 있는 가능성을 제시합니다.

요약하자면, DSLean 은 Lean 4 생태계에서 외부 자동화 도구의 활용을 획기적으로 증대시키는 핵심 인프라로, 복잡한 메타 프로그래밍을 추상화하고 타입 안전성을 보장함으로써 형식적 증명과 외부 계산 도구의 융합을 가능하게 합니다.