기술 요약: BARReL - Atelier B를 위한 현대적인 Lean 기반 백엔드

문제 정의

B 방법론과 그 산업용 도구 세트인 Atelier B는 강력한 안전 보증 논거가 필요한 안전 필수 시스템을 개발하는 데 오랫동안 표준 역할을 해왔습니다. 그러나 이 생태계는 Atelier B의 내부 증명기(prover)에 크게 의존하고 있으며, 이는 효과적이기는 하지만 신뢰할 수 있는 컴퓨팅 기반(TCB) 측면에서 "블랙박스" 형태로 작동합니다. 이전의 노력들이 B를 Isabelle, PVS 또는 Rocq와 같은 현대적인 대화형 정리 증명기(ITP)와 연결하려는 시도를 해왔으나, 이러한 접근 방식들은 주로 B의 의미론(semantics)을 형식화하는 데 집중할 뿐, 기존의 산업적 워크플로우에 통합된 실용적인 백엔드를 제공하는 데는 미흡했습니다. 또한, 기존 도구들은 B 방법론의 핵심인 부분 연산자(예: min, 부분 도메인에서의 함수 적용)를 견고하게 처리하는 능력이 부족하며, 이는 논리적 건전성(well-definedness, WD)을 보장하기 위해 세심한 검증이 필요합니다. Atelier B의 대화식 모드에서 사용자는 규칙을 수동으로 적용하는 동안 의도치 않게 정의되지 않은 항(예: min(∅))을 인스턴스화할 수 있으며, 이는 도구가 유형 제약 조건을 강제하지 못할 경우 부적절한 증명으로 이어질 수 있습니다.

방법론

본 논문은 Atelier B와 Lean 증명 보조기를 연결하기 위해 설계된 Lean 4 라이브러리인 BARReL(B Automated tRanslation for Reasoning in Lean)을 소개합니다. 이 방법론은 B 증명 의무(Proof Obligations, POs)를 Lean 정리로 변환하는 모듈형 번역 파이프라인에 의존하며, Lean의 의존 타입 시스템(dependent type system)을 활용하여 구조적으로 잘 정의됨(well-definedness)을 강제합니다.

핵심 아키텍처

Figure 1에 묘사된 워크플로우는 네 가지 단계를 거칩니다:

1. 파싱 및 PO 생성: BARReL은 B 머신(.mch), 정제(refinement), 또는 기존의 PO 생성기(POG) 파일을 수용합니다. 이는 XML 형식으로 증명 의무를 생성하기 위해 Atelier B의 bxml 및 pog 도구를 호출합니다.
2. AST 정규화: XML 형태의 PO를 추상 구문 트리(AST)로 파싱하고 정규화합니다(예: P ∧ Q ⇒ R을 P ⇒ Q ⇒ R로 변환). 이는 후속 인코딩을 단순화하기 위함입니다.
3. 인코딩 및 메타 프로그래밍: 정규화된 B 공식은 Lean의 메타 프로그래밍 프레임워크를 사용하여 Lean 항으로 전사됩니다. 결정적으로, 이 계층은 B의 집합론적 구조를 Mathlib의 타입이 지정된 집합 및 관계 프리미티브로 매핑합니다.
4. 잘 정의됨(Well-Definedness, WD) 처리: 이것이 핵심적인 기술적 혁신입니다. BARReL은 B의 암시적인 부분 연산자 처리에 의존하는 대신, 모든 부분 연산자 사용에 대해 명시적인 WD 조건을 생성합니다.

부분 연산자 처리

B에서 min(S)나 함수 적용 f(x)와 같은 연산자들은 부분적입니다. Atelier B는 WD 사이드 목표(side goals)를 생성하지만, 이들이 만족되면 메인 목표가 성립한다고 가정합니다. BARReL은 이와 달리 부분 연산자를 명시적인 증명 파라미터를 요구하는 **전체 함수(total function)**로 인코딩합니다.

• 메커니즘: Classical.choose(Hilbert의 $\epsilon$ 연산자)를 사용하여, BARReL은 부분 연산자의 타입 시그니처에 증명 파라미터(예: min.WD S)를 포함하도록 정의합니다.
• 강제: min(S)를 Lean 항에서 사용하려면, 사용자는 S가 WD 조건(예: S가 비어 있지 않고 하한이 존재함)을 만족한다는 증명을 제공해야 합니다.
• 자동화: BARReL은 이러한 루틴한 WD 목표를 해결하기 위해 WD 증명을 사이드 정리 또는 서브골(subgoal)로 생성합니다. wd_min 또는 wd_app과 같은 카테고리로 태깅된 경량 자동화 택틱(tactic) 계층은 Mathlib의 재작성 규칙과 집합론적 보조 정리를 사용하여 이러한 WD 목표를 자동으로 해결하려고 시도합니다.

신뢰 경계(Trust Boundary)

이 시스템은 증명을 생성하는 백엔드로 설계되었습니다. 사용자가 Lean에서 목표를 해결하면, 결과물인 정리는 Lean의 작고 검증 가능한 커널에 의해 검사됩니다. 신뢰할 수 있는 구성 요소는 다음과 같이 축소됩니다:

1. Lean의 커널 및 메타 이론.
2. Atelier B의 외부 PO 생성( bxml/pog 단계)의 정확성.
3. B의 의미론을 Lean으로 인코딩하는 BARReL의 충실도.
   논문은 Atelier B의 대화형 계층(사용자가 변수를 수동으로 인스턴스화하는 단계)은 증명을 생성하지 않으며 불일치를 초래할 수 있다고 명시하며, BARReL은 Lean의 타입 체커를 통해 유형 정확성과 잘 정의됨을 강제함으로써 이 위험을 제거합니다.

주요 기여

1. BARReL 라이브러리: B의 구문과 표기법을 최대한 가깝게 유지하면서 B 개발(머신, 정제, 구현)을 Lean 정리로 변환하는 오픈 소스의 모듈형 Lean 4 백엔드입니다.
2. 명시적 잘 정의됨(Well-Definedness) 규율: B의 암시적 부분성을 명시적이고 증명 가능한 WD 조건으로 변환하는 번역 파이프라인입니다. 이를 통해 잘못된 유형이나 정의되지 않은 인스턴스화에 대한 묵시적 의존을 방지합니다. 이는 Atelier B의 대화형 증명기에서 알려진 함정입니다.
3. 평가 및 워크플로우: Lean 내에서 "최솟값 탐색" 알고리즘에 대한 3단계 정제 체인을 통한 엔드 투 엔드 과정을 입증합니다. 연구 결과, BARReL이 Atelier B보다 더 많은 양의 WD 목표를 생성하지만, 대다수는 자동으로 해결되어 사용자가 핵심 정제 로직에 집중할 수 있음을 보여줍니다.

결과

저자들은 "최솟값 탐색" 명세에 대한 3단계 정제 체인을 통해 BARReL을 평가했습니다.

• 규모: 사례 연구는 세 단계(명세, 두 번의 정제)에 걸쳐 총 190개의 목표를 생성했습니다.
• 잘 정의됨(WD) 오버헤드: 이 중 146개가 WD 조건이었습니다.
• 자동화 성공률: BARReL의 자동화는 생성된 WD 조건의 **100%**를 자동으로 해결했습니다.
• 비교:
  • Atelier B: 서브 골(sub-goal) 간에 조건을 공유하기 때문에 더 적은 WD 목표(예: 두 번째 정제에서 2개)를 생성했습니다. 그러나 대화형 증명기는 사용자가 주의하지 않을 경우 부적절한 인스턴스화(예: min(∅))를 허용할 수 있습니다.
  • BARReL: 각 발생 건수마다 조건을 구체화하기 때문에 더 많은 WD 목표(예: 두 번째 정제에서 100개)를 생성했습니다. 그러나 이들 모두 자동으로 해결되었으며, 남은 21개의 표준 PO는 Lean에서 대화형으로 증명되었습니다.
• 구현 지표: 핵심 툴링은 **1,331 라인의 코드(LoC)**로 구성되며, 지원하는 보조 정리 라이브러리와 자동화 택틱을 위해 추가로 1,282 LoC가 사용되었습니다.

의의 및 주장

본 논문은 BARReL을 Lean에 기반을 둔 강력하고 신뢰할 수 있는 Atelier B 툴체인을 향한 디딤돌로 규정합니다.

• 신뢰성: 증명 의무를 Lean으로 옮김으로써, BARReL은 모든 증명이 작은 검증된 커널에 의해 검사되도록 보장하며, Atelier B의 GUI에서 발견되는 부적절한 대화형 증명의 위험을 제거합니다.
• 사용성: 익숙한 B 구문과 구조를 유지하여 산업용 B 개발자의 학습 곡선을 최소화합니다.
• 확장성: 모듈형 설계는 새로운 B 구성 요소와 인코딩 규칙을 점진적으로 추가할 수 있게 합니다.
• 향atic 방향: 저자들은 세 가지 향후 연구 과제를 제시합니다:
  1. 지원되는 B 언어의 파편(fragment) 확장 (예: 시퀀스, 트리, 고급 한정사).
  2. 포섭(subsumption)을 통한 WD 목표의 중복 감소 (Atelier B에 비해 높은 목표 수를 해결하기 위함).
  3. Lean 내부에 검증된 PO 생성기를 개발하여, 궁극적으로 Atelier B의 pog를 신뢰할 수 있는 컴퓨팅 기반에서 제거하고 Lean에서 직접 B를 작성할 수 있는 임베디드 DSL을 가능하게 하는 것.

결론적으로, 본 논문은 BARReL이 원래 명세의 구조적 무결성을 희생하지 않으면서도 산업용 B 개발을 현대적인 타입 이론 기반 백엔드로 성공적으로 이주할 수 있음을 입증하였으며, 동시에 검증 과정의 건전성 보증을 크게 향상시켰음을 보여줍니다.