유한 Kripke 의미론에서의 유계 불식별성(Bounded Indistinguishability)에 대한 GPU 가속 검색 및 인증

우리는 양상 논리식(modal formulas)에 대한 명시적인 검색 및 인증 문제로서 유한 Kripke 의미론(finite Kripke semantics)을 연구합니다. 세계(worlds)의 집합은 정수 비트마스크(integer bitmasks)로 인코딩되므로, 불리언 연결사(Boolean connectives), $\Box$, 그리고 $\Diamond$는 단어 수준의 포함(containment) 및 교집합(intersection) 테스트로 축소됩니다. 이를 통해 독립적인 인증 검사기(certificate checker)를 갖춘 결정론적 평가기(deterministic evaluator)를 제공하며, 이후 소규모 프레임(small-frame)의 전수 스캔을 위해 융합된 CUDA 커널(fused CUDA kernel)을 통해 확장합니다. $K, T, S4, S5$에 대해, 5,624개의 논리식 코퍼스를 5개 세계까지의 모든 프레임에서 평가하였으며, 단 한 대의 H100에서 45분 동안 $1.63\times 10^{14}$번의 논리식 평가를 수행했습니다. 생성된 20,990개의 반례 모델(countermodel) 인증서는 모두 검증되었습니다. 이 유계 코퍼스(bounded corpus) 내에서, 모든 $K$-반박 가능한(K-refutable) 논리식은 최대 2개의 세계에서 반례 모델을 가지며, 이는 표준 여과 경계(filtration bound)인 $2^{|\mathrm{Sub}(\varphi)|}$보다 훨씬 낮습니다. 그런 다음 우리는 쌍별 논리식 동치성(pairwise formula equivalence)을 쌍조건문(biconditionals)에 대한 최소 반례 모델 문제로 전환하고, 의미론적 신기루(semantic mirages)를 합성합니다. 즉, 유한한 크기까지의 모든 모델에서는 일치하지만 나중에 분리되는 논리식들입니다. 특히, $\alpha_2=(\Box\Diamond)^2\top$와 $\alpha_3=(\Box\Diamond)^3\top$는 최대 5개의 세계를 가진 모든 프레임에서 일치하지만, 검증된 6개 세계 경로에 의해 분리됩니다. 마지막으로, 우리는 표현 가이드형 후보 검색(representation-guided candidate retrieval)을 위한 밀도 집계 의미론적 아틀라스(density-aggregated semantic atlas)를 구축하고, 공통된 백만 쌍 검증기 예산 하에서 원시 특징(raw features), PCA, UMAP, 스펙트럼 레이아웃(spectral layouts), 그리고 랜덤 레이아웃을 비교합니다. 그 결과는 양상 유한 모델 이론(modal finite-model theory), GPU 열거(enumeration), 인증 검사(certificate checking), 그리고 그래픽 지원 의미론적 탐색 사이의 재현 가능한 가교를 제공합니다.