유래 반환: 사실은 어디서 오는가
📍 현재 위치: 6부 · 주석·시간 논리 — 18장. 추론 벤치마크는 추론기가 어떤 사실이 성립하는지에 답하는 속도가 얼마나 빠른지를 측정했습니다; 이제 우리는 같은 사실에 대해 다른 질문을 던집니다 — 그것은 어디서 왔는가? — 그리고 유래(provenance)와 신뢰도(confidence)가 사실은 두 벌의 옷을 입은 하나의 개념임을 발견합니다.
평범한 추론기는 "이것이 함의되는가?"라는 질문에 예 또는 아니오라는 맨몸의 대답만 내놓습니다. 그러나 실제 지식 베이스는 도출된 사실로부터 더 많은 것을 원합니다: 그것이 어떤 단언된 사실 위에 놓여 있는지, 그것을 얼마나 확신해야 하는지, 그리고 때로는 그것이 언제 성립하는지까지 말입니다. 이 장은 그 가운데 첫 번째 — 사실이 어디서 왔는지에 대한 기록인 유래(provenance) — 를 다루며, 이것이 덧붙인 부가 기능이 아니라 단 하나의 대수적 조작임을 보입니다. 모든 기초 사실(base fact)에 레이블(label)을 붙이고, 평범한 전방 연쇄(forward-chaining) 고정점을 실행하며, 유도가 결합하는 대로 레이블도 결합하게 두십시오. 레이블이 살고 있는 대수를 바꾸면, 같은 실행이 같은 결론에 대해 다른 정보를 보고합니다.
소문 하나가 두 경로로 동시에 당신에게 도달한다고 상상해 보십시오. 한 친구는 직접 말해 주고, 다른 친구는 제삼자에게서 들은 이야기를 공통의 지인을 통해 전해 들었습니다. 그 소문이 당신에게 도달했는지를 알고 싶다면 둘 중 어느 경로만으로도 충분합니다 — 둘 중 하나의 경로만 전달되었어도 "그렇다"고 말할 수 있습니다. 하지만 그 소문이 무엇에 의존하는지를 알고 싶다면, 두 사람을 거치는 사슬은 두 연결 모두가 제대로 작동해야 하는 반면, 직접 경로는 그 하나의 연결만 있으면 됩니다. "어느 한쪽 경로로도 충분하다"와 "경로의 모든 연결이 필요하다"는 증거를 결합하는 서로 다른 두 방식이며 — 놀랍게도 이 두 연산만 있으면 도출된 어떤 사실이 정확히 어디서 왔는지를 추적하는 데 충분합니다.
이 장에서 다루는 내용
- 반환 해독하기 — 가환 반환(commutative semiring) 은 그저 "더하기"와 "곱하기"를 가진 레이블의 집합일 뿐입니다; 이를 유래로 읽어내는 방식은 규칙 몸체(논리곱)가 로 결합되고, 같은 사실의 대안적 유도들이 로 결합된다는 것입니다.
- 주석 달린 고정점 — 데이터로그와 정확히 동일한 최소 고정점 루프이지만, 이제는 맨몸의 진리값 대신 모든 유도를 통해 반환 값을 실어 나릅니다.
- 하나의 그래프, 두 개의 유도 —
reach(p3, p1)이 두 가지 다른 방식으로 증명될 수 있는, 세 개의 엣지로 이루어진 인용 그래프이며, 바로 이것이 가 눈에 보이는 일을 하게 만드는 지점입니다. - 하나의 유도에 대한 네 가지 해석 — 불(Boolean), Which, Why, 그리고 다항식 반환으로, 각각이 같은 실행 위에서 서로 다른 입니다.
- 실제 실행 결과 — 하나의 사실, 네 개의 레이블을 프로그램의 실제 출력에서 그대로 인용하고, 유래 다항식의 순서를 설명합니다.
- 유래가 곧 신뢰인 이유 — 자신이 의존하는 기초 사실과 경로의 이름을 댈 수 있는 도출된 사실은 감사 가능(auditable)하며, 이는 신경망 모델이 줄 수 없는 설명에 대응하는 기호적 대응물입니다.
반환 해독하기
위협적으로 들리는 이 단어를 풀어 보겠습니다. 반환(semiring)이란 레이블들의 집합 에, 그것들을 결합하는 두 가지 방법 — 덧셈 ("오플러스"라 읽습니다)와 곱셈 ("오타임스"라 읽습니다) — 을 더한 것으로, 각각은 항등원을 하나씩 가집니다 — 은 가 무시하는 레이블이고(), 은 가 무시하는 레이블입니다(). 두 연산 모두 결합법칙과 교환법칙을 만족하고, 는 에 대해 분배되며, 은 아래에서 소멸합니다. 이 전체 묶음을 다섯 개짜리 튜플 로 씁니다. 이것은 뺄셈 능력을 잃어버린 환(ring)입니다 — 이는 유래에 정확히 딱 들어맞는데, 왜냐하면 증거는 결합할 수는 있어도 사실을 역도출할 수는 없기 때문입니다.
이제 이 대수를 유래로 바꾸어 놓는 해석을 보겠습니다. 도출된 사실은 규칙이 발동함으로써 증명됩니다. 규칙이 한 번 발동하는 것을 살펴보면: 그 몸체는 모두 성립해야 하는 사실들의 논리곱(conjunction)이므로, 그 발동의 레이블은 그것이 사용한 사실들의 레이블의 -곱입니다. 하나의 사실은 여러 번의 발동 — 여러 개의 대안적 유도(alternative derivation) — 로 증명될 수 있으며, 그 가운데 어느 하나만으로도 충분하므로, 그 사실의 전체 레이블은 그 모든 것에 걸친 -합입니다. 두 낱말, 두 연산자입니다:
- (곱하기)는 한 규칙 몸체 안의 사실들을 결합합니다 — "그리고"이며, 모든 연결 고리가 필요합니다.
- (더하기)는 같은 사실에 대한 대안적 유도들을 결합합니다 — "또는"이며, 어느 증인 하나로도 충분합니다.
동반 프로그램은 반환을 말 그대로 네 개의 연산과 두 개의 상수로 인코딩합니다 — 위의 정의보다 더 많은 구조를 갖지 않습니다(annotated.py, 38–46번째 줄):
class Semiring:
"""A commutative semiring (K, ⊕, ⊗, 0, 1) as four operations + two constants."""
def __init__(self, zero, one, plus, times, name=""):
self.zero = zero
self.one = one
self.plus = plus
self.times = times
self.name = name
이후의 모든 것은 이 객체에 대해 제네릭합니다: 다른 Semiring을 고르더라도 추론 엔진은 단 한 줄도 바뀌지 않고, 그것이 실어 나르는 레이블만 바뀝니다. 형식적으로, 머리 원자 의 레이블은 다음과 같습니다
를 결론짓는 모든 발동에 걸친, 그 발동의 몸체 레이블들의 -곱에 대한 -합입니다 [1]. 왼쪽에서 오른쪽으로 읽으십시오: 몸체 안에서는 곱하고, 몸체들 사이에서는 더합니다.
주석 달린 고정점
은 실제로 어디서 계산될까요? 바로 1권이 데이터로그를 위해 구축했던 그 루프 안에서입니다. 즉시 귀결 연산자(immediate-consequence operator)를 떠올려 보십시오: 기초 사실로 씨앗을 뿌리고, 몸체가 현재 성립하는 모든 규칙을 발동시키며, 한 라운드가 아무것도 더하지 못할 때까지 반복합니다 — 이것이 최소 고정점(least fixpoint)입니다. 주석 달린 버전은 그 형태를 정확히 그대로 유지하면서 그 안에 반환 값을 실어 나릅니다(annotated.py, 79–95번째 줄):
def provenance_lfp(edb_annot, rules, sr: Semiring, max_iter: int = 100):
"""Least fixpoint of the semiring-annotated immediate-consequence operator.
Each round recomputes every fact's annotation as the ⊕-sum, over all one-step
derivations, of the ⊗-product of the body annotations — starting from the EDB
tokens, which persist. Converges for any ω-continuous semiring on an acyclic
program (all five below, on the DAG example)."""
ann = dict(edb_annot)
for _ in range(max_iter):
new = dict(edb_annot) # base tokens persist; IDB is recomputed
for head, body in rules:
for sub, prod in _match_body(body, ann, sr, {}, sr.one):
h = _apply(head, sub)
new[h] = sr.plus(new.get(h, sr.zero), prod)
if new == ann:
return ann
ann = new
세 줄이 이 발상 전체를 실어 나릅니다. _match_body는 규칙 몸체를 훑으면서 그것이 매칭하는 모든 사실의 -곱을 실어 나르는데, 곱셈 항등원 sr.one에서 시작하여 사실의 레이블을 하나씩 곱해 나갑니다 — 그 재귀 단계는 말 그대로 sr.times(acc, label)입니다(annotated.py, 71번째 줄). 각 발동은 그 한 번의 유도에 대한 레이블인 prod를 산출합니다. 그런 다음 new[h] = sr.plus(new.get(h, sr.zero), prod)는 덧셈 항등원 sr.zero에서 시작하여 그 유도를 로 머리의 누적 합계에 접어 넣습니다. 그리고 if new == ann: return ann은 평범한 데이터로그와 동일한 고정점 검사입니다 — 한 라운드가 아무것도 바꾸지 못하면 멈춥니다. 여기서 EDB는 외연 데이터베이스(extensional database), 즉 단언된 기초 사실이며, IDB는 내포 데이터베이스(intensional database), 즉 도출된 사실입니다. 기초 토큰(token)은 매 라운드마다 그대로 유지되고(new = dict(edb_annot)), 도출된 레이블은 처음부터 다시 계산됩니다 — 그래서 모든 대안적 유도가 다시 합산되며 그 무엇도 이중으로 세어지지 않습니다 [2].
하나의 그래프, 두 개의 유도
가 제 몫을 하는 모습을 보려면 하나 이상의 유도를 가진 사실이 필요합니다. 그 예시는 세 개의 엣지를 가진, 세 편의 논문으로 이루어진 작은 인용 그래프이며, 각 엣지는 서로 다른 유래 토큰(provenance token)을 지니고 있습니다(annotated.py, 151–155번째 줄):
EDGES = [
("p3", "p2", "r", 0.9),
("p2", "p1", "s", 0.8),
("p3", "p1", "t", 0.5),
]
엣지에서 토큰을 읽어 보십시오: r은 엣지 p3 → p2에, s는 p2 → p1에, 그리고 t는 직접 엣지 p3 → p1에 레이블로 붙습니다. (각 행의 네 번째 숫자는 지금은 무시하십시오 — 그것은 신뢰도(confidence)이며, 이 장 끝의 다리 놓기 부분이 바로 그것을 위한 것입니다.) 도달가능성(reachability)은 여러분이 전에 본 적 있는 두 절짜리 전이 규칙(transitive rule)입니다: 엣지 하나는 도달가능성이며, 엣지 다음에 도달가능성이 이어지면 그것도 도달가능성입니다(annotated.py, 157–160번째 줄):
REACH_RULES = [
(("reach", "?x", "?y"), [("edge", "?x", "?y")]),
(("reach", "?x", "?z"), [("edge", "?x", "?y"), ("reach", "?y", "?z")]),
]
이제 reach(p3, p1)을 살펴보십시오. 이것은 두 개의 유도를 가집니다. 기초 절(base clause)은 직접 엣지 위에서 발동하여 하나의 토큰으로 이루어진 레이블 를 냅니다. 재귀 절은 p3 → p2에 이어 도달가능성 p2 → p1 위에서 발동하는데, 이는 레이블이 곱해지는 두 사실로 이루어진 몸체입니다: . 어느 유도든 독립적으로 그 사실을 성립시키므로, 그 레이블은 둘의 -합입니다:
아래의 모든 반환은 바로 그 하나의 식 를 서로 다르게 읽어낸 것일 뿐입니다.
하나의 유도에 대한 네 가지 해석
다음은 네 개의 반환으로, 각각 레이블이 무엇인지, 그리고 와 가 그 위에서 어떻게 작용하는지에 대한 서로 다른 선택입니다. 그 정의역은 정보량 면에서 점점 올라갑니다 — 비트 하나에서부터 완전한 다항식에 이르기까지 — 그리고 마지막 열은 각각이 우리의 이중으로 도출된 사실에 대해 무엇을 계산하는지를 보여줍니다.
| 반환 | 정의역 (레이블이란…) | (대안 결합) | (몸체 결합) | reach(p3, p1)을 …로 읽음 |
|---|---|---|---|---|
| 불(Boolean) | 진리값 | ∨ (또는) | ∧ (그리고) | True |
| Which | 토큰들의 집합 | ∪ (합집합) | ∪ (합집합) | [r, s, t] |
| Why | 토큰 집합들의 집합 | ∪ (합집합) | ⋈ (쌍별 합집합) | [[r, s], [t]] |
| 다항식 | + (계수 더하기) | × (곱하기) | t + r·s |
불(Boolean) 반환 은 모든 세부 사항을 버리고 오직 "성립하는가?"에만 답합니다 — 는 가 됩니다(annotated.py, 100번째 줄). Which-유래 레이블은 두 연산 모두를 집합 합집합으로 만드는데(annotated.py, 102–103번째 줄), 그래서 어떤 유도에든 참여하는 모든 토큰의 납작한 집합을 누적합니다: . 이것은 어떤 출처가 관여했는지는 말해 주지만, 그것들이 어떻게 경로로 묶이는지는 잃어버립니다 — 그리고 두 연산 모두가 합집합이기 때문에, 공집합이 두 항등원 역할을 동시에 합니다. 엄밀히 말하면 이것은 반환의 정의를 구부립니다: 이면 소멸 법칙 이 더는 성립하지 않습니다 — 공집합이 아닌 에 대해 이기 때문입니다 — 그리고 은 어떤 진짜 반환이든 원소 하나로 붕괴시켜 버릴 것입니다. 그래서 Which는 온전한 반환이라기보다는 두 연산 모두에 재사용된 멱등 가환 모노이드(idempotent commutative monoid)로 읽는 것이 가장 좋습니다 — 이는 유래 문헌이 조심스럽게 다루는 계보(lineage) 사례로서, 이 위계에서 하나뿐인 퇴화된 모서리입니다.
Why-유래는 그 묶임을 그대로 유지합니다. 레이블은 증인 집합(witness set)들의 집합이며, 각 증인 집합은 그 사실을 증명하는 하나의 자족적인 토큰 묶음입니다. 그 는 합집합입니다(대안적 증인들을 모읍니다), 그러나 그 는 쌍별 합집합 조인(join) ⋈입니다 — 두 몸체를 결합하면 그 증인들의 모든 쌍별 합집합이 만들어집니다(annotated.py, 106–111번째 줄). 우리 사실에 대해 직접 유도는 증인 집합 를 제공하고 두-홉 유도는 를 제공하여, 두 개의 대안적 증인 와 를 냅니다. 마지막으로 다항식 반환(polynomial semiring) — 토큰을 변수로 하는, 자연수 계수를 가진 평범한 다항식(annotated.py, 114–130번째 줄) — 은 모든 것을 유지합니다: 는 다항식 곱셈이고 는 덧셈이므로, 두 유도는 두 개의 단항식 가 됩니다. 이것이 가장 많은 정보를 담은 해석입니다; 불(Boolean)과 Why는 모두 그것으로부터 어떤 구조를 "잊어버림"으로써 얻어지는 반환 준동형사상의 상(homomorphic image)이며, 반면 Which는 — 소멸 법칙이 없으므로 — 깔끔한 준동형사상의 상이라기보다는 퇴화된 계보 붕괴입니다 [1].
실제 실행 결과
그 모듈을 실행하면 네 가지 모두를(그리고 잠시 보류해 둔 다섯 번째까지) reach(p3, p1)에 대해 평가하고, 하나의 사실을 여러 레이블 아래 출력합니다(annotated.py, 272–281번째 줄):
reachability of (p3, p1) — direct edge t, plus two-hop path r·s
Boolean : True
Which-prov : ['r', 's', 't']
Why-prov : [['r', 's'], ['t']]
Polynomial : t + r·s
Confidence : 0.8
하나의 유도, 네 개의 유래 답변, 단 한 번의 고정점 실행에서 — 다섯 줄의 출력에 이 논지 전체가 담겨 있습니다. 다항식 줄은 r·s + t가 아니라 t + r·s로 나타나며, 그 순서는 우연이 아니라 선택된 것입니다. 렌더러는 단항식을 먼저 차수로, 그다음 사전순으로 정렬합니다(annotated.py, 140–144번째 줄):
for m in sorted(p, key=lambda m: (len(m), m)):
c = p[m]
mon = "·".join(m) if m else "1"
terms.append(mon if c == 1 else f"{c}·{mon}")
return " + ".join(terms)
그래서 더 짧은 직접 유도 (토큰 하나, 차수 1)가 더 긴 두-홉 유도 (토큰 둘, 차수 2)보다 앞서 출력됩니다. 다항식을 왼쪽에서 오른쪽으로 읽는 것은 유도를 최단 경로부터 순서대로 읽는 것과 같습니다. 참고로 각 단항식의 계수는 정확히 같은 토큰 묶음을 산출하는 서로 다른 유도의 개수를 셉니다 — 여기서는 각각이 이므로 둘 다 맨몸으로 출력되며, 계수가 였다면 같은 출처를 사용하는 서로 다른 두 경로가 있음을 알려 주었을 것입니다.
아직 풀리지 않은 부분
위의 모든 해석은 고정점의 독스트링(docstring)에 있는 조용한 단어 하나에 기대고 있었습니다: 이 프로그램은 비순환적(acyclic)이라는 것입니다. 인용 그래프는 유향 비순환 그래프(directed acyclic graph)이므로, reach(p3, p1)은 유한하게 많은 유도만을 가지며 다항식 는 유한한 대상입니다. 역방향 엣지 하나를 더해 보십시오 — 이를테면 p1도 p3를 인용하여 논문들이 순환적으로 인용한다고 하면 — reach(p3, p1)은 무한히 많은 유도를 얻게 됩니다: 고리를 한 번, 두 번, 얼마든지 도는 만큼입니다. 불(Boolean), Which, Why 해석은 여전히 수렴하는데, 진리값이나 유한한 토큰 집합의 합집합은 결국 안정되기 때문입니다. 그러나 다항식 해석은 그렇지 않습니다: 그 "완전한 회계"는 무한한 형식적 거듭제곱급수(formal power series)가 될 것이고, 평범한 반환에는 그것을 이름 붙일 방법이 없습니다. 코드는 이 경계에 대해 정직합니다 — max_iter 라운드가 지나도록 고정점에 이르지 못하면 거짓말을 하기를 거부하고 RuntimeError("annotated fixpoint did not converge (cyclic provenance?)")를 일으킵니다(annotated.py, 96번째 줄). 따라서 재귀적 유래는 진짜 선택을 강요합니다: 비순환적 질의로 제한하거나, 실제로 수렴하는 더 성긴 반환으로 내려가거나, 무한합이 정의된 값을 갖는 -연속 구조와 형식적 거듭제곱급수로 옮겨 가야 합니다 [2]. 가장 많은 정보를 담은 레이블이야말로 유한하게 유지하기 가장 어려운 바로 그것입니다 — 공짜로 풀리지 않는 긴장입니다.
왜 중요한가
유래는 감사 가능성(auditability)이며, 감사 가능성은 신경-기호 최전선이 신경망 쪽에서 가장 뚜렷하게 결여하고 있는 속성입니다. 1권이 미해결로 남겨 둔 날카로운 트레이드오프(trade-off)를 떠올려 보십시오: 기호적 추론은 구성상 설명 가능한 반면 학습된 모델은 기본적으로 불투명합니다 — 그것들은 읽을 수 있는 이유 없이 답만 건네줍니다. 유래로 주석이 달린 사실은 기호적 절반에서 바로 그 틈을 메웁니다. 어떤 추론기가 한 논문이 다른 논문을 전이적으로 인용한다고 결론지을 때, 그것은 그저 단언만 하는 것이 아닙니다; 다항식 는 그 결론이 의존하는 기초 엣지와 경로의 이름을 댑니다. 여러분은 그것을 감사할 수 있습니다: 토큰 를 철회하면 두-홉 증인은 무너지지만 직접 증인 는 살아남으므로 그 사실은 그대로 성립합니다 — 대수는 각 출처가 어떤 결론을 뒷받침하는지를 미리 말해 줍니다 [3]. 그것이 바로 신경망이 만들어 낼 수 없는 설명에 대응하는 기호적 대응물이며, 답을 그저 내놓는 것이 아니라 정당화해야 하는 하이브리드 시스템이 정확히 이 장치를 찾게 되는 이유입니다.
두 개의 유도를 가진 하나의 도달가능성 사실을, 네 개의 반환을 통해 한꺼번에 읽어 봅니다: 직접 토큰 t는 하나의 더하기-곱하기 대수 아래에서 두-홉 곱 r 곱하기 s와 결합하며, 대수를 바꾸어 끼우면 같은 유도가 진리값, 토큰 집합, 증인 집합들의 집합, 또는 완전한 유래 다항식으로 다시 출력됩니다.
저자가 AI의 도움을 받아 직접 제작한 원본 도해.
핵심 용어
- 가환 반환(commutative semiring) — 결합법칙과 교환법칙을 만족하는 "더하기"와 "곱하기", 항등원 과 , 분배법칙, 그리고 아래에서 소멸하는 을 가진 레이블의 집합; 뺄셈이 없는 환(ring)이므로 증거는 결합되지만 결코 상쇄되지 않습니다.
- (곱하기) / (더하기) — 몸체-논리곱 연산자(규칙 몸체의 모든 사실이 필요함)와 대안-유도 연산자(어느 한 유도만으로도 충분함)입니다.
- 유래 토큰(provenance token) — 각 기초 사실에 붙는 고유한 레이블(세 엣지 위의 , , )로, 도출된 사실의 레이블이 그것이 사용한 출처의 이름을 대게 해 줍니다.
- 주석 달린 고정점(annotated fixpoint,
provenance_lfp) — 반환 값을 실어 나르는 데이터로그 최소 고정점 루프로, 한 라운드가 아무것도 더하지 못할 때까지 각 사실의 유도에 대한 -곱을 로 합산합니다. - 불(Boolean) / Which / Why / — 세부 정보가 점점 늘어나는 네 개의 레이블 대수입니다: 성립하는가, 어떤 토큰인가, 어떤 증인 집합인가, 완전한 다항식인가; 가 가장 많은 정보를 담고 있고, 불(Boolean)과 Why는 그것의 준동형사상 상(homomorphic image)이며 Which는 하나뿐인 퇴화된 계보 모서리(이어서 소멸이 실패하는 경우)입니다.
- 증인 집합(witness set) — 사실을 증명하는 하나의 자족적인 토큰 묶음; Why-유래는 대안적 증인 집합들의 집합이며, 여기서는 와 입니다.
- 유래 다항식(provenance polynomial) — 레이블, 예컨대 ; 단항식은 유도이고, 차수는 경로 길이이며, 계수는 서로 다른 유도의 개수를 셉니다.
- EDB / IDB — 단언된 기초 사실(외연적)과 도출된 사실(내포적); 기초 토큰은 매 라운드마다 그대로 유지되는 반면 도출된 레이블은 다시 계산됩니다.
- 감사 가능성(auditability) — 유래가 얻어 주는 신뢰 속성: 도출된 사실이 자신이 의존하는 기초 사실과 경로의 이름을 대는 것이며, 이는 신경망 모델이 줄 수 없는 설명입니다.
이 장이 이끄는 곳
다시 그 실행을 살펴보십시오: 네 개의 유래 레이블 아래에 다섯 번째 줄, Confidence : 0.8이 놓여 있었습니다. 그것은 반환 에서 평가된, 같은 그래프 위의 같은 고정점입니다 — 여기서 레이블은 단위 구간 안의 진리 정도(degree)이고, 는 이며(사슬은 가장 약한 연결만큼만 강하므로, 입니다), 는 입니다(대안 중 최선이므로, 입니다). provenance_lfp 안에서는 아무것도 바뀌지 않았습니다; 오직 대수만 바뀌었고, 그 결과 유래 대신 신뢰도가 나왔습니다. 그것이 이 틀 전체의 핵심이자 다음 장으로 가는 문입니다: 유래와 등급이 매겨진 진리는 하나의 구성물이며, 어떤 반환을 끼워 넣는지에 의해서만 구별됩니다. 다음 장인 주석 논리는 그 의 실마리를 데이터베이스 유래 밖으로 이끌어 내어 주석 논리와 퍼지 추론(fuzzy reasoning) 속으로 들어가는데, 거기서 레이블은 더는 출처에 대한 장부 기록이 아니라 규칙이 존중해야 하는 진짜 믿음의 정도가 됩니다.