A Machine-Checked Cost Analysis of the BMSSP Recurrence in Isabelle/HOL With a Non-Vacuous Size-Parametric Runtime Witness

기술 요약: BMSSP 재귀에 대한 기계 검증된 비용 분석

문제 정의
본 논문은 2025년 Duan, Mao, Mao, Shu, Yin의 알고리즘이 달성한, 유향 단일 출발점 최단 경로(SSSP)의 오랜 $O(m + n \log n)$ "정렬 장벽"을 깨뜨린 핵심 엔진인 Bounded Multi-Source Shortest Path (BMSSP) 재귀의 형식적 검증을 다룬다. 원본 알고리즘은 $O(m \log^{2/3} n)$의 실행 시간을 달성하지만, 이를 증명 보조기(proof assistant)에서 정식화하는 과정, 특히 그 타당성과 분할 데이터 구조에 대한 분할 상환 비용(amortized cost) 분석을 정식화하는 것은 상당한 어려움을 수반한다. 이러한 어려움에는 소스 집합과 유계 거리 범위를 포함하는 재귀적 정당성 논증의 복잡성, 커스텀 파티션 데이터 구조에 대한 분할 상환 회계의 섬세함, 그리고 입력 패밀리가 유계이거나 필요한 실행이 존재하지 않아 기술적으로는 참이지만 의미가 없는 "공허한(vacuous)" 점근적 정리의 위험 등이 포함된다.

방법론
저자들은 모듈성을 확보하고 관심사의 엄격한 분리를 보장하기 위해 6개의 뚜렷한 계층적 이론으로 구성된 Isabelle/HOL(Isabelle2025-2) 기반의 완전한 정식화를 제시한다. 이 개발 과정은 외부 공리, sorry, 또는 oops 문 없이 오직 HOL과 HOL-Library만을 임포트한다.

1. 의미론적 기초 (Semantic Foundations): 저자들은 유한 가중치 유향 그래프, 단순 보행(simple walks), 그리고 거리 메트릭을 정의한다. 고유한 최단 보행 및 엄격한 타이 브레이킹(tie-breaking)에 관한 구조적 보조 정리를 확립하며, 이는 이후 모든 논증의 기초가 된다.
2. 재귀적 정당성 (Recursive Correctness): BMSSP 재귀의 추상 모델을 정식화하며, 여기에는 FindPivots 루틴, 기저 사례(base cases), 그리고 파티션 루프가 포함된다. 기계 검증된 증명은 추상 알고리즘이 잘 형성된 임의의 그래프에 대해 최단 거리를 올바르게 계산함을 입증한다.
3. 실행 가능한 산출물 (Executable Artifact): 추상 모델은 자연수 정점과 가중치를 사용하는 실행 가능한 함수(bmssp_distances)로 구체화된다. 저자들은 bmssp_correct_strong를 증명하여, 실행 가능한 출력값이 최단 거리의 의미론적 정의와 일치함을 확인하며, 이는 특정 5개 정점 예시에 대한 평가를 통해 검증된다.
4. 비용 모델 (Cost Model): 비용 술어(cost predicates)를 가진 추상 파티션 인터페이스(Insert, BatchPrepend, Pull)가 정의된다. 저자들은 이 추상 재귀에 대해 $O(m \log^{2/3} n)$의 분할 상환 비용 엔벨로프를 증명한다. 결정적으로, 그들은 논문의 로그 스케줄을 충실히 구현하는 **버킷형 파티션 데이터 구조(bucketed partition data structure)**를 구현하여, 속도 향상에 필요한 결정적인 $O(\log(N/M))$ 삽입 스케일을 증명한다.
5. 운영적 구체화 (Operational Refinements): 두 가지 운영 계층이 정의된다:
   • Exact-Concrete: 재귀적 자식의 출력을 증가하는 범위 슬라이스에 엄격하게 결합한다.
   • Charged: 출력을 분리하고, 증가하는 슬라이스에 대해서만 비용을 부과한다.
     저자들은 exact-concrete 관계가 의도된 입력(특히 경로 패밀리)에 대해 **비전체적(non-total)**임을 기계 검증하여, 완전한 실행이 존재할 수 없는 장애물이 발생함을 보여준다.
6. 크기 매개변수 계층 (Size-Parametric Layer): 저자들은 무한한 단위 가중치 유향 경로 패밀리($P_n$)를 구축한다. 이들은 charged 관계가 전체적(total)이며 완전한 실행이 존재함을 증명한다. 점근적 클래스를 변경하지 않으면서 전체성을 확보하기 위해, "확장된(inflated)" 스케줄 인덱스($N = n \cdot n$)를 사용하여 버킷 용량이 경로를 커버하면서도 $O(\log^{2/3} n)$ 인자를 보존하도록 한다.

주요 기여

• 최초의 기계화된 정식화: BMSSP 재귀 및 그 실행 시간 분석에 대한 최초의 기계 검증된 정식화이다.
• 비공허한 크기 매개변수 증거: 본 논문은 단위 가중치 유향 경로 상에서 charged 실행 시간이 $O(|V| \cdot (\ln |V|)^{2/3})$임을 입증하는 완전한 무조건적 정리를 제공한다. 이 결과는 저자들이 "비공허성 원장(non-vacuity ledger)"을 통해 패밀리가 무한히 성장하고, 완전한 실행이 존재하며, 작동 체계가 실현됨을 명시적으로 증명했기에 비공허하다.
• 결합 장애의 형식적 진단: 저자들은 나이브하고 긴밀하게 결합된 비용 관계(exact-concrete 모델)의 결함을 공식적으로 식별하고 증명한다. 이 관계가 경로 패밀리에 대해 알고리즘을 최대 한 단계만 수행하도록 강제하여, 이를 기반으로 한 크기 매개변수 경계가 공허해짐을 보여준다. 이 장애물은 기계 검증된 보조 정리로 기록되며, 헤드라인 결과는 이를 우회하기 위해 분리된 charged 관계를 사용하여 도출된다.
• 실행 가능 검증: 개발 과정에는 최단 거리 계산 실행 함수와 코드 평가를 통해 검증된 정당성 증명이 포함된다.

결과
헤드라인 정리인 path_nonvac_runtime_bigo_card_V_unconditional은 다음과 같다:
$$(\lambda n. \text{real}(\text{path\_nonvac\_time } n)) \in O(\lambda n. \text{real}(\text{card}(\text{path\_k\_V } n)) \cdot (\ln(\text{real}(\text{card}(\text{path\_k\_V } n) + 2))^{2/3})$$
이 경계는 다음을 만족한다:

• 무조건적(Unconditional): 실행 존재 여부나 그래프 특성에 대한 가설 없이 패밀리의 정의만으로 성립한다.
• 크기 매개변수적(Size-Parametric): 점근적 변수는 고정된 파라미터가 아닌 실제 그래프 크기($|V|$)이다.
• 비공허적(Non-Vacuous): 존재가 증명된 최소 비용(least-cost) 실행의 비용을 제한한다.

또한 본 논문은 구체적인 버킷 구조에 의해 실현된 추상 비용 모델에 대해 $O(m \log^{2/3} n)$ 경계를 확립하여, $O(\log(N/M))$ 삽입 스케일을 확인한다.

의의 및 범위
저자들은 본 연구의 의의를 Duan–Mao–Mao–Shu–Yin SSSP 구현의 엔드 투 엔드 검증이 아니라, BMSSP 재귀의 정당성과 charged 실행 시간 분석에 대한 엄격한 정식화로 규정한다.

• 주장하는 바: 본 논문은 재귀 로직의 정당성과 특정 무한 패밀리에 대한 비공허한 점근적 경계를 포함한 charged 연산 비용 분석의 유효성을 검증했다고 주장한다.
• 주장하지 않는 바: 저자들은 내보낸 SML 코드의 머신 스텝 복잡도를 검증하거나, 모든 그래프 또는 모든 실행에 대한 보편적 경계를 주장하지 않는다. 이들은 점근적 경계가 특정 패밀리의 최소 비용 실행을 제한하는 것임을 명시하며, 보편적 경계는 이 패밀리에 대해 거짓임을 밝힌다.
• 방법론적 기여: 본 논문은 "비공허성(non-vacuity)"을 기계화된 복잡도 이론의 제1급 증명 의무로 강조한다. 이는 점근적 정리가 입력 패밀리가 유계이거나 실행이 존재하지 않을 경우 논리적으로는 타당하더라도 공허할 수 있음을 보여준다. "비공허성 원장"(성장성, 실행 존재성, 체계 실현 증명)은 향후 재귀적 복잡도 논증의 정식화를 위한 재사용 가능한 템플릿으로 제시된다.