Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound

기술 요약: 최소 코헨-슈펙터(Kochen–Specker) 경계의 기하학적 절반에 대한 기계 검증 인증서

문제 정의

최소 코헨-슈펙터(KS) 문제는 $\mathbb{R}^3$ 내의 0이 아닌 벡터 $n$개의 최소 개수를 찾는 문제이다. 이때 각 벡터는 광선(ray)으로서 서로 구별되어야 하며, 이들의 직교 그래프는 모든 직교 쌍이 최대 하나의 1을 포함하고 모든 직교 삼조(triad)가 정확히 하나의 1을 포함하는 $\{0, 1\}$-채색(coloring)을 허용하지 않아야 한다. 현재 알려진 최선의 하한선은 $n \ge 24$이며, 이는 Li 등과 Kirchweger 등에 의해 계산적으로 확립되었다.

이 증명은 두 부분으로 구성된다:

1. 조합론적 절반(Combinatorial Half): 차수(order) 23까지의 후보 그래프들에 대한 동형 불변(isomorph-free) SAT 열거. 불만족(Unsatisfiability) 결과에는 독립적으로 검증 가능한 DRAT 증명이 수반된다.
2. 기하학적 절반(Geometric Half): 열거된 모든 후보 그래프가 $\mathbb{R}^3$에 임베딩될 수 없음을 입증한다. 이 부분은 Z3의 비선형 실수 산술(NRA) 솔버에 의존하여, 0이 아닌 광선 구별 벡터의 할당이 직교 제약 조건을 만족할 수 없음을 결정한다.

본 연구에서 식별된 결정적인 간극은 기하학적 절반이 검증 가능한 증명 객체를 생성하지 못한다는 점이다. 신뢰 체인은 $\exists\mathbb{R}$-hard 이론에 대한 Z3의 결정 절차에서 종료되며, 이로 인해 커뮤니티는 비임베딩 판정을 신념(faith)에 의존하여 수용해야 한다. 또한, 공개된 파이프라인은 Z3로부터 유도되었으나 검증되지 않은 최소 비임베딩 부분 그래프의 "차단 데이터베이스(blocking databases)"에 의존한다.

방법론

저자들은 실수의 비임베딩에 대한 정확한 유리수 케이스 트리(exact rational case-tree) 인증서를 생성하고 검증하기 위한 프레임워크를 도입한다. 이 방법론은 불투명한 Z3 결정 절차를 투명한 대수적 검증 과정으로 대체한다.

1. 인증서 구조
인증서는 다음을 포함하는 독립적인 객체이다:

• 앵커 및 전파(Anchor and Propagation): 정규화 단계(직교 삼조 또는 에지를 앵커링)와, 외적(cross-product) 및 평면 매개변수화를 사용하여 몇 개의 파라미터로 모든 정점 벡터를 표현하는 전파 스케줄로 구성된다.
• 케이스 트리(Case Tree): 내부 노드가 다음을 기준으로 분기되는 트리 구조이다:
  • 인수분해(Factorization): 전개를 통해 검증되는 $p = \prod f_k$.
  • 제곱합(Sum-of-Squares, SOS): $c_k \in \mathbb{Q}_{>0}$인 $p = \sum c_k m_k^2$ 형태이며, 전개를 통해 검증된다.
• 리프(Leaves): 다음 네 가지 메커니즘 중 하나에 의해 브랜치가 닫힌다:
  • 단사 충돌(Injectivity Collision): 두 개의 서로 다른 정점이 평행한 광선으로 매핑됨을 증명.
  • 의무 붕괴(Obligation Collapse): 요구되는 0이 아닌 다항식이 항등적으로 0임을 보임.
  • 이데알 멤버십(Ideal Membership): 다항식이 제약 조건에 의해 생성된 이데알에 속함을 증명하는 명시적 코팩터(cofactor).
  • 포지티벨슈테사츠(Positivstellensatz) 형태의 양의 성질: 양의 항들의 합(단사 다항식)이 제곱합의 합과 같음을 보여 실점(real points)에서 모순을 이끌어내는 일반화된 논증.

2. 검증 아키텍처
시스템은 인증서 생성기와 코드를 공유하지 않는 두 개의 독립적인 검사기를 사용한다:

• Pure-Python 리플레이: 정확한 유리수 산술을 사용하여 인증서 로직을 실행한다.
• Lean 4 전체 검사기: Lean 4 증명 보조기에 구현된 반사적 함수 Cert.check.
  • 커널 가산성(Kernel-Reducibility): 판정이 닫힌 커널 정리임을 보장하기 위해, 저자들은 gcd-free 유리수 산술 계층(KRat)과 fuel-structural 재귀를 구현하였다. 이를 통해 전체 계산을 네이티브 감소나 커스텀 공리 없이 Lean 커널에 의해 축소할 수 있다.
  • 공리 폐쇄성(Axiom Closure): 건전성 정리는 검증되지 않은 네이티브 감소를 피하고 오직 {propext, Classical.choice, Quot.sound}에만 의존한다.

3. 건전성 정리(Soundness Theorem)
핵심 정리인 check_sound는 check c = true이면 그래프의 실현(realization)이 존재하지 않음을 명시한다. 실현은 0이 아닌 벡터, 에지 상의 직교성, 그리고 모든 정점 쌍에 대한 쌍별 광선 구별성(단사성)을 만족하는 $\mathbb{R}^3$로의 사상으로 정의된다.

주요 기여

1. 정확한 유리수 인증서: 수치적 근사와 불투명한 솔버를 정확한 유리수 산술, 다항식 인수분해, SOS 분해로 대체하는 인증서 형식을 도입하였다.
2. 차단 데이터베이스의 완전한 커버리지: 공개된 PhysicsCheck 차단 리스트(차수 10–13)의 모든 291개 소스 라인(180개 고유 그래프)을 검증하여, 모든 Z3 판정을 기계 검증된 정리로 대체하였다.
3. 이중 독립 리플레이: 두 개의 서로 다른 검사기(Python 및 Lean)를 통한 검증을 통해, 115개의 적대적 변이(예: 조작된 계수, 누락된 브랜치)를 거부하고 진정한 인증서는 수용함을 입증하였다.
4. 정형화 기반의 발견: 엄격한 정형화 과정은 기존 파이프라인의 구체적인 문제점들을 드러냈다:
   • 단사성의 핵심 역할: 기존 Z3 인코딩은 인접한 쌍뿐만 아니라 모든 쌍에 대해 쌍별 광선 구별성을 강제했다. 데이터베이스 내의 여러 그래프는 표준 기하학 솔버로는 보이지 않는 이 단사성 제약 때문에 비임베딩된다.
   • 숨겨진 WLOG 케이스: 기존 파이프라인에서 사용된 직교 평면 매개변수화는 단사성 논증에 의해 명시적으로 해소되어야 하는 퇴화 케이스(평행 벡터)를 은닉하고 있었다.
   • 경험적 최적화: 기존 파이프라인의 "비채색성(non-colorability)" 최적화는 핵심적인 보조정리가 아니라 경험적인 것으로 밝혀졌다.
   • 재현 가능한 수치: 최종 차수-23 후보의 공개된 수치(41개)는 아티팩트로부터 재현할 수 없었으나, 실제 정답은 43개이며, 42개는 새로운 차수-13 인증서에 의해 해소되었다.

결과

• 검증 커버리지: 차단 데이터베이스의 180개 고유 그래프 모두가 이제 비임베딩을 증명하는 닫힌 커널 정리를 갖는다.
• 성능: 표준 노트북에서 차수 10/11/12 그래프의 커널 평가 비용은 약 0.5초, 차수 13 그래프는 1.8초이다. 전체 검증 스위트는 몇 분 내에 실행된다.
• 경계에 미치는 영향: 7개의 새로운 차수-13 인증서는 검증된 부분 그래프 단조성(monotonicity)을 통해 차수-22/23 열거의 최종 후보 44개 중 42개를 해소한다. 나머지 2개의 후보는 명시적인 기계 판독 가능 의무(obligation)로 추적된다.
• 적대적 견고성: 두 검사기 모두 지속적 통합(CI) 과정에서 115개의 변이된 인증서를 성공적으로 거부함으로써, 검증 로직이 단순히 생성기의 출력을 재현하는 것이 아니라 진정한 독립적 검사임을 입증하였다.

의의

본 논문은 차단 데이터베이스와 관련하여 최소 KS 경계의 기하학적 절반에 대한 신뢰 간극을 메운다고 주장한다. 검증되지 않은 Z3 판정을 닫힌 커널 정리로 변환함으로써, 본 연구는 핵심 부분 그래프의 비임베딩이 더 이상 블랙박스 솔버에 대한 신념의 문제가 아님을 보장한다.

저자들은 정형화 과정 자체가 숨겨진 가정(단사성), 숨겨진 케이스 의무, 그리고 기존 워크플로우에서는 보이지 않았던 데이터 불일치를 드러내는 주요 가치 창출원이었음을 강조한다. 비록 본 논문이 (SAT 열거 및 정형성 증명의 규모로 인해) $n \ge 24$에 대한 완전히 검증된 엔드-투-엔드 정리를 아직 구성하지는 못했지만, 검증된 기하학적 토대를 구축하고 확장 가능한 경로를 제시하였다. 본 연구는 양자 기초론의 복잡한 기하학적 추론이 정확한 산술과 최소한의 공리만으로 완전히 기계 검증 가능하게 만들어질 수 있음을 보여준다.