Revisiting average case complexity of multilevel syllogistic: From the 1995 Courant Technical Report to Lean 4 Formalization

기술 요약: 다층 술어 논리(Multilevel Syllogistic)의 평균 사례 복잡도 재고

문제 정의
본 연구는 Cox, Ericson, Mishra의 1995년 Courant 기술 보고서 TR1995-711, "다층 술어 논리의 평균 사례 복잡도(The average case complexity of multilevel syllogistic)"를 재고한다. 원본 보고서는 집합론의 결정 가능한 부분 언어들—구체적으로 다층 술어 논리(MLS)와 기본 다층 술어 논리(EMLS)—이 최악의 경우(worst case)에는 NP-완전(NP-complete)임에도 불구하고, 평균적인 경우에는 다루기 쉬운지(tractable)를 조사했다. 해당 보고서는 이러한 문제들이 **NP-평균 완전(NP-average complete)**하다고 주장했으며, 이는 단순하고 순위 매길 수 있는 확률 분포 하에서, NEXP와 EXP 클래스가 붕괴하지 않는 한 효율적인 평균 사례 알고리즘이 존재할 수 없음을 의미한다.

원래의 보고서는 수학적 증명을 제공했으나, 기계 검증(machine-checked verification)은 결여되어 있었다. 또한, 자동 정리 증명(automated theorem proving) 분야는 이후 집합론적 파편에 대한 경험적 벤치마크나 SMT 솔버 쪽으로 중심축을 옮겼다. 본 논문은 현대적 형식 검증 표준과 원본 이론적 주장 사이의 간극을 메우기 위해, 보고서의 논리, 정의 및 정리를 Lean 4로 재구현함으로써 이 문제를 해결한다.

방법론
저자들은 엄격한 "증명 프로그램" 전략을 채택하며, 최종 정의에서 sorry(증명되지 않은 가정)의 사용을 피하고 정리보다 형식적 정의를 우선시한다. 개발은 다섯 단계로 구성된다:

1. 인프라 (단계 0): Lake 프로젝트 및 Lean 환경 설정.
2. 평균 사례 복잡도(AvCom) 어휘 (단계 1): Reischuk–Schindelhauer(1993) 프레임워크와 Levin(1986)의 평균 사례 복잡도 정의를 형식화한다. 여기에는 다음이 포함된다:
   • 분포(Distributions): 비트 문자열에 대한 유한 지지(finite-support) 확률 분포.
   • 순위 함수(Rank Functions): 주어진 입력보다 확률이 크거나 같은 입력을 세는 함수.
   • 복잡도 클래스: RS93 순위 합 부등식을 사용하여 AvP(평균 다항 시간), distNP(분포적 NP), AvDTime(평균 결정론적 시간)을 정의한다.
   • 축약(Reductions): 평균 사례의 다루기 쉬움을 보존하기 위한 지배 조건(domination condition)을 갖춘 분포적 축약을 형식화한다.
3. MLS 임베딩 (단계 2): MLS 및 EMLS의 구문(syntax)과 의미론(semantics)을 깊이 있게 임베딩한다.
   • 구문: 항(변수, 합집합, 교집합, 차집합), 관계(멤버십, 등가), 그리고 공식에 대한 귀납적 정의.
   • 의미론: 비계산적 평가 함수를 가진 공리적 ZF 집합론 의미론(ZFSet).
   • 결정 절차: Ferro–Omodeo–Schwartz(1980)에 기반한 부분적 결정 절차를 구현한다. 저자들은 멤버십이 없는 파편(fragment)에 대해 **건전성(soundness)**과 **부분적 완전성(partial completeness)**을 증명하는 한편, 전체 완전성(Step 1 치환 및 전체 Step 4 모델 탐색 필요)은 미해결 상태로 남겨둔다.
4. 직렬화 및 NP 멤버십 (단계 3): MLS 공식의 이진 인코딩을 정의하고, 인증서 기반 검증기를 통해 만족 가능성 문제(SatMLS)가 NP에 속함을 증명한다.
5. 난해도 및 완전성 (단계 4–5):
   • 축약: Bounded Halting(NBH)에서 SatMLS로의 분포적 축약을 구성한다. TM-to-MLS 번역의 복잡성 때문에, 일반적인 축약 맵은 공리화(nbhToMlsMap)되었으며, 특정 지지 분포에 대해 지배 조건을 검증한다.
   • 완전성: 모든 distNP 문제가 NBH로 축약된다는 공리를 조건으로, SatMLS가 NP-평균 완전함을 증명한다.
   • 난해도 코롤러리(Hardness Corollaries): 확립된 완전성과 붕괴 가설을 사용하여, SatMLS가 NEXP = EXP가 아닌 한 AvP에 속하지 않음을 도출한다.

주요 기여

• TR1995-711의 형식화: MLS 및 EMLS에 대한 평균 사례 복잡도 결과에 대한 최초의 기계 검증된 형식화.
• AvCom을 위한 Lean 4 라이브러리: Reischuk–Schindelhauer 클래스, 분포적 축약, 그리고 순위 매길 수 있는 분포를 구현한 맞춤형 라이브러리(AvgCaseMls)를 구축하여, 현재 최악의 경우 복잡도에 집중하고 있는 Mathlib4 생태계의 공백을 메움.
• 건전성 및 부분 완전성의 검증: 구현된 결정 절차가 멤버십 리터럴이 없는 특정 MLS 파편에 대해 건전하고 완전함을 엄격하게 증로 증명함.
• 공리적 투명성: 저자들은 "forks"(설계 선택)와 공리(예: 일반적인 TM-to-MLS 축약 맵, NEXP ≠ EXP 가설)를 DEFINITION_FORKS.md에 명시적으로 기록하여, 증명된 정리와 필요한 스캐폴딩(scaffolding)을 구분한다.

결과
논문은 단계별 계획에 대해 다음과 같은 결과를 보고한다:

• 단계 1A–1D (AvCom 정의): 모든 정의가 sorry 없이 컴파일된다. 입력, 분포, 순위 함수 및 복잡도 클래스의 형식화는 문헌과 일치한다.
• 단계 2A–2D (MLS 및 결정): 구문, 의미론 및 부분적 결정 절차가 검증된다. 건전성은 증명되었으나, 완전성은 멤버십이 없는 파편에 대해서만 증명되었다.
• 단계 3A–3B (인코딩): 인코딩 크기에 대한 다항식 경계와 검사기(checker)의 NP 멤버십이 검증된다.
• 단계 4A–4C (축약 및 완전성): 공리화된 일반 번역 맵을 제외하고 NBH에서 SatMLS로의 축약이 검증된다. SatMLS의 NP-평균 완전성은 모든 distNP 문제가 NBH로 축약된다는 공리를 전제로 증명된다.
• 단계 5A–5B (난해도): NEXP ≠ EXP 공리에 근거하여 SatMLS의 조건부 비-AvP 난해도가 도출된다.

의의 및 주장
본 논문은 실질적인 소프트웨어 엔지니어링을 변화시키는 방식으로 MLS의 평균 사례 복잡도를 "해결"했다고 주장하는 것이 아니다. 대신, 그 의의는 역사적 및 방법론적이다:

1. 이론의 생존력: 1995년 보고서의 수학적 주장이 현대적 증명 보조 도구와 접촉했을 때 살아남는지 테스트한다. 결과는 특정 구조적 공리(예: NBH로의 보편적 축약의 존재)가 수용된다면 핵심 논리가 유지됨을 나타낸다.
2. 가정의 명확화: 작업을 형식화함으로써, 저자들은 난해도 결과를 위한 NEXP ≠ EXP 가설에 대한 의존성이나 특정 분포적 축약 특성의 필요성과 같은 원본 증명의 정확한 의존성을 드러낸다.
3. 미래 연구를 위한 토대: 본 논문은 AvCom을 MLS 결정 절차에 적용하는 작업이 1990년대 이후 SMT 솔버에 밀려 상당 부분 중단되었지만, 여기서 개발된 형식적 프레임워크가 Lean 생태계 내에서 평활 분석(smoothed analysis)이나 양자 내성 암호(post-quantum cryptography)와 같은 다른 영역의 평균 사례 분석을 재방문하기 위한 필수적인 인프라를 제공한다고 주장한다.

저자들은 sorry나 공리를 성공으로 취급하지 않음을 명시적으로 밝힌다. 대신, 그것들은 향후 작업을 위한 티켓을 가진 "일시적인 스캐폴딩" 역할을 한다. 논문은 1995년 보고서가 검증 문제의 다루기 쉬움을 특징짓기 위해 평균 사례 복잡성을 사용하고자 했던 비전이, 비록 실질적인 구현 경로는 바뀌었을지라도 수학적으로 여전히 일관성이 있다는 결론을 내린다.