LeanBET: Formally-verified surface area calculations in Lean

본 논문은 수학적 정확성을 보장하면서도 확립된 BETSI 참조 구현체와 거의 완벽한 수치적 일치를 달성하는 Lean 4로 구현된 완전히 실행 가능하고 형식적으로 검증된 브루너-엠티-텔러 (BET) 표면적 분석 파이프라인인 LeanBET 을 제시합니다.

핵심

상상해 보세요. 여러분이 스펀지의 표면적을 측정하려고 하는데, 그 스펀지는 보이지 않는 미세한 구멍으로 이루어져 있습니다. 과학자들은 BET(세 명의 과학자의 이름에서 유래) 이라는 방법을 사용하여 기체가 스펀지에 어떻게 달라붙는지 관찰함으로써 이 면적을 추정합니다. 이는 화학 분야에서 표준 도구이지만, 상자 위의 그림이 흐릿한 퍼즐을 풀려고 하는 것과 조금 비슷합니다.

여기에는 문제가 있습니다. 답을 얻기 위해 과학자들은 실험에서 특정 데이터 포인트 범위를 선택하고 그들을 통과하는 직선을 그려야 합니다. 문제는 서로 다른 사람들 (또는 다른 컴퓨터 프로그램) 이 약간 다른 범위를 선택할 수 있다는 점입니다. 한 사람은 "중앙 10 개 포인트를 사용하자"라고 말할 수 있고, 다른 사람은 "아니오, 중앙 12 개를 사용하자"라고 말할 수 있습니다. 이로 인해 동일한 스펀지에 대해 서로 다른 답이 도출되어 혼란과 결과에 대한 신뢰 부족을 초래합니다.

이를 해결하기 위해 한 팀은 모든 가능한 데이터 범위를 자동으로 확인하여 "최적"인 범위를 찾는 BETSI라는 컴퓨터 프로그램을 만들었습니다. 이는 퍼즐 조각의 모든 가능한 조합을 시도하여 완벽하게 맞는 조합을 찾는 로봇과 같습니다. 그러나 로봇조차도 버그가 있거나 미묘하게 잘못된 결과를 초래할 수 있는 숨겨진 가정을 가질 수 있습니다.

"LeanBET" 등장: 수학적으로 증명된 로봇

이 논문의 저자들은 Lean 4라는 특수한 컴퓨터 도구를 사용하여 이 로봇의 새로운 버전을 구축했습니다. Lean 4 를 단순히 프로그래밍 언어로 생각하지 말고, 증명 없이 실수를 허용하지 않는 엄격한 수학 선생님으로 생각하세요.

다음은 몇 가지 간단한 비유를 사용하여 그들이 어떻게 했는지 설명한 것입니다:

1. "두 개의 뇌" 시스템 (다형성)

일반적으로 컴퓨터 프로그램을 작성할 때 "부동 소수점 숫자"(계산기 위의 숫자 같은 것) 를 사용합니다. 이는 빠르지만 컴퓨터가 무한한 정밀도를 유지할 수 없기 때문에 약간 불완전합니다. 수학 증명을 할 때는 "실수"(완벽하고 무한한 정밀도) 를 사용하지만, 이를 컴퓨터에서 실행할 수는 없습니다.

저자들은 변신 로봇을 구축함으로써 이를 해결했습니다.

• 뇌 A (증명): 수학이 옳음을 증명해야 할 때, 로봇은 "실수" 정장을 착용합니다. 완벽한 이론적 수학으로 논리가 결함이 없음을 증명합니다.
• 뇌 B (실행): 실제 데이터로 프로그램을 실행해야 할 때, 로봇은 "부동 소수점" 정장으로 갈아입습니다. 실제 컴퓨터에서 빠르게 실행됩니다.
• 마법: 로봇이 두 가지 정장에서 동일한 방식으로 구축되었기 때문에, "증명 뇌"가 논리가 완벽하다고 말하면 "실행 뇌"도 반드시 동일한 규칙을 따르도록 보장됩니다. 완벽한 수학으로 교량 설계가 안전함을 증명하고, 실제 강철로 실제 교량을 건설할 때 그 설계가 견딜 수 있음을 아는 것과 같습니다.

2. "레시피 대 요리" (명세로서의 유도)

일반적인 과학에서는 종이 위에 레시피 (수학 이론) 를 쓰고, 셰프 (프로그래머) 가 부엌 (소프트웨어) 에서 요리를 시도합니다. 때로는 셰프가 여기에 약간의 소금을 추가하거나 단계를 오해하여 요리가 레시피와 다르게 맛이 날 수 있습니다.

LeanBET에서는 레시피와 요리가 같은 방에서 일어납니다. "수학적 유도"(레시피) 가 코드에 직접 작성됩니다. 컴퓨터는 코드가 레시피 그 자체임을 확인합니다. 코드가 "소금을 추가하라"고 말하면, 수학 증명이 "소금 추가"가 이론이 요구하는 것과 정확히 일치함을 검증합니다. 이론과 실천 사이에 간극이 없습니다.

3. "엄격한 검사관" (형식적 검증)

이 논문은 그들의 프로그램이 단순히 답을 "추측"하는 것이 아니라, 정확성 증명서를 지니고 있다고 주장합니다.

• 표준 소프트웨어: 프로그램을 실행하면 숫자가 나오고, 그것이 맞기를 바랍니다.
• LeanBET: 프로그램을 실행하면 숫자가 나오고, 또한 "모든 단계를 확인했고 모든 규칙을 따랐으며, 이 숫자는 여러분이 제공한 데이터를 기반으로 한 유일한 올바른 답입니다"라고 말하는 수학적으로 증명된 문서를 함께 건네줍니다.

그들이 발견한 것은 무엇입니까?

그들은 19 개의 서로 다른 데이터 세트 (19 개의 서로 다른 스펀지와 같은) 를 사용하여 새로운 "수학적으로 증명된 로봇"을 기존의 "표준 로봇"(BETSI) 과 비교 테스트했습니다.

• 결과: 19 개의 스펀지 중 18 개에서 두 로봇은 가장 작은 소수점 자릿수까지 정확히 동일한 답을 제시했습니다.
• 하나의 결함: 한 개의 스펀지 (UiO-66 이라고 함) 에서는 미세한 차이 (0.03%) 가 있었습니다. 저자들은 아직 그 이유를 확신하지 못한다고 인정하지만, 이는 실험에서 일반적으로 발생하는 노이즈에 비해 매우 작은 오차입니다.

결론

이 논문은 스펀지를 측정하는 새로운 방법을 발명하는 것이 아닙니다. 기존 방법을 신뢰할 수 있는 버전으로 구축하는 것입니다. 그들은 표준 과학 도구를 가져와 "수학 증명" 환경 내에서 재구축하고, 기존 도구만큼 잘 작동하지만 논리적 실수를 하지 않았다는 보장을 제공함을 보여주었습니다.

이는 일반적인 지도에서 GPS 로 업그레이드하는 것과 같습니다. GPS 는 경로뿐만 아니라 숨겨진 우회로 없이 그 경로가 가장 짧고 안전한 경로임을 단계별로 증명해 줍니다.

기술 요약

"LeanBET: Lean 에서의 형식적으로 검증된 표면적 계산"의 기술적 요약

문제 제기
Brunauer–Emmett–Teller(BET) 방법은 기체 흡착 등온선으로부터 비표면적을 추정하기 위한 표준 프레임워크입니다. 그러나 실제 구현에는 상당한 주관성이 수반되며, 특히 선형 회귀를 위한 상대 압력 범위 선택에서 두드러집니다. 일관성 기준 (Rouquerol 기준) 이 유효한 영역을 필터링하기 위해 존재하지만, 여러 압력 구간이 이러한 규칙을 만족하는 경우가 많아 서로 다른 실험실과 소프트웨어 구현체 간에 보고된 표면적의 변동성이 발생합니다. BET 표면 식별 (BETSI) 알고리즘과 같은 이전의 표준화 노력들은 범용 수치 소프트웨어 (Python) 에 의존합니다. BETSI 는 철저한 열거를 통해 주관성을 줄이지만, 숨겨진 구현 가정이나 미묘한 오류를 형식적으로 배제할 수 없는 수치 알고리즘으로 남아 있어 결과의 과학적 보장이 검증되지 않은 상태입니다.

방법론
저자들은 Lean 4 정리 증명기에 구현된 완전히 실행 가능하고 형식적으로 검증된 BET 분석 파이프라인인 LeanBET을 제시합니다. 이 접근법은 단일 환경 내에서 실행 가능한 코드와 수학적 증명을 통합하며, 다형적 수치 설계를 활용하여 계산과 검증 간의 간극을 해소합니다:

• 다형성: 알고리즘은 BETLike 타입 클래스에 의해 제약된 범용 타입 α를 사용하여 작성됩니다. 이를 통해 동일한 코드 구조가 실제 실험 데이터에 대한 효율적인 실행을 위해 부동 소수점 숫자(Float) 로, 그리고 비계산 가능한 수학적 증명을 위해 실수(Real) 로 인스턴스화될 수 있습니다.
• 유도로서의 명세: BET 선형화 방정식의 대수적 유도는 단순한 동기가 아니라 형식적 명세로 작용합니다. 코드는 이 유도를 반영하도록 구성되어 실행 가능한 변환이 이론적 모델과 일치하도록 보장합니다.
• 워크플로우: 파이프라인은 각각 형식적 증명과 짝을 이루는 다음 단계들을 수행합니다:
  1. 창 열거: 적어도 두 개의 데이터 포인트를 포함하는 등온선의 모든 연속 부분 리스트를 체계적으로 생성합니다.
  2. 선형화: 데이터 포인트 $(p, n)$을 선형화된 BET 형태 $p/[n(1-p)]$로 변환합니다.
  3. 선형 회귀: 각 창에 대해 최소 제곱 회귀를 수행하여 기울기, 절편 및 $R^2$를 추출합니다.
  4. 허용성 검사: Rouquerol 기준 ($n(1-p)$의 단조성, 매개변수 $C$와 $n_m$의 양수성, 그리고 단분자층 압력의 일관성) 에 따라 후보들을 필터링합니다.
  5. 무릎 선택: 유효한 창들 간의 동점을 해결하기 위해 가장 큰 끝 인덱스를 가진 창을 선택하고, 추가적인 동점은 가장 작은 백분율 오차로 깨뜨립니다.

주요 기여

1. BETSI 파이프라인의 형식적 검증: 이 논문은 전체 BETSI 워크플로우에 대한 최초의 기계 검증 구현을 제공합니다. 실행 가능한 코드가 BET 이론의 수학적 정의와 특정 선택 기준을 만족함을 증명합니다.
2. 정합성 및 완전성 증명: 저자들은 다음을 형식적으로 증명합니다:
   • 정리 A.1 및 A.2: BET 등온선 방정식은 층 모델 가정에서 유도되었으며, 선형화 단계는 대수적으로 정확합니다.
   • 정리 A.3: 창 열거는 정합적입니다 (유효한 창만 생성됨) 그리고 완전합니다 (유효한 연속 창이 누락되지 않음).
   • 정리 A.4 및 A.5: 회귀 단계는 진정한 최소 제곱 최소화기를 반환하며, 추출된 물리적 매개변수 ($n_m$, $C$) 는 이론적 정의와 일치합니다.
   • 정리 A.6 및 A.7: 허용성 검사 및 무릎 기반 선택 전략은 형식적 명세를 엄격하게 만족합니다.
3. 다형적 구현: 이 연구는 이상화된 실수 위에서 정확성이 증명되는 동안 부동 소수점 산술에서 실행이 이루어지는 Lean 내 과학적 계산을 위한 실용적 패턴을 보여줍니다. 이는 별도의 검증 언어가 필요하지 않도록 합니다.

결과
LeanBET 구현체는 19 개의 흡착 등온선으로 구성된 벤치마크 세트를 사용하여 참조 Python 기반 BETSI 구현체와 비교 평가되었습니다.

• 수치적 일치: LeanBET 은 19 개 등온선 중 18 개에서 기계 정밀도로 BETSI 참조와 일치합니다.
• 불일치: UiO-66데이터셋의 경우 약 0.03% (0.36 m²/g) 의 편차가 관찰되었습니다. 저자들은 이 특정 편차의 원인은 아직 결정되지 않았지만, 이는 일반적인 실험적 불확도보다 훨씬 작다고 강조합니다.
• 검증 상태: 모든 증명이 성공적으로 컴파일되어 알고리즘의 출력이 지정된 수학적 제약을 준수한다는 기계 검증 보장을 제공했습니다.

의의
이 논문은 LeanBET 이 확립된 참조 구현체와의 수치적 일치를 희생하지 않고도 정리 증명기 내에서 실용적인 과학 계산 워크플로우를 구축할 수 있음을 보여준다고 주장합니다. 주요 기여는 새로운 알고리즘이 아니라 정확성에 대한 형식적으로 검증된 보장입니다. 실행 가능한 파이프라인을 기계 검증된 수학적 명제와 연결함으로써, 이 연구는 구현이 근본 이론 및 선택 기준에 부합하는지에 대한 모호성을 제거하여 BET 분석의 재현성 위기를 해결합니다. 저자들은 이를 재료 과학에서 이론적 유도 및 소프트웨어 구현 간의 간극을 해소하는 단계로 위치시킵니다.