GPU 추론: 고정점을 배치로

📍 현재 위치: IV부 · 규모와 시스템 — 10장. 구체화 대 재작성은 폐쇄를 저장하는 쪽과 질의를 재작성하는 쪽을 저울질했습니다. 이 장은 구체화 차선을 택해, 고정점이 행렬 대수가 될 때 폐쇄 자체를 얼마나 빨리 지을 수 있는지를 묻습니다.

4권에는 기억해 둘 만한 순간이 하나 있었습니다: Neural-LP 장에서 하나의 혼 사슬 규칙(Horn chain rule)이 관계 인접 행렬 위의 행렬 곱이 되었고, 그리하여 논리의 한 조각이 신경망과 똑같은 하드웨어 위에서 돌아갔습니다. 그 시연은 가능한 가장 다루기 쉬운 규칙, 곧 하나의 이항 관계를 다른 이항 관계와 합성한 것을 골라잡은 것이었습니다. 진짜 추론 계산법은 더 지저분합니다: 2권의 EL 완성은 서로 다른 두 자료 구조(개념 레이블과 역할 엣지)를 유지하고, 둘 다를 읽고 쓰는 여섯 가지 규칙 모양을 발동시키며, 고정된 홉 수가 아니라 정확한 고정점까지 실행되어야 합니다. 이 장은 그 텐서화가 이 업그레이드에서도 살아남음을 보여 줍니다. 컴패니언 모듈 gpu_fixpoint.py는 완성 계산법 전체를 불 행렬 대수로 다시 표현하고, 포화될 때까지 반복하며, 그런 다음 이 권이 고집하는 어떤 일을 합니다: 그것은 실제 학계 TBox와 세 개의 시드가 부여된 합성 TBox 위에서, 자신이 벡터화하는 바로 그 오라클인 2권 자신의 추론기에 맞서 칸 하나하나까지의 동등성을 단언합니다. 아무것도 학습되지 않고 아무것도 근사되지 않습니다; 이득은 순전히 아키텍처적입니다. 행렬 안에 사는 상태는 행렬 전체 연산으로 갱신될 수 있고, 실전 데이터로그 엔진처럼 델타로 걸러질 수 있으며, 백 개의 온톨로지 깊이로 쌓여 한 번의 패스가 그것들을 전부 닫을 수 있습니다. 이 장은 이 분야가 계속 다다르는 그 지점에서 끝납니다: 정확한 배치 추론과, 추론기를 흉내 내도록 훈련되어 더 빠르지만 건전성을 대가로 치르는 신경망 사이의, 측정되고 출처가 밝혀진 대조입니다.

쉽게 말하면

스카프를 한 코 한 코 뜨개질하는 것과 베틀로 짜는 것을 상상해 보십시오. 뜨개질하는 손은 한 번에 한 코씩 찾아가며, 이웃한 코들을 살펴 다음에 무엇을 할지 정합니다: 이것이 바로 2권의 추론기이며, 사실에서 사실로 포인터를 쫓아갑니다. 베틀은 다르게 작동합니다: 무늬는 바디(harness)에 한 번 설정되고, 그런 다음 바디를 한 번 당기면 그 무늬가 전체 가로줄의 모든 실에 동시에 적용됩니다. 같은 천, 같은 무늬지만, 근본적으로 다른 동작입니다. 이 장은 완성 규칙들을 베틀 당기기로 다시 짜 맞춥니다: 각 규칙은 한 번에 어디서나 발동하는 하나의 행렬 연산이 되고, 모든 규칙의 한 차례 완전한 순회는 뜨개질 한 줄이 됩니다. 두 가지 개선이 이 그림을 완성합니다. 첫째, 신중한 직조공은 바뀌지 않은 줄을 다시 짜지 않고, 오직 새로운 최전선만을 짭니다(이것이 델타 요령입니다). 둘째, 거의 같은 무늬로 백 벌의 스카프를 짜야 한다면, 백 벌 모두를 한꺼번에 베틀에 실을 걸어 같은 당기기로 짤 수 있습니다(이것이 배치화이며, 그래픽 하드웨어가 빠른 근본 이유가 전부 여기에 있습니다). 베틀이 결코 하지 않는 단 한 가지는 천을 바꾸는 것입니다: 모든 스카프는 손으로 뜬 원본에 맞서 실 한 올 한 올까지 검사됩니다.

이 장에서 다루는 내용

행렬로서의 상태: 완성 알고리즘의 포섭자 집합과 역할 엣지가 어떻게 하나의 불 레이블 행렬 $S$ 와 역할마다 하나씩인 인접 행렬이 되는지, 모든 연산에 앞서 모든 색인이 어떻게 해독되는지, 그리고 불 곱셈 밑에 깔린 float32 요령이 왜 근사가 아니라 정확한지.
모든 규칙이 하나의 곱으로: 각 완성 규칙을 그 행렬 형태로 유도한 다음 커밋된 코드에서 그대로 인용합니다. CR1은 레이블-폐쇄 곱으로, CR2는 gather-후-조인으로, CR3은 외적 방출로, CR4는 이단계 조인으로, 바닥 규칙은 행렬-벡터 곱으로, 역할 사슬은 그래프 합성으로 각각 나타납니다; 그 대수가 왜 OR-AND 불 반환(semiring)인지, 그리고 멱등성이 어디에서 조용히 제 몫을 하는지도 다룹니다.
오라클 표준: 실제 14개 공리 TBox와 세 개의 시드가 부여된 합성 TBox 위에서 el_completion.classify와의 정확한 포섭-집합 동등성, 그대로 인용된 assert들, 그리고 시험용 온톨로지 하나만으로는 규칙-커버리지 공백이 숨을 수 있는 이유 때문에 합성 교차 검사가 왜 중요한지.
준순진 델타: 실전 엔진의 규율을 행렬 항으로 되짚어 유도하며, 커밋된 연산 횟수(순진 방식으로는 71번의 도출 사건, 델타를 쓰면 28번)와, 1권의 고정점 장으로 곧장 이어지는 파동 전선 그림을 함께 다룹니다.
GPU 논지로서의 배치화: 배치 위에 파이썬 루프를 두지 않고 하나의 쌓인 텐서 패스로 백 개의 TBox 변형을 닫는 과정, CPU 프록시라고 정직하게 이름 붙인 커밋된 루프-대-스택 타이밍 표, 그리고 실전 시스템이 그 위에 더 얹는 것들(작업 목록, 희소 커널, 128코어 구체화)까지.
정직한 장부: 조밀한 불 행렬이 볼 수 없는 것(제곱으로 자라는 메모리, 사라지는 유래, 새 연산자가 필요한 규칙 모양들)과, F1을 자릿수 단위로 사들이는 신경망-모방 대안이 건전성을 무엇과 맞바꾸는지, 즉 이 권이 정확한 차선에서는 계속 거부하는 그 거래.

하나의 사슬 규칙에서 계산법 전체로

무엇을 표현해야 하는지부터 되짚어 봅시다. 2권의 완성 알고리즘은 개념 이름들의 유한한 전체 집합 위에서 두 구조를 포화시킵니다: $S(A)$ 는 $A$ 를 레이블하는 개념들의 집합이고(" $B$ 가 $A$ 를 레이블한다"는 것을, 도출된 포섭 관계 $A \sqsubseteq B$ 로 읽으십시오), $R(r)$ 는 도출된 역할 엣지 $(A, B)$ 들의 집합으로, $A$ 의 모든 인스턴스가 $B$ 안에 $r$ -후속자를 가진다는 뜻입니다. 이 규칙들은 EL 계열의 고전적인 귀결-기반(consequence-based) 계산법이며, 이 계보는 SNOMED CT의 379,691개 개념을 최초로 분류했고 2006년에는 그 일을 1,782초 만에 해냈는데, 이는 완주에 성공한 유일한 태블로 추론기(FaCT++, 3,859초)보다 대략 두 배 빠른 것이었고 나머지 두 태블로 추론기는 메모리 부족으로 멈췄으며 [1], 이후 동시(concurrent) 작업 목록 큐로 현대화되어 같은 포화를 몇 초 안으로 끌어내렸습니다 [2]. 2권의 el_completion.py는 그 계산법을 순진한(naive) 방식으로 축소하여 구현합니다: 파이썬 집합, 소속 검사, changed 플래그입니다(el_completion.py 177–261행). 이것이 아래의 모든 것에 대한 오라클이며, 그 규칙 집합을 여기 눈앞에 두고 볼 가치가 있습니다. 읽기 전에 그 안의 기호들부터 해독해 둡시다: ⊓는 개념 논리곱이고( $A_1 \sqcap A_2$ 는 $A_1$ 이면서 동시에 $A_2$ 인 것들의 개념입니다), $\exists r.B$ 는 $B$ 안에 $r$ -후속자를 적어도 하나 가진 것들의 개념이며, $r \circ s$ 는 역할 합성( $r$ -엣지 다음에 $s$ -엣지)이고, ⊥는 "바닥"이라고 읽으며 아무것도 충족할 수 없는 불가능한 개념이고, ⟹는 "그러면 더하라"라고 읽습니다(el_completion.py 25–30행):

CR1  A' ∈ S(A),  A' ⊑ B          ⟹  add B to S(A)
CR2  A₁,A₂ ∈ S(A),  A₁ ⊓ A₂ ⊑ B  ⟹  add B to S(A)
CR3  A' ∈ S(A),  A' ⊑ ∃r.B       ⟹  add (A, B) to R(r)
CR4  (A,B) ∈ R(r),  B' ∈ S(B),  ∃r.B' ⊑ C  ⟹  add C to S(A)
CR⊥  (A,B) ∈ R(r),  ⊥ ∈ S(B)     ⟹  add ⊥ to S(A)   (the bottom rule)
CRχ  (A,B) ∈ R(r),  (B,C) ∈ R(s),  r ∘ s ⊑ t  ⟹  add (A,C) to R(t)

행렬화(matrixization)는 자료 구조의 변경일 뿐, 그 이상은 아닙니다. 개념 이름들의 전체 집합을 오라클이 고정하는 것과 정확히 똑같이 고정하고(정규화된 공리에 나타나는 모든 이름에, "꼭대기"라고 읽으며 모든 것을 담는 개념인 ⊤와 바닥 개념 ⊥를 더한 것), 결정론을 위해 정렬한 다음, 그 크기, 즉 개념 이름의 개수를 $n$ 으로 표기합니다. 각 이름에 $0$ 부터 $n-1$ 까지의 정수 색인을 하나씩 배정합니다. 그러면:

레이블 상태는 하나의 불 행렬 $S \in \lbrace 0,1 \rbrace^{n \times n}$ (참/거짓 칸으로 이루어진 $n$ 행 $n$ 열 격자)이 되며, $B \in S(A)$ 일 때, 즉 $A \sqsubseteq B$ 가 도출되었을 때 정확히 $S[A, B] = 1$ 입니다;
각 역할 $r$ 은 인접 행렬 $R_r \in \lbrace 0,1 \rbrace^{n \times n}$ 이 되며, $(A, B) \in R(r)$ 일 때 정확히 $R_r[A, B] = 1$ 입니다;
공리 자체는 불 표가 됩니다: TBox가 $A' \sqsubseteq B$ 를 명시할 때의 $H_1[A', B] = 1$ , TBox가 $A' \sqsubseteq \exists r.B$ 를 명시할 때 역할마다 하나씩인 존재-방출 표 $E^3_r[A', B] = 1$ , TBox가 $\exists r.B' \sqsubseteq C$ 를 명시할 때 역할마다 하나씩인 발동 표 $E^4_r[B', C] = 1$ , 그리고 논리곱 공리를 위한 색인 배열과 투영 행렬로, 이는 아래 CR2에서 함께 설명됩니다(gpu_fixpoint.py 86–137행).

초기화는 오라클의 $S(A) = \lbrace A, \top \rbrace$ 를 그대로 반영합니다: $S$ 의 대각선이 참으로 설정되고(모든 개념은 자기 자신을 레이블합니다) ⊤ 열이 참으로 설정되며(모든 것은 ⊤에 포섭됩니다), 모든 $R_r$ 은 전부 거짓으로 시작합니다(gpu_fixpoint.py 140–148행). 실행 예제 위에서 커밋된 실행은 전체 설정을 다음과 같이 보고합니다:

[1] matrixization of the normalized academic TBox
    14 axioms → 16 normal forms; universe n = 12 (8 named + 2 fresh + ⊤ + ⊥); roles: advises, authored, grandAdvisor
    S: 12×12 bool (S[A,B] = "A ⊑ B"); one 12×12 adjacency R_r per role
    axiom tables: H1 nnz=6, conjunctions m=2, E3 nnz=3, E4 nnz=4, chains=1

숫자들을 해독해 봅시다. 정규화(2권 자신의 elc.normalize를 임포트한 것이며, 다시 타이핑하지 않았습니다)는 저작된 14개의 공리를 16개의 정규형으로 바꾸고, 복합 부분개념을 위한 새 이름 두 개를 만들어 냅니다; 선언된 열 개의 개념 중 TBox에 실제로 나타나는 것은 여덟 개뿐이므로, 전체 집합은 $n = 12$ 입니다: 이름 붙은 개념 여덟 개, 새 이름 두 개, ⊤와 ⊥입니다. 세 개의 역할이 등장합니다: 공리에서 나온 advises와 authored, 그리고 사슬의 목표로만 나타나는 grandAdvisor입니다. 약어 nnz는 0이 아닌 항목의 개수를 뜻하는 표준적인 희소 행렬 용어입니다: $H_1$ 은 여섯 개의 알려진 포섭 관계를 싣고, 두 개의 논리곱 공리는 CR2를 위한 표를 채우며, 하나의 사슬 공리(advises ∘ advises ⊑ grandAdvisor)가 CRχ에 공급됩니다.

모든 것을 움직이는 연산은 하나입니다: 여기서 $\odot$ 로 쓰는 불 행렬 곱(boolean matrix product)입니다. 보통의 행렬 곱이 숫자들의 곱을 합하는 곳에서, 불 곱은 비트들의 AND를 OR로 묶습니다. 행렬 $X$ 와 $Y$ 에 대해, 임의의 행 색인 $i$ 와 열 색인 $j$ 에 대해, $k$ 가 $n$ 개의 내부 위치 전체에 걸칠 때,

(X \odot Y)[i, j] \;=\; \bigvee_{k=0}^{n-1} \; X[i, k] \,\wedge\, Y[k, j],

여기서 $\bigvee_k$ 는 $k$ 의 모든 값에 대한 큰 OR("적어도 하나의 $k$ 가 통하는가?")이고 $\wedge$ 는 AND입니다. 이것은 불 반환(Boolean semiring), 즉 덧셈이 OR이고 곱셈이 AND인 대수 위에서의 행렬 곱입니다. 컴패니언은 이를 의도적인 요령으로 계산합니다(gpu_fixpoint.py 73–81행):

def bmm(a: np.ndarray, b: np.ndarray) -> np.ndarray:
    """Boolean matrix product over the (∨, ∧) semiring,

        (A ⊙ B)[i, j] = ⋁_k  A[i, k] ∧ B[k, j],

    computed as a float32 BLAS matmul of 0/1 matrices followed by "> 0".
    Exact: every partial sum is an integer ≤ n ≪ 2²⁴, representable in
    float32.  Broadcasts over leading batch dimensions like np.matmul."""
    return (a.astype(np.float32) @ b.astype(np.float32)) > 0.0

정확하다는 주장은 두 줄짜리 증명을 받을 자격이 있습니다. "부동소수점"과 "정확함"이 보통 한 문장에 같이 나오지 않기 때문입니다. float32로 형변환하면 두 행렬의 모든 항목은 $0.0$ 이거나 $1.0$ 이므로, 각 항 $X[i,k] \cdot Y[k,j]$ 는 $0$ 이거나 $1$ 이고, 보통의 행렬 곱은 정수 $c = \sum_k X[i,k]\, Y[k,j]$ 를 계산하는데, 이는 두 비트가 모두 켜져 있는 증인 $k$ 의 개수입니다. 그 개수는 많아야 $n$ 입니다. float32 수는 24비트 가수(significand)를 담으므로, 크기가 많아야 $2^{24} = 16{,}777{,}216$ 인 모든 정수는 정확히 표현되며, 그 한계 아래의 정수에 $1$ 을 더하는 것도 다시 정확합니다; $n = 12$ 일 때는 물론이고, $n$ 이 수백만이라도, 반올림은 결코 일어나지 않습니다. 마지막 비교 $c > 0$ 은 적어도 하나의 증인이 존재할 때 정확히 참이며, 이는 바로 AND들의 OR입니다. 이 float 경로는 불 곱의 근사가 아닙니다; 그것은 불 곱 그 자체이며, 다만 지구상의 모든 가속기가 이십 년을 들여 최적화해 온 단 하나의 커널(조밀 행렬 곱셈)을 거쳐 흐를 뿐입니다. 그 경로 배정이 바로 이 장의 논지 전체입니다.

선형대수로 다시 짜 맞춘 완성 계산법: 포화 상태는 불 행렬로, 각 규칙은 고정점까지 반복되는 하나의 마스킹되거나 합성된 행렬 곱으로, 그리고 같은 패스가 쌓아 올린 백 개의 온톨로지 변형을 한 번에 닫으며, 모든 조각이 오라클과 정확히 일치합니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

모든 규칙이 하나의 곱이 되다

규칙들을 하나씩 다뤄 봅시다; 각 규칙마다 먼저 유도를 보이고 그다음 커밋된 코드를 보입니다.

CR1, 레이블 폐쇄. 이 규칙은 다음을 말합니다: $A'$ 가 $A$ 를 레이블하고 TBox가 $A' \sqsubseteq B$ 를 명시하면, $B$ 가 $A$ 를 레이블합니다. 행 $A$ 와 목표 열 $B$ 를 고정하고, 이 규칙이 어떤 증인 $A'$ 에 대해 언제 발동하는지를 물어봅시다. 증인의 이름을 내부 색인 $k$ 로 바꾸면: 이 규칙은 $S[A, k] = 1$ (개념 $k$ 가 $A$ 를 레이블함)이고 $H_1[k, B] = 1$ (TBox가 $k \sqsubseteq B$ 라고 말함)인 $k$ 가 존재할 때 정확히 발동합니다. 유한한 색인 집합에 대한 존재는 하나의 논리합이므로,

\text{fires}(A, B) \;=\; \bigvee_{k} \; S[A, k] \wedge H_1[k, B] \;=\; (S \odot H_1)[A, B],

여기서 두 번째 등식은 그저 $\odot$ 의 정의를 거꾸로 읽은 것일 뿐입니다. 따라서 하나의 곱이 모든 쌍 $(A, B)$ 와 모든 증인 $k$ 에 대해 이 규칙을 동시에 평가합니다: 가능한 $n^3$ 개의 규칙 인스턴스 전부를 커널 호출 한 번으로 처리하는 것입니다. 상태 갱신은 포화시키는 OR-대입 $S \leftarrow S \vee (S \odot H_1)$ 이며, 코드는 한 줄에 기록 관리(bookkeeping)를 더한 것입니다(gpu_fixpoint.py 179–181행):

        # CR1: A' ∈ S(A), A' ⊑ B ⟹ B ∈ S(A)   —   S ← S ∨ S⊙H1.
        out = bmm(S, H1)
        matmuls += 1; derivations += int(out.sum()); S |= out

CR2, 논리곱 조인. 이 규칙은 공리 $A_1 \sqcap A_2 \sqsubseteq B$ 의 두 논리곱 항 모두가 $A$ 를 레이블할 것을 요구합니다. 공리는 모양이 $(m, 2)$ 인 정수 배열 $C_2$ 로 보관되는데, 여기서 $m$ 은 논리곱 공리의 개수이고 행 $m'$ 는 그 공리의 두 논리곱 항의 열 색인을 담습니다. 여기에 더해, 공리 $m'$ 의 머리가 $B$ 일 때 정확히 $P_2[m', B] = 1$ 인 투영 행렬 $P_2 \in \lbrace 0,1 \rbrace^{m \times n}$ 이 함께 있습니다. NumPy의 gather 연산 S[..., :, C2]는 모양이 $(n, m, 2)$ 인 세-색인 배열을 만드는데, $[A, m', j]$ 위치의 항목은 $S[A, \text{conjunct}_j(m')]$ 입니다; 마지막 축에 대해 .all로 축약하면 두 슬롯을 AND하여, 발동 마스크 $\text{fires}[A, m'] = S[A, A_1^{m'}] \wedge S[A, A_2^{m'}]$ 를 얻는데, 이는 "두 논리곱 항 모두가 $A$ 를 레이블한다"는 CR2의 전제를 그대로 옮긴 것입니다. 마지막 불 곱은 각 발동을 그 머리 열로 실어 나릅니다: $(\text{fires} \odot P_2)[A, B] = \bigvee_{m'} \text{fires}[A, m'] \wedge P_2[m', B]$ . 데이터베이스 용어로 말하면 이는 상태와 공리 표 사이의 AND-조인이며, gather, 축약, 곱셈으로 실행됩니다(gpu_fixpoint.py 183–187행):

        # CR2: A1, A2 ∈ S(A), A1 ⊓ A2 ⊑ B ⟹ B ∈ S(A) — conjunction mask
        # (both conjunct columns true) projected onto the target columns.
        fires = S[..., :, mats["C2"]].all(axis=-1)       # (..., n, m)
        out = bmm(fires, mats["P2"])
        matmuls += 1; derivations += int(out.sum()); S |= out

CR3, 존재 방출. $A'$ 가 $A$ 를 레이블하고 TBox가 $A' \sqsubseteq \exists r.B$ 를 명시하면, 엣지 $(A, B)$ 가 $R(r)$ 에 합류합니다. 공리 표 $E^3_r$ 과 함께, CR1과 똑같은 논리합 논증이 $R_r \leftarrow R_r \vee (S \odot E^3_r)$ 를 줍니다. 이 곱을 읽는 더 물리적인 두 번째 방법이 있습니다. 어떤 불 행렬이든 그 참인 칸들의 OR이므로, $E^3_r = \bigvee_{(A', B)} \mathbf{e}_{A'} \mathbf{e}_B^{\top}$ 입니다. 여기서 $\mathbf{e}_j$ 는 $j$ 번째 표준 기저 열(위치 $j$ 의 하나만 빼고 모두 0)이고, 전치 $\top$ 은 열을 옆으로 눕혀 행으로 바꾸며(이 위 첨자는 꼭대기 개념 ⊤와 글리프만 같을 뿐, 여기서는 개념이 아니라 벡터에 작용하는 연산입니다), 외적(outer product) $\mathbf{e}_{A'} \mathbf{e}_B^{\top}$ 은 칸 $(A', B)$ 하나에만 1이 있는 행렬입니다. $\odot$ 가 $\vee$ 위에 분배되므로(이 분배법칙은 반환 공리 중 하나이며, AND가 OR 위에 분배되기 때문에 칸마다 성립합니다),

S \odot E^3_r \;=\; \bigvee_{(A', B)\,:\, A' \sqsubseteq \exists r.B} \; (S\, \mathbf{e}_{A'})\, \mathbf{e}_B^{\top},

그리고 $S \mathbf{e}_{A'}$ 는 그저 $S$ 의 $A'$ 열, 즉 현재 $A'$ 에 의해 레이블된 모든 개념의 집합입니다. 각 존재 공리는 그 열 전체를 역할 행렬의 $B$ 열에 도장 찍듯 새기며, 이는 현재 레이블들을 공리 템플릿과 교차시키는 외적 갱신입니다. 코드는 다른 표를 쓴다는 점만 다를 뿐 CR1과 같은 패턴입니다(gpu_fixpoint.py 189–192행).

CR4, 이단계 조인. 이 전제는 세 사실을 사슬로 잇습니다: 엣지 $(A, B) \in R(r)$ , 레이블 $B' \in S(B)$ , 공리 $\exists r.B' \sqsubseteq C$ 입니다. 중첩된 두 개의 존재 양화사는 두 개의 곱을 뜻합니다. 먼저 증인 $B'$ 를 소거합니다: $T = S \odot E^4_r$ 로 정의하면,

T[B, C] \;=\; \bigvee_{B'} \; S[B, B'] \wedge E^4_r[B', C],

이는 " $B$ 의 어떤 레이블이 $C$ 에 이르는 $r$ -존재 공리를 촉발한다"라고 읽습니다. 그다음 증인 $B$ 를 소거합니다: $(R_r \odot T)[A, C] = \bigvee_B R_r[A, B] \wedge T[B, C]$ 이며, 이는 " $A$ 에서 $r$ -엣지를 따라, 레이블이 $C$ 에 이르는 어떤 $B$ 까지 간다"라고 읽습니다. 첫 번째 식을 두 번째 식에 대입하면 CR4의 전제가 정확히 복원되며, 두 존재 양화사 모두가 두 개의 내부 논리합으로 실현됩니다. 그에 맞추어 코드는 스스로 두 번의 행렬 곱을 치릅니다(gpu_fixpoint.py 194–198행):

        # CR4: (A,B) ∈ R(r), B' ∈ S(B), ∃r.B' ⊑ C ⟹ C ∈ S(A)
        #   — the two-step join  S ← S ∨ R_r ⊙ (S ⊙ E4_r).
        for r, E in mats["e4"].items():
            out = bmm(R[r], bmm(S, E))
            matmuls += 2; derivations += int(out.sum()); S |= out

CR⊥, 바닥 규칙. 충족 불가능한 개념으로 들어가는 $r$ -엣지는 그 출발지를 오염시킵니다: $(A, B) \in R(r)$ 이고 $\bot \in S(B)$ 이면, $\bot \in S(A)$ 입니다. $S$ 의 ⊥ 열을 $n \times 1$ 행렬로 잘라내어 곱합니다: $(R_r \odot S[:, \bot])[A] = \bigvee_B R_r[A, B] \wedge S[B, \bot]$ 이며, 그 출력이 ⊥ 열에 OR되어 들어가는 행렬-벡터 곱입니다(gpu_fixpoint.py 200–205행). 이것이 바로 아래의 커밋된 실행에서 ⊥를 advises 엣지를 따라 거꾸로 실어 나를 규칙입니다.

CRχ, 역할 사슬. 공리 $r \circ s \sqsubseteq t$ 에 대해, 이 규칙은 엣지들을 합성합니다: $(R_r \odot R_s)[A, C] = \bigvee_B R_r[A, B] \wedge R_s[B, C]$ 이며, 어떤 $B$ 가 두-홉 경로를 완성할 때 정확히 참입니다. 사슬 공리는 문자 그대로 그래프 합성이며, 4권이 그 사슬 규칙에 사용했던 것과 같은 연산이지만, 이제 세 번째 관계로 OR됩니다: $R_t \leftarrow R_t \vee (R_r \odot R_s)$ (gpu_fixpoint.py 207–211행). 표 하나가 계산법 전체를 모아 놓습니다:

규칙	전제(오라클 형태)	행렬 형태	코드
CR1	$A' \in S(A)$ , $A' \sqsubseteq B$	$S \leftarrow S \vee (S \odot H_1)$	179–181행
CR2	$A_1, A_2 \in S(A)$ , $A_1 \sqcap A_2 \sqsubseteq B$	gather + AND, 그다음 $\vee\,(\text{fires} \odot P_2)$	183–187행
CR3	$A' \in S(A)$ , $A' \sqsubseteq \exists r.B$	$R_r \leftarrow R_r \vee (S \odot E^3_r)$	189–192행
CR4	$(A,B) \in R(r)$ , $B' \in S(B)$ , $\exists r.B' \sqsubseteq C$	$S \leftarrow S \vee \big(R_r \odot (S \odot E^4_r)\big)$	194–198행
CR⊥	$(A,B) \in R(r)$ , $\bot \in S(B)$	$S[:, \bot] \leftarrow S[:, \bot] \vee (R_r \odot S[:, \bot])$	200–205행
CRχ	$(A,B) \in R(r)$ , $(B,C) \in R(s)$ , $r \circ s \sqsubseteq t$	$R_t \leftarrow R_t \vee (R_r \odot R_s)$	207–211행

왜 불 반환인가, 그리고 왜 반드시 끝나는가. OR의 두 성질이 조용히 제 몫을 합니다. 첫째는 멱등성(idempotence), $x \vee x = x$ 입니다: 이미 알려진 사실을 다시 도출해도 아무것도 바뀌지 않으므로, 위의 OR-대입들은 매 파동마다 같은 규칙 인스턴스를 발동시켜도 상태를 손상시키지 않습니다. 같은 곱들을 계수(counting) 반환(보통의 $+$ 와 $\times$ ) 위에서 돌린다면, 각 칸은 대신 도출 경로의 개수를 셀 것입니다; 반복하면 TBox에 순환이 있을 때마다 그 개수는 한없이 자라나고, 그 반복에는 값의 고정점이 없고 오직 지지 집합의 고정점만 있게 됩니다. 포화는 "이미 알려짐"이 흡수적인 대수를 원하며, OR이 정확히 그렇습니다. 두 번째 성질은 단조성(monotonicity)입니다: 모든 갱신은 칸을 켜기만 할 뿐 결코 끄지 않으므로, 상태들의 수열은 불 행렬의 유한한 격자, 즉 $S$ 에 대한 $\lbrace 0,1 \rbrace^{n \times n}$ 과 역할마다 하나씩 더한 것 안에서 하나의 상승 사슬을 이룹니다. 그곳에서 엄밀하게 상승하는 사슬의 길이는 많아야 전체 칸의 개수, 즉 $n^2 (1 + \lvert \text{roles} \rvert)$ (여기서 $\lvert \text{roles} \rvert$ 는 역할 이름의 개수이며, 세로 막대는 "집합의 크기"라고 읽습니다)이므로, 어떤 파동은 반드시 아무것도 바꾸지 못하게 되고, 루프는 파동 전후의 전체 참-칸 개수를 비교함으로써 정확히 그것을 감지합니다(gpu_fixpoint.py 213–216행). 이것은 1권의 클레이니 등반을 그대로 옮긴 것, 곧 유한 격자 위에서 최소 고정점까지 오르는 단조 연산자입니다; 바뀐 것은 오직 각 파동을 실어 나르는 대수뿐이며, 집합 합집합에서 행렬 전체의 OR로 바뀌었을 뿐입니다.

오라클 표준: 두 번 겹친 정확함

커밋된 실행은 학계 TBox를 닫고 다음을 보고합니다:

[2] naive dense fixpoint: every rule × the FULL state, every wave
    waves=3  matmuls=33  derivations=71  →  closure |S|=39 cells, |R|=7 edges
    oracle equality: S and R match el_completion cell-for-cell; 8 named subsumptions == classify()
    unsatisfiable == oracle: ['TenuredStudent', 'TenuredStudentAdvisor']

믿기 전에 숫자들을 먼저 해독해 봅시다. 세 번의 파동이면 충분하며, 각 파동은 11번의 불 곱을 냅니다: CR1에 한 번, CR2에 한 번, 존재-방출 공리를 가진 유일한 역할(advises)에 대한 CR3 곱 한 번, 발동 공리를 실어 나르는 두 역할(advises와 authored) 각각에 대한 두-곱짜리 CR4 조인, 세 번의 바닥-규칙 곱(역할마다 하나씩), 그리고 하나의 사슬 합성입니다; 도합 $3 \times 11 = 33$ 번의 행렬 곱입니다. 초기 상태는 $S$ 에 23개의 참-칸을 가집니다(12칸짜리 대각선에 12칸짜리 ⊤ 열을 더한 것이며, ⊤ 자신에 대한 단 하나의 칸에서 겹칩니다); 폐쇄는 39개를 가지므로, 포화는 16개의 새 레이블 칸에 더해 7개의 역할 엣지를 도출했습니다. 충족 불가능한 쌍은 이 계산법이 처음부터 끝까지 작동하고 있다는 증거입니다: TenuredStudent는 CR2를 거쳐 Professor/Student 배타성(disjointness)에 의해 ⊥로 무너지고, 그런 다음 CR⊥가 ⊥를 TenuredStudentAdvisor의 advises-엣지를 가로질러 거꾸로 그 지도교수 안으로 끌고 들어갑니다.

이 장의 척추는 run()에서 다음에 일어나는 일입니다: 몇 군데 표본 검사가 아니라 모든 것에 대한 집합 동등성입니다. 행렬들은 이름-쌍 집합으로 다시 읽히고, 동일한 정규화된 공리 위에서 2권의 추론기를 새로 실행한 결과와 비교됩니다(gpu_fixpoint.py 405–408행):

    pairs, roles = matrix_sets(S_nv, R_nv, mats["names"])
    o_pairs, o_roles = oracle_sets(normalized)
    assert pairs == o_pairs, "vectorized S differs from el_completion's S"
    assert roles == o_roles, "vectorized R differs from el_completion's R"

여기서 동등성은 $S$ 의 모든 칸과 모든 $R_r$ 의 모든 칸을 뜻하며, 사소한 사실과 새 이름까지 전부 포함할 뿐, 유명한 함의들의 표본이 아닙니다. 두 번째 assert는 그런 다음 행렬로부터 딕셔너리 상태를 재구성하고, 이를 el_completion 자신의 보고 필터를 거쳐 통과시킨 뒤, 독자에게 보이는 분류 결과가 classify()와 정확히 일치할 것을, 즉 이름 붙은 여덟 개의 포섭 관계와 두 원소짜리 충족 불가능 집합을 요구합니다(gpu_fixpoint.py 412–422행). 조밀한 엔진과 포인터를 쫓는 엔진은 하나의 수학적 대상에 대한 두 개의 구현이며, assert는 둘 사이의 어떤 틈도 빌드 실패로 취급합니다.

시험용 온톨로지 하나는 여전히 시험용 온톨로지 하나일 뿐입니다. 실제 TBox는 교육을 위해 쓰였습니다: 그 표들은 작고( $H_1$ 은 여섯 항목, 논리곱 둘, 사슬 하나뿐입니다), 학계 세계가 결코 만들어 내지 않는 구성, 이를테면 사슬에 공급되는 논리곱 머리, 또는 배타성이 아니라 존재 공리를 거쳐 도달하는 ⊥ 같은 것에서만 문제를 일으키는 벡터화 버그가 있다면 그것은 그냥 통과해 버릴 것입니다. 그래서 이 모듈은 작은 시드 부여 생성기 synth_tbox를 함께 갖고 있는데, 이는 8개 개념과 2개 역할에 대한 무작위 14-공리 TBox를 시드마다 결정론적으로 내놓으며, 알려진 포섭 관계, ⊥를 머리로 갖는 논리곱, 양쪽 모두에 있는 존재 제한, 역할 사슬을 섞습니다(gpu_fixpoint.py 333–360행). 세 개의 시드가 정규화되고, 행렬화되며, 두 조밀 엔진 모두로 닫히고, 오라클에 맞서 동일한 집합-동등성 표준에 붙들어 매어집니다(gpu_fixpoint.py 428–445행):

[4] seeded synthetic TBoxes — exact oracle equality on each
    seed  axioms   n   |S|  |R|  waves  vs oracle
       1      14  10    28    0      3  exact
       2      14  10    21    2      2  exact
       3      14  10    21    3      2  exact

이 세 폐쇄는 학계 폐쇄와 유용하게도 다릅니다(시드 1은 28칸짜리 레이블 폐쇄를 도출하지만 역할 엣지는 전혀 없고, 시드 2와 3은 서로 다른 규칙 조합에서 엣지를 도출합니다), 그리고 그것이 핵심입니다: 시연용 TBox가 줄 수 없는 커버리지입니다. 이것이 사 주는 것에 대해 정직하게 말하자면: 세 개의 시드는 증명이 아니라 하나의 스모크 테스트 배터리(smoke battery)입니다. 정확성 논증은 앞 절에서 규칙별로 이루어진 유도이며, 시드들은 그 유도를 구현하는 코드를 수학과 NumPy 사이의 간극으로부터 지켜 줍니다.

준순진(semi-naive): 행렬 항으로 본 델타 규율

위의 순진한 루프는 매 파동마다 전체 상태에 맞서 모든 규칙을 발동시킵니다. 커밋된 파동별 도출 사건 개수를 보십시오(도출 사건(derivation event)이란 어떤 규칙의 원출력 안의 참-칸 하나이며, 이미 알려진 사실의 재도출도 포함합니다): 19, 그다음 26, 그다음 26입니다. 파동 3은 26개의 사건을 도출하지만 아무것도 더하지 못합니다; 그 하나하나가 상태가 이미 가지고 있는 사실의 재도출이며, 파동 2는 이미 파동 1의 대부분을 재도출했습니다. 이것이 순진한 방식의 세금입니다: 어떤 사실이 도출 가능해지면, 고정점에 이를 때까지 그 이후의 모든 파동에서 계속 재도출됩니다. 실전 데이터로그 시스템이 병렬화하는 그 고전적인 해법, 곧 엔진 규율은 [3] 준순진 평가(semi-naive evaluation)입니다: 규칙을 오직 이전 파동에서 도출된 전제를 통해서만 발동시키고, 그 규칙의 다른 전제에 대해서는 그 델타(delta)를 전체 상태와 조인합니다.

행렬로 된 유도는 네 줄이면 됩니다. 어떤 파동에 들어가는 상태를 옛것-더하기-델타로 씁니다, $X = X_{\text{old}} \vee \Delta X$ 와 $Y = Y_{\text{old}} \vee \Delta Y$ 이며, 여기서 $\Delta X$ 는 지난 파동에서 켜진 칸들만을 정확히 담고 있습니다. $\odot$ 가 양쪽에서 $\vee$ 위에 분배되므로,

X \odot Y \;=\; (X_{\text{old}} \odot Y_{\text{old}}) \;\vee\; (\Delta X \odot Y_{\text{old}}) \;\vee\; (X_{\text{old}} \odot \Delta Y) \;\vee\; (\Delta X \odot \Delta Y).

첫 번째 항은 옛 전제만을 쓰므로, 이미 앞선 파동에서 계산되었고 그 출력도 이미 OR되어 들어가 있습니다: 이를 다시 계산하는 것은 순전한 낭비입니다. 나머지 세 항은 각각 적어도 하나의 델타 피연산자를 담고 있으며, 이들은 준순진 파동이 실제로 실행하는 두 개의 곱으로 함께 커버됩니다. 각각을 전체 상태에 맞서 전개하면 다음을 얻기 때문입니다,

\Delta X \odot Y \;=\; (\Delta X \odot Y_{\text{old}}) \vee (\Delta X \odot \Delta Y), \qquad X \odot \Delta Y \;=\; (X_{\text{old}} \odot \Delta Y) \vee (\Delta X \odot \Delta Y),

그리고 이 둘의 합집합이 정확히 세 개의 델타 항입니다. 그러므로 $\Delta X \odot Y$ 와 $X \odot \Delta Y$ 만을 발동시키면 적어도 하나의 새 전제를 가진 도출은 하나도 잃지 않으면서, 전부-옛것인 항만을 정확히 건너뜁니다. 컴패니언의 close_seminaive는 모든 규칙에 대해 이 분할을 구체화하며, 그 독스트링이 바로 공식 모음표입니다(gpu_fixpoint.py 224–240행):

        CR1   ΔS ⊙ H1                     CR3   ΔS ⊙ E3_r
        CR2   (all conjuncts ∈ S) ∧ (some conjunct ∈ ΔS), projected
        CR4   ΔR_r ⊙ (S ⊙ E4_r)  ∨  R_r ⊙ (ΔS ⊙ E4_r)
        CR⊥   ΔR_r ⊙ S[:,⊥]      ∨  R_r ⊙ ΔS[:,⊥]
        CRχ   ΔR_r ⊙ R_s         ∨  R_r ⊙ ΔR_s

CR1과 CR3은 상태 피연산자가 하나뿐이므로, 그 델타 형태는 더 작은 곱 하나입니다; CR2는 전체 논리곱 마스크는 그대로 유지하되, 추가로 델타가 어떤 논리곱 항을 건드렸을 것을 요구합니다(gpu_fixpoint.py 264–268행); 두 피연산자를 가진 세 규칙은 둘로 나뉩니다. 파동이 끝날 때, 다음 델타는 도출된 것에서 이미 알려진 것을 뺀 것, $\Delta^{i+1} = \text{new} \wedge \neg S^{i}$ 이며(여기서 위 첨자 $i$ 는 파동을 세는 수이므로, $S^{i}$ 는 행렬 거듭제곱이 아니라 파동 $i$ 이후의 상태입니다), 상태가 그것을 흡수합니다(gpu_fixpoint.py 299–305행). 델타 피연산자가 전부 거짓인 규칙은 아예 건너뜁니다. 커밋된 비교는 다음과 같습니다:

[3] semi-naive (delta) iteration — same closure, fewer derivations
    engine       waves  matmuls  derivations  per-wave derivations
    naive            3       33           71   19  26  26
    semi-naive       4       49           28    9  12   7   0
    (the delta split makes MORE, smaller products, but never fires
     on all-old premises: derivations 71 → 28, the semi-naive economy RDFox parallelizes)

두 열 모두 정직하게 읽으십시오. 행렬 곱의 개수는 33에서 49로 오히려 늘었습니다, 두 피연산자를 가진 각 규칙이 이제 두 개의 곱을 내놓고, 델타 방식이 다 소진되는 데 한 번의 라운드를 더 필요로 하기 때문입니다; 모든 곱이 마이크로초 단위인 열두 이름짜리 장난감 위에서는, 준순진 방식이 실제 시계로는 이득이 아닙니다. 떨어지는 것은 도출-사건 개수, 71에서 28이며, 규모가 커질 때 중요해지는 숫자는 바로 이것입니다. 폐쇄는 진짜로 새로운 사실 23개가 필요했습니다(레이블 칸 16개에 엣지 7개); 준순진은 그것들에 도달하는 데 28번의 사건을 썼고, 이는 5번의 오버헤드인 반면, 순진 방식은 71번을 써서 같은 귀결을 파동마다 되풀이해 도출했습니다. 실제 엔진에서 작업량은 몇 번의 커널 실행이 그것을 둘러싸는지가 아니라 도출 사건의 수에 비례합니다: 작업 목록 엔진은 사건 하나당 메모리를 한 번 건드리며, 이 모듈은 그 경제성을 의미론적 사실로서 단언합니다, st_sn["derivations"] < st_nv["derivations"]이며, 두 엔진이 동일한 폐쇄를 내놓는다는 assert 바로 옆에 있습니다(gpu_fixpoint.py 400–402행과 424–426행). 파동별 열들 또한 잠시 멈춰 볼 만한 그림입니다: 9, 12, 7, 0은 확장되었다가 정점을 찍고 비워지는, 새로운 귀결의 최전선인 파동 전선(wavefront)입니다. 이는 1권이 23개-사실 지식 베이스 위에서 $T_P$ 연산자(1권의 즉각귀결 연산자로, 사실들의 집합을 프로그램 $P$ 가 거기서 한 걸음에 도출하는 모든 것으로 보내는 연산자입니다)의 폐쇄 파동들에 대해 그렸던 것과 같은 파동 전선이며, 2권의 오라클이 파이썬 집합으로 순회하는 것과 같은 파동 전선입니다; 델타 규율은 그저 파동의 앞부분만이 방문할 가치가 있다는 관찰일 뿐입니다.

배치화: 진짜 GPU 논지

지금까지의 모든 것은 온톨로지를 한 번에 하나씩만 닫는다면 그저 흥미로운 이야기에 그칠 것입니다; 작업 목록 엔진은 이미 그 일을 잘 해냅니다 [2]. 하드웨어가 보상하는 움직임은 많은 온톨로지를 한꺼번에 닫는 것입니다. 컴패니언은 학계 TBox의 $B = 100$ 개 변형을 만드는데, 각 변형은 서로 다른 이름 붙은 개념들 사이에 알려진 포섭 관계 하나를 추가로 더한 것이어서, 변형들 사이에는 오직 $H_1$ 표만 다릅니다; 이 변형들은 모양이 $(100, 12, 12)$ 인 하나의 쌓인 불 텐서가 되며, 변형마다 하나씩인 $H_1$ 판을 갖되 다른 모든 공리 표는 공유합니다(gpu_fixpoint.py 365–383행). 여기서 앞선 설계 선택들이 한꺼번에 보상받습니다. bmm은 np.matmul이 그러듯 앞쪽 배치 차원에 대해 브로드캐스트하고, 초기 상태 생성자는 배치 차원을 받으며, close_naive는 그 쌓인 텐서를 자신의 $H_1$ 오버라이드로 받아들이므로, 모든 파동의 모든 규칙이 하나의 전체-배치 연산이 되어 백 개의 변형에 대한 파이썬 루프 없이 배치 전체가 닫힙니다(gpu_fixpoint.py 153–169행). 배치는 가장 느린 구성원이 도달할 때 고정점에 도달합니다; 일찍 포화된 조각들은 그저 더 이상 바뀌지 않을 뿐이며, 멱등성 덕분에 그 여분의 파동들은 그것들에게 무해한 아무-일도-안-함(no-op)이 됩니다. 검증은 이전과 마찬가지로 조금도 봐주지 않습니다: 100개의 조각 하나하나가 자신의 변형별 폐쇄와, 그리고 기본 공리에 그 변형이 더한 포섭 관계를 더해 다시 실행한 오라클과 같음이 단언됩니다(gpu_fixpoint.py 447–460행). 커밋된 실행:

[5] batching: B = 100 TBox variants (one extra told subsumption each) closed in
    ONE stacked (100, 12, 12) tensor pass, no Python loop over B; every slice ==
    its per-variant closure == the replayed oracle
    batched pass: waves=5, matmuls=55 (each a whole-batch op), derivations=16152

다섯 번의 파동이 필요한 것은 가장 어려운 변형이 그만큼을 요구하기 때문입니다; 55번의 행렬 곱은 각각 백 개의 세계 전부를 건드립니다; 배치 전체에 걸쳐 16,152번의 도출 사건입니다. 실제 시계(wall-clock)는 이 모듈이 단언하기를 거부하는 유일한 숫자인데, 밀리초는 기계마다 다르기 때문입니다; 그 대신 이 스위트는 인용된 표가 실재하는 무언가로 이어지도록 하나의 정본 실행을 하나의 산출물로 커밋합니다. 그 커밋된 정본 타이밍(5회 중 최선, 이 스위트의 README.md):

    timing, best of 5 (measured wall-clock: varies run to run, asserted NOWHERE):
      Python loop over 100 closures :   14.75 ms
      one stacked tensor pass       :    1.79 ms   (≈8.2× faster)

이 모듈이 그러하듯, 이것을 정직하게 이름 붙입시다. 이것은 GPU 측정이 아니라 CPU-NumPy 프록시입니다: 파이썬-루프 오버헤드를 없애고 하나의 BLAS(Basic Linear Algebra Subprograms, 모든 수치 스택이 호출해 들어가는 표준 최적화 행렬-곱 라이브러리) 호출이 배치 전체에 걸쳐 상각되도록 함으로써 얻는 여덟 배의 이득이며, 진짜 가속기라면 거의 깨어나지도 않을 만큼 작은 행렬 위에서의 이야기입니다. 이것이 보여 주는 것은 이득의 크기가 아니라 그 형태입니다: 조밀하고 규칙적인 대수로 표현된 고정점은 공짜로 배치화되며, 이것이 바로 GPU 하드웨어가 대가를 치르고 사는 성질입니다. 이 프록시와 실전 시스템 사이의 거리는 이름 붙은 공학 작업들의 목록이며, 그 전부가 같은 계산법 계약의 하류에 놓여 있습니다 [1]: 조밀한 판 대신 희소 커널(실제 온톨로지의 $S$ 는 압도적으로 0입니다), 규칙 표를 위한 해시 조인과 열-지향 레이아웃, 그리고 유휴 조각이 더 이상 아무 비용도 치르지 않도록 하는 작업 목록 스케줄링입니다. 그 공학이 달성하는 바에 대한 멀티코어 닻은 RDFox 배후의 병렬-구체화 계열이며, 이는 데이터로그 고정점의 규칙 인스턴스를 대부분 락-프리 색인을 써서 코어들에 걸쳐 어떻게 분할하는지를 보여 주었습니다 [3]; 그 이후의 시스템 보고서 [4]는 128코어 머신에서 최대 87배에 이르는 구체화 속도 향상을 측정했으며, 초당 수백만 개의 트리플을 지속적으로 처리했습니다. 그 숫자들은 그 엔진과 그 하드웨어에 속하는 것이며, 여기서는 이 장난감이 가리키는 천장으로서 인용될 뿐, 이 장난감이 달성한 그 무엇으로서 인용되는 것이 결코 아닙니다.

다른 차선: 건전성으로 속도를 사다

배치 하드웨어 위에서 추론기를 빠르게 만드는 두 번째 방법이 있으며, 이 권은 그것을 계속 만나 왔습니다: 추론을 멈추고, 대신 추론기를 흉내 내도록 신경망을 훈련시키는 것입니다. 그 흐름의 성숙한 버전은 온톨로지의 구체화된 폐쇄 위에서 재귀적 아키텍처를 훈련시킨 다음 순전파(forward pass)로 함의를 예측하며, 온톨로지마다 다시 훈련되고 벤치마크 온톨로지들에 걸쳐 0.916에서 0.999 사이의 함의-가능-관계 F1을 보고합니다 [5]; 같은 흐름의 더 앞선 보고서는 그것이 흉내 내던 RDFox 구체화 엔진보다 최대 두 자릿수(백 배) 더 빠르면서 F1은 0.95 근처였다고 측정했습니다 [6]. 이 거래를 시스템의 화폐로 해독해 봅시다. 처리량은 진짜입니다: 순전파는 정확히 이 장이 방금 지은 조밀한 배치 텐서 프로그램에서 고정점 루프만 뺀 것이므로, 여기서 문제 삼는 모든 하드웨어 이점을 그대로 물려받습니다. 그 대가는 두 줄입니다. 첫째, 건전성입니다: F1이 0.95 근처라는 것은 도출된 사실 스무 개 중 대략 하나가 틀렸거나 빠졌다는 뜻이며, 그 어떤 증명도 딸려 있지 않고 옳은 열아홉 개를 구별해 줄 신호도 없습니다; 놓친 충족 불가능성은 조용히 출하된 모델링 버그이며, 이는 정확히 2권의 ⊥-기계 장치가 잡아내기 위해 존재하는 그 실패입니다. 둘째, 일반성입니다: 이 모방기는 온톨로지마다 훈련되고 자신이 본 분포에 대해서만 답하는 반면, 이 장의 엔진은 한 번도 만난 적 없는 세 개의 합성 TBox 위에서 아무 변경 없이 돌아갔는데, 구성에 의한 정확함은 공짜로 전이되기 때문입니다. 이 비교는 허수아비가 아닙니다; 이것은 이 분야가 되풀이하는 흥정이며, 정직한 진술은 두 차선 모두가 이제 같은 하드웨어 위에서 돌아간다는 것입니다. 이 권은 정확한 차선에서는 이 거래를 거부하는데, 그 차선에서 폐쇄의 요점 전체가 모든 칸이 하나의 정리라는 데 있기 때문입니다. 7부는 다른 조건으로 그 속도를 되사 옵니다: 기호 어텐션은 추론을 어텐션 모양의 커널 안에 집어넣은 다음, 그 보증에 대한 대가를 F1이 아니라 증명과 탐침(probe)으로 치를 것입니다.

행렬이 볼 수 없는 것

조밀한 표현에는 세 개의 사각지대가 있으며, 각각에 이름과 해법이 있습니다.

메모리는 전체 집합에 대해 제곱으로 자랍니다. $S$ 와 모든 $R_r$ 은 $n^2$ 개의 칸을 대가로 치릅니다. 이 장의 $n = 12$ 에서는 그것이 144개의 불리언이지만, SNOMED CT 규모에서는 $n \approx 3.8 \times 10^5$ 개의 개념 이름이므로 단일 조밀 행렬은 $n^2 \approx 1.4 \times 10^{11}$ 개의 칸이 되어 도착하자마자 죽습니다. 반면 실제 폐쇄는 희소합니다(우리의 장난감조차 포화된 $S$ 는 144칸 중 겨우 39칸만을 채웁니다). 그러므로 희소 형식과 작업 목록은 규모에서의 최적화가 아니라 실행 가능성의 조건이며, 이것이 위에서 인용한 실전 엔진들이 그것들을 중심으로 지어진 이유입니다 [2][3].

불 OR은 유래를 지웁니다. 순진한 실행의 71번의 도출 사건은 39개의 칸으로 무너져 들어갑니다; 어떤 공리가 어떤 칸을 만들어 냈는지, 어떤 규칙 발동을 거쳤는지는 멱등성이 그 재도출을 흡수하는 순간 사라져 버립니다. 그 해법은 4권의 움직임과 같습니다: Scallop의 데이터로그가 그러하고 2권의 유래 반환 장이 마련해 둔 것처럼, 원소들이 설명, 즉 공리 지시자(indicator) 위의 유래 다항식을 실어 나르는 더 풍부한 반환 위에서 같은 곱들을 평가하는 것입니다. 그 대가는 실재합니다: 칸은 더 이상 비트 하나가 아니고, 덧셈은 더 이상 멱등적이지 않으며, 종료성은 다시 주의를 필요로 합니다; 이 권 자신의 정당화 장은 최소 공리 집합을 얻기 위해 바로 그 대가를 의도적으로 치렀습니다.

이 모양들을 벗어난 규칙들은 저마다의 연산자를 필요로 합니다. 이 모듈은 CR1–CR4와 CR⊥, 사슬 규칙만을 정확히 벡터화하며, 자신이 구현하지 않은 것은 거부합니다: 어떤 assert는 커밋된 실행이 조금도 사용하지 않는 규칙을 몰래 내보내는 대신, 단순한 역할 포함 $r \sqsubseteq s$ 를 시끄럽게 거부합니다(gpu_fixpoint.py 96–99행). 완전한 EL++는 노미널(nominal), 구체 영역(concrete domain), 범위 제한을 더하며, 그 각각은 저마다의 행렬 연산자와 저마다의 정확성 논증을 요구합니다. 새로운 규칙 모양 하나하나가 새로운 커널이며, 그 유지 보수 표면이야말로 성숙한 추론기가 갖추어야 할 바로 그것입니다. 이 규율 전체의 형제 사례는 4권에서 한 층 아래에 놓여 있습니다: KLay는 불규칙한 산술 회로를 가속기를 위한 조밀한 레벨별 텐서 연산으로 계층화하는데 [7], 이는 여기서 포화 계산법에 대해 이루어진 것과 같은 움직임이며, GPU 네이티브 장이 그 이야기를 들려주었습니다; 이 장은 회로가 아니라 논리의 수준에서 그 시스템적 형제입니다.

아직 풀리지 않은 부분

세 개의 공백이 여전히 열려 있으며, 그중 세 번째는 이 장 자신의 숫자 안에서 열려 있습니다. 첫째, 가속기 위의 동적 작업 목록입니다: 준순진 최전선(9, 12, 7, 0)이 계산해야 할 옳은 대상이지만, 그것은 희소하고 줄어드는 반면, SIMD(단일 명령 다중 데이터, single instruction, multiple data) 하드웨어, 곧 하나의 연산을 여러 값에 한꺼번에 적용하는 하드웨어는 넓고 규칙적이며 예측 가능한 작업을 원합니다; 여기서 배치화된 패스는 조밀하게 다시 계산함으로써 그 불일치를 덮어 버리는데, 이는 오직 행렬이 작기 때문에만 온당합니다. 희소해져 가는 포화 최전선을 GPU 위에 그대로 머무르게 하는 정립된 설계는 아무도 갖고 있지 않습니다. 둘째, 디바이스 위에서의 점진적 구체화입니다: 앞 장은 삭제가 어려운 방향임을 보였고(DRed는 과잉 삭제한 뒤 다시 도출합니다), 그 기계 장치 전체, 즉 과잉삭제 집합, 재도출 패스, 유래 검사에는 배치화된-텐서 정식화가 전혀 받아들여진 바 없습니다; GPU 위에서의 철회(retraction)는 사실상 연구된 바가 없습니다. 셋째, 빠져 있는 비용 모델입니다. 이 장은 커밋된 숫자를 가진 세 가지 체제, 곧 포인터 쫓기(오라클), 조밀한 순진 방식, 조밀한 배치 방식을 보여 주고 인용된 네 번째 체제(병렬 작업 목록)도 하나 더하지만, $n$ 이나 표 밀도, 배치 폭 같은 TBox 통계로부터 어떤 체제가 주어진 작업 부하에서 이기는지를 예측하는 것은 여기에도 문헌에도 없습니다. 우리의 8.2배는 한 대의 기계, 한 가지 모양, 한 가지 배치 크기에 대한 것입니다; 작업 부하마다 자신의 실행 전략을 선택할 수 있는 시스템이라면, 이 분야 전체가 그렇듯 이 장도 갖고 있지 않은 그 모델을 필요로 할 것입니다.

왜 중요한가

이 시리즈는 세 방향에서 이 그림으로 수렴해 왔습니다. 1권은 추론을 유한 격자를 오르는 단조 연산자로 정의했습니다; 2권은 그것을 EL 완성으로 구체화하고 그 계산법이 건전하고 완전함을 증명했습니다; 4권은 반환 위에서 평가된 논리가 학습 하드웨어 위에서 돌아감을 보였습니다. 이 장은 그 셋이 영수증을 지참하고 만나는 곳입니다: 포인터를 쫓는 집합으로 계산한 것과 배치화된 불 대수로 계산한 것이 같은 폐쇄이며 칸 하나하나까지 동일함이 단언되므로, "추론이 어떤 하드웨어를 써야 하는가"는 정확성에 관한 물음이 아니라 희소성과 스케줄링에 관한 공학적 물음이 됩니다. 여러분 자신의 연구에 옮겨 갈 수 있는 자산은 바로 오라클 표준 그 자체입니다: 정확한 방법을 벡터화하거나 델타로 걸러 내거나 그 밖의 방식으로 다른 플랫폼으로 옮길 때, 빠른 버전을 독립적인 느린 구현에 맞서 실제 입력 위에서 그리고 적대적인 합성 입력 위에서 집합-동등성에 붙들어 매고, 눈짐작이 아니라 assert가 그 주장을 책임지게 하십시오. 그리고 이 장이 그래야 했듯, 여러분의 글에서도 두 차선을 구분해 두십시오: 측정된 장난감 타이밍은 이름 붙이되 결코 단언하지 말고, 인용된 시스템 숫자는 출처를 밝히되 결코 혼동하지 말며, 학습된 모방기는 그것이 치르는 건전성의 값어치로 매기십시오.

핵심 용어

행렬화(Matrixization) — 정규화된 TBox를 불 표( $H_1$ , $E^3_r$ , $E^4_r$ , 논리곱 색인과 투영)로 컴파일하여, 완성 규칙이 색인이 매겨진 개념 전체 집합 위의 행렬 연산이 되게 하는 것.
불 행렬 곱( $\odot$ ) — OR-AND 반환 위의 행렬 곱, $(X \odot Y)[i,j] = \bigvee_k X[i,k] \wedge Y[k,j]$ ; 0/1 행렬의 float 행렬 곱셈 뒤에 0보다 크다는 검사를 붙여 정확하게 계산됩니다.
포화 / 고정점(Saturation / fixpoint) — 어떤 파동이 아무것도 바꾸지 못할 때까지 단조적이고 멱등적인 갱신을 반복하는 것; 불 행렬의 유한한 격자 위에서 종료가 보장됩니다.
순진 평가(Naive evaluation) — 매 파동마다 전체 상태에 맞서 모든 규칙을 발동시키는 것; 옳지만, 알려진 사실이 매 파동 재도출되므로 최대로 낭비적입니다.
준순진(델타) 평가(Semi-naive / delta evaluation) — 각 규칙을 오직 이전 파동에서 새로 생긴 전제만을 통해 발동시키고, 다른 전제에 대해서는 전체 상태와 조인하는 것; $\odot$ 가 $\vee$ 위에 분배되는 성질에 의해 전부-옛것인 규칙 인스턴스만을 정확히 건너뜁니다.
도출 사건(Derivation event) — 어떤 규칙 적용의 원출력 안의 참-칸 하나이며, 재도출도 포함됩니다; 준순진 평가가 줄이는(여기서는 71에서 28로) 작업량 척도이며, 실제 엔진의 비용이 뒤따르는 그 척도입니다.
배치화 / 브로드캐스팅(Batching / broadcasting) — $B$ 개의 문제 인스턴스를 하나의 앞쪽 텐서 차원으로 쌓아, 모든 규칙 적용이 인스턴스별 루프 없이 하나의 커널 호출로 배치 전체를 처리하게 하는 것.
구체화 처리량(Materialization throughput) — 이 부의 시스템 화폐로, 포화 상태에서 초당 도출되는 사실의 개수입니다; 인용된 멀티코어 엔진이 보고한 스케일링(128코어에서 최대 87배)이 그 기준점입니다.
신경망 추론기 모방(Neural reasoner emulation) — 추론기의 폐쇄를 예측하도록 신경망을 훈련시키는 것; 구성에 의해 빠르고 배치화되어 있으며, 구성에 의해 근사적이고, 온톨로지마다 다시 훈련됩니다.

이 장이 이끄는 곳

이 장은 파동당 연산 횟수를 헤아리고 그 파동들을 저렴하게 만들었을 뿐, 파동이 몇 번이나 있어야 하는지는 결코 묻지 않았습니다. 그 물음에는 그 나름의 형태가 있습니다: 작업량(총 연산 수)과 깊이(의존적인 단계들의 가장 긴 사슬)의 대결이며, 추론에게 이것은 진짜 트릴레마입니다. 사슬을 한 고리씩 늘리는 대신 관계를 제곱하는 것 같은, 깊이를 줄이는 요령들은 작업량을 폭발시키고, 작업량을 억제하는 요령들은 깊이를 다시 늘어나게 하기 때문입니다. 작업-깊이 트릴레마는 실행 예제와 합성 사슬 위에서 이를 정확하게 만듭니다: 512노드짜리 관계 사슬이 510번의 저렴한 파동으로 닫히거나, 아홉 번의 거대한 제곱(더하여 한 번의 확인 패스)으로 닫힙니다. 51배의 깊이 절감에 10,270배의 작업량 비율이라는 커밋된 숫자와, 어떤 일정도 둘 다를 가질 수 없는 이유에 대한 정직한 진술이 함께 있습니다. 이것이 이 부의 시스템 장부에서 V부로 이어지는 다리이며, 그곳에서 깊이는 더 이상 스케줄링의 선택이 아니라 아키텍처에 구워 넣어진 단단한 천장이 됩니다.

컴패니언 코드: examples/frontier/gpu_fixpoint.py는 행렬화, 두 고정점 엔진, 시드 부여 합성 생성기, 배치화된 텐서 패스, 그리고 모든 오라클 assert를 구현하며, 2권의 examples/symbolic/el_completion.py를 정답(ground truth)으로서 변경 없이 임포트합니다. python3 examples/frontier/gpu_fixpoint.py를 실행하면 이 장의 모든 숫자를 재현할 수 있습니다; 이름 붙은 실제 시계 행들을 제외하면, 출력은 실행할 때마다 바이트 단위로 동일하며 모든 주장은 assert로 지켜집니다.

이 장에서 다루는 내용​

하나의 사슬 규칙에서 계산법 전체로​

모든 규칙이 하나의 곱이 되다​

오라클 표준: 두 번 겹친 정확함​

준순진(semi-naive): 행렬 항으로 본 델타 규율​

배치화: 진짜 GPU 논지​

다른 차선: 건전성으로 속도를 사다​

행렬이 볼 수 없는 것​

아직 풀리지 않은 부분​

왜 중요한가​

핵심 용어​

이 장이 이끄는 곳​