추론 벤치마크: LUBM, OWL2Bench, ORE
📍 현재 위치: 5부 · 실전 추론기 — 17장. 데이터로그와 DL 엔진은 생산 엔진들을 정리하여 — 규칙을 포화시키는 RDFox, 모델을 탐색하는 HermiT와 Konclude — 두 계열로 나누고, 이들이 다루기 쉬운 논리에 대해서는 동일한 고정점을 계산한다는 것을 보였습니다; 그 장은 스스로 답할 수 없었던 질문으로 끝났습니다 — 실제로 어떤 엔진을 써야 하며, 그것을 어떻게 알 수 있는가? 이 장은 그 질문에 답하는 도구를 만듭니다.
두 추론기가 둘 다 정확하면서도 속도에서는 자릿수 단위로 차이가 날 수 있습니다; 또 다른 두 추론기는 둘 다 빠르면서도 답에서는 조용히 어긋날 수 있습니다. "내 온톨로지에서는 빠르게 느껴졌다"는 말은 그 어느 격차에 대해서도 아무것도 말해 주지 않습니다 — 그것은 측정이 아니라 일화(anecdote)인데, 온톨로지도 하드웨어도 작업도 결코 고정되지 않았고 그 주장 중 어떤 것도 다시 실행할 수 없기 때문입니다. 그 일화를 대체하는 것이 바로 벤치마크(benchmark)입니다: 모든 추론기가 동일한 규칙 아래에서 실행하는 고정된 데이터셋과 고정된 작업으로, 이로써 "더 빠르다"와 "더 정확하다"는 자랑거리이기를 멈추고 누구나 재현할 수 있는 숫자가 됩니다. 이 장은 온톨로지 추론을 형성해 온 세 가지 벤치마크 — LUBM, OWL2Bench, ORE — 를 살펴보고, 이 셋 모두가 핵심만 남기고 나면 동반 코드가 하나의 작은 온톨로지 위에서 측정하는 것과 똑같은 두 가지 — 정확성과 속도 — 를 측정한다는 것을 보입니다.
모든 주자가 같은 오후에, 같은 스톱워치로 시간이 재어지는, 같은 측정된 트랙을 달리는 학교 체육대회를 상상해 보십시오. 공유된 트랙이 없다면 "내가 더 빠르다"는 그저 주장일 뿐입니다; 트랙이 있으면 누구나 하나의 게시판에서 자신의 기록을 읽습니다. 추론 벤치마크는 추론기를 위한 바로 그 측정된 트랙입니다: 같은 온톨로지, 같은 질문, 같은 시계입니다. 이는 어느 엔진이 더 나은지에 관한 논쟁을 여러분이 확인할 수 있는 리더보드로 바꾸어 놓습니다 — 그리고 그만큼 중요하게도, 내일 다시 실행해 우승자가 여전히 우승하는지를 볼 수 있게 해 줍니다.
이 장에서 다루는 내용
- 벤치마크가 존재하는 이유 — 추론기들은 자릿수 단위로 성능이 다르고 서로 다른 프로파일을 다루므로, 공유된 데이터셋과 고정된 작업만이 이들을 비교할 수 있습니다; 증언(testimonial)은 그럴 수 없습니다.
- LUBM — 리하이 대학교 벤치마크(Lehigh University Benchmark): 열네 개의 고정된 질의 뒤에서 임의의 규모로 대학 도메인 데이터를 찍어내는 생성기이며, 고전적인 확장성(scalability) 시험이자 우리 학계 세계를 규모를 키운 사촌 격입니다.
- OWL2Bench — 프로파일을 인식하는 벤치마크로, 각 OWL 2 프로파일(EL, QL, RL, DL)을 부하 시험하여, 추론기가 정확히 자신이 지원한다고 주장하는 바에 대해서만 평가받도록 합니다.
- ORE — OWL 추론기 평가(OWL Reasoner Evaluation) 경연: 실제 온톨로지 말뭉치(corpus) 위에서 분류(classification), 일관성(consistency), 충족 가능성(satisfiability)을 겨루며, 정확성과 시간으로 순위를 매깁니다.
- 두 지표 해독하기 — 정확성(출력이 신뢰할 수 있는 골드 스탠다드와 일치하는가?)과 성능(실제 경과 시간, 메모리, 확장), 그리고 정확성이 더 어려운 지표인 이유 — 참조 기준(reference)이 필요하기 때문입니다.
- 하나의 온톨로지로 이루어진 벤치마크로서의 동반 코드 — 우리의 정확성 지표는
classify()와 HermiT의 정확한 일치입니다: 8개의 포섭 관계, 2개의 충족 불가능한 개념, 일치 확인됨.
왜 벤치마크인가: 증언은 추론기를 비교할 수 없다
이전 장의 엔진들은 서로 바꿔 쓸 수 있는 것이 아닙니다. 같은 입력에 대해서도 이들은 속도에서 자릿수(orders of magnitude) 단위로 벌어지며; 서로 다른 OWL 2 프로파일 — 웹 온톨로지 언어(Web Ontology Language)의 표준화된 하위 언어들로, 각각이 표현력을 더 나은 최악의 경우 비용과 맞바꾼 것 — 을 차지하고; 서로 다른 질문에 맞추어 조율되어 있습니다. EL 전문 분류기가 생의학 용어 체계를 몇 초 만에 끝내는 반면 완전한 DL(서술 논리, Description Logic) 추론기는 몇 분씩 애쓸 수도 있으며, 데이터베이스 규모의 ABox 위에서 동작하는 질의 엔진은 분류기가 결코 마주치지 않는 작업을 위해 만들어진 것입니다. 이런 도구들을 증언으로 비교하는 일은 가망이 없습니다: 온톨로지도 다르고, 하드웨어도 다르며, 작업은 모호하게 남아 있고, 논쟁을 매듭지을 아무것도 다시 실행되지 않습니다.
벤치마크는 이러한 자유도를 하나도 남김없이 제거합니다. 그것은 세 가지를 고정합니다 — (i) 데이터셋(dataset): 그대로 주어지거나 씨앗(seed)으로부터 재현 가능하게 생성된 온톨로지; (ii) 작업(task): 분류, 일관성 확인, 질의 응답과 같이 단 하나의 정답을 갖도록 충분히 정확하게 정의된 것; 그리고 (iii) 프로토콜(protocol): 실행 시간을 어떻게 재고 무엇이 정답으로 간주되는지를 명시한 것. 이 삼중항(triple)을 고정하면, 실제로 중요한 두 속성이 동등한 조건 위에서 측정 가능해집니다:
아래의 각 벤치마크는 그 삼중항을 서로 다르게 선택한 것으로, 소박한 비교의 서로 다른 약점을 겨냥하지만, 셋 모두 동일한 출력 쌍에 안착합니다. 우리는 이들을 이 분야가 구축해 온 순서대로 다루겠습니다.
LUBM: 데이터는 확장하고, 질의는 고정하라
리하이 대학교 벤치마크(Lehigh University Benchmark, LUBM)는 OWL 지식베이스 시스템을 위한 최초의 확장성 시험입니다 [1]. 그 심장은 데이터 생성기(data generator)입니다: 목표로 하는 대학교 수와 난수 씨앗(random seed)이 주어지면, 이는 결정론적으로 학과, 정교수와 조교수, 대학원생과 학부생, 강좌, 출판물, 그리고 이들 사이의 지도(advising), 강의, 소속(member-of) 관계로 이루어진 합성 대학 세계를 찍어냅니다. 대학교 하나에서 천 개로 다이얼을 돌려도 같은 스키마가 비례하여 더 큰 ABox(기초 단언들)를 만들어 내므로, 손잡이 하나만으로 데이터셋을 작은 인스턴스에서부터 1억 개를 훌쩍 넘는 단언을 가진 것에 이르기까지 훑을 수 있으며, 그동안 스키마 — Univ-Bench 온톨로지 — 는 처음부터 끝까지 고정된 채로 유지됩니다.
작업은 질의 응답(query answering)입니다. LUBM은 그 온톨로지 위에서 열네 개의 고정된 질의를 제공하며, 이는 단순한 테이블 조회가 아니라 하위 개념 계층을 따라가고, advises와 member-of 관계를 뒤쫓고, 이행성(transitivity)을 적용하는 등 진정한 추론을 요구하도록 골라진 것들입니다. 여기서 생성기는 ABox만 내놓을 뿐 정답표(answer key)는 내놓지 않습니다; 골드 스탠다드는 다른 출처에서 공짜로 옵니다. 데이터가 합성물이고 Univ-Bench의 의미론이 고정되어 있으므로, 각 질의에 대한 정답 집합은 구성 그 자체로부터 알려져 있습니다 — 결정론적 데이터와 고정된 온톨로지로부터 오라클(oracle) 없이도 정확하게 계산할 수 있습니다. 그 공짜 골드 스탠다드는 흔치 않은 사치이며 — ORE에서 보게 되듯 — 온톨로지가 생성된 것이 아니라 실제의 것이 되는 순간 사라져 버리는 것이기도 합니다.
우리가 계속 사용해 온 예시와의 친연성은 장식이 아닙니다; 그것은 규모만 커진 같은 세계입니다. 우리 온톨로지의 사슬 Professor ⊑ Researcher ⊑ Person, 그 advises 역할, 그리고 역할 사슬 advises ∘ advises ⊑ grandAdvisor는 LUBM의 교수/학생 계층과 지도 관계를 손바닥만 한 크기로 줄인 판본입니다. 동반 코드가 13개의 개체를 가진 곳 — python3 ontology.py를 실행하면 10 named concepts, 6 roles, 14 TBox axioms; ABox: 13 concept assertions, 18 role assertions over 13 individuals.가 출력됩니다 — 에서, LUBM은 똑같은 형태를 수백만 개의 엣지로 풀어낸 것입니다. 바로 이것이 LUBM을 추론 시험이 아니라 확장성 시험으로 만드는 이유입니다: 각 질의가 필요로 하는 추론은 쉬우며, 양(volume)이야말로 도전 과제이고, 지표는 ABox가 커짐에 따라 시간과 메모리 곡선이 어떻게 휘어지는가입니다.
OWL2Bench: 스스로 주장하는 프로파일로 평가받다
LUBM은 OWL 2보다 앞서 나왔고 하나의 모델링 스타일만을 단련합니다. OWL2Bench는 더 좁은 범위의 불공정함을 바로잡기 위해 만들어졌습니다: 추론기는 자신이 실제로 구현한 프로파일을 기준으로 시험받아야 하며, 다루겠다고 약속한 적도 없는 구성자를 기준으로 시험받아서는 안 됩니다 [2]. OWL 2는 세 개의 다루기 쉬운 프로파일에 완전한 서술 논리를 더해 정의하며, 각각은 서로 다른 임무를 위해 설계되었습니다:
- OWL 2 EL — EL 계열(우리 완성 알고리즘의 논리) 위에 세워졌습니다; 분류는 다항 시간에 머무르므로 SNOMED CT나 유전자 온톨로지(Gene Ontology)처럼 수십만 개의 클래스를 가진 용어 체계까지 확장됩니다.
- OWL 2 QL — DL-Lite 위에 세워졌습니다; 질의를 평범한 데이터베이스 질의로 재작성함으로써 거대한 ABox 위에서의 질의 응답에 맞추어져 있습니다.
- OWL 2 RL — 규칙 언어 파편(fragment)입니다; 추론은 전방 연쇄(forward-chaining) 규칙으로 실행되며, 이는 이전 장의 데이터로그 방식입니다.
- OWL 2 DL — 완전한 표현력을 가진 논리로, 결정 가능하지만 가혹한 최악의 경우 비용을 치릅니다.
OWL2Bench는 각 프로파일의 구성자를 단련하는 TBox를 (LUBM의 정신을 이어받은) 확장 가능한 ABox 생성기 및 SPARQL 질의 모음과 함께 제공하여, 추론기가 자신이 주장하는 프로파일 안에서 TBox 추론(분류, 일관성)과 ABox 추론(질의 응답) 양쪽 모두에 대해 측정될 수 있게 합니다. EL 추론기는 자신이 만들어진 목적인 EL 작업 부하에 대해서만 점수를 받으며, 자신의 소관 밖에 있는 구성자에 대해 불이익을 받지도, 빠진 기능을 숨기도록 허용되지도 않습니다. 세 벤치마크는 작업을 깔끔하게 나눕니다:
| 벤치마크 | 무엇을 부하 시험하는가 | 주요 지표 |
|---|---|---|
| LUBM | 하나의 고정된 대학 TBox 위에서 확장 가능한 ABox 질의 응답 | 적재 시간 + 질의 응답 시간; 답의 건전성과 완전성 |
| OWL2Bench | 프로파일별 추론(EL, QL, RL, DL), TBox 및 ABox, 대규모로 | 추론 시간 + 질의 시간, 프로파일별로 보고 |
| ORE | 실제 온톨로지 위에서의 분류, 일관성, 충족 가능성 | 정확성(참조 대비) + 실제 경과 시간 |
ORE: 실제 온톨로지를 둘러싼 경연
합성 데이터는 반복 가능하지만 길들여져 있습니다; 그것은 실제 추론기를 걸려 넘어지게 하는, 어색하고 손수 작성된 모델링을 좀처럼 담고 있지 않습니다. OWL 추론기 평가(OWL Reasoner Evaluation, ORE) 경연은 커뮤니티에서 모은 실제 온톨로지 말뭉치(corpus) 위에서 추론기들을 정면으로 맞붙게 하고 그 결과를 순위가 매겨진 경연으로 보고함으로써 그 간극을 메웠습니다 [3]. ORE는 각각 명확한 답을 가진 세 가지 표준 추론 작업을 고정했습니다:
- 분류(Classification) — 완전한 포섭 계층을 계산합니다: 이름 붙은 개념들 사이에서 함의되는 모든 입니다.
- 일관성(Consistency) — 온톨로지가 애초에 모델을 가지는지, 아니면 그 공리들이 서로 대놓고 모순되는지를 판정합니다.
- 충족 가능성(Satisfiability) — 주어진 클래스가 어떤 인스턴스든 가질 수 있는지, 아니면 우리의
TenuredStudent처럼 강제로 공집합이 되는지()를 판정합니다.
추론기들은 프로파일 트랙(DL, EL, RL) 안에서 경쟁했으므로, 저마다 비교 가능한 입력 위에서 동료들과 맞붙었고, 시간 제한 안에서 얼마나 많은 문제를 정확하게 풀었는지, 그리고 얼마나 빠르게 풀었는지로 순위가 매겨졌습니다. Konclude, HermiT, ELK, FaCT++, Pellet, JFact와 같은 이름 있는 엔진들이 하나의 말뭉치 위에서 하나의 시계 아래 모였고, 증언이 아니라 리더보드(leaderboard)가 순위를 결정했습니다.
ORE가 풀어야 했던 어려운 부분은 정확히 LUBM이 비켜 갔던 바로 그것입니다: 실제 온톨로지에는 정답표가 딸려 오지 않습니다. 웹에서 가져온 임의의 온톨로지의 참된 분류를 이미 알고 있는 오라클은 없습니다. ORE의 실용적인 해법은 다수결(majority vote)입니다 — 추론기들이 어떤 문제에 대해 의견이 갈릴 때, 대다수가 반환한 답을 참조 기준으로 삼고, 의견 불일치는 사람이 검토하도록 표시해 둡니다. 이는 불완전한 골드 스탠다드이지만 재현 가능한 것이며, 이는 어떤 수작업 정답표도 다다를 수 없는 규모에서 정확성을 점수화할 수 있게 해 줍니다.
두 지표 해독하기: 정확성과 성능
세 벤치마크를 갈라놓는 것들을 걷어내면 동일한 두 축만 남습니다.
성능(performance)은 정의하기 쉬운 축이며 요란하게 보고되는 축입니다. 그것은 작업을 마치는 데 걸리는 실제 경과 시간(wall-clock time), 최대 메모리(peak memory), 그리고 — LUBM이 바로 이것을 위해 만들어진 축인데 — 그 수치들이 입력 크기에 따라 어떻게 확장(scale)되는가입니다. 개의 단언으로 이루어진 ABox에서의 시간을 이라 쓰면: 잘 확장되는 추론기는 을 거의 선형으로 유지하는 반면, 최악의 경우 DL 추론은 지수적으로 치솟을 수 있으며, 이것이 바로 다루기 쉬운 프로파일들이 존재하는 정확한 이유입니다. 성능은 측정하기가 쉬운데, 스톱워치는 오라클을 필요로 하지 않기 때문입니다 — 그러나 빠르지만 틀린 답은 아무 가치가 없으며, 그래서 속도는 결코 혼자서만 보고되지 않습니다.
정확성(correctness)은 미묘한 축인데, 그것이 무언가에 비추어 옳아야 한다는 것 — 즉 골드 스탠다드(gold standard) — 를 전제하기 때문입니다. 분류와 같은 집합값(set-valued) 작업의 경우, 정확성은 추론기의 출력 집합 와 참조 집합 사이의 정확한 일치입니다. 대칭 차집합(symmetric difference) — 두 집합이 의견을 달리하는 항목들, 즉 한쪽에는 있지만 다른 쪽에는 없는 항목들 — 을 도입하면, 정확성은 단순히 다음과 같습니다
즉 빈 대칭 차집합입니다. 질의 응답에서는 정확성이 보통 정밀도(precision)와 재현율(recall)에서 빌려온 두 비율로 보고됩니다: 완전성(completeness)(참인 답을 전부 반환했는가?)과 건전성(soundness)(반환한 답이 전부 실제로 참이었는가?)입니다,
이 둘은 반환된 집합이 정답 집합과 같을 때 정확히 함께 1에 도달합니다. 정확성이 안고 있는 모든 어려움 — 그리고 LUBM은 그럴 필요가 없는데 ORE는 다수결이 필요한 모든 이유 — 은, 정답인 가 어느 공식이든 의미를 갖기 전에 신뢰할 수 있는 어딘가로부터 와야만 한다는 것입니다.
축소판 벤치마크로서의 동반 코드
동반 코드는 하나의 온톨로지 위에서, 골드 스탠다드를 대신하는 신뢰할 수 있는 참조와 함께, 정확히 이 정확성 측정을 실행합니다. 모듈 reasoners.py는 owlready2로 학계 세계를 다시 구축하고, sync_reasoner(reasoners.py 99번째 줄)를 통해 HermiT — 완전한 OWL 2 DL 추론기이므로 EL의 엄격한 상위 집합이자 사용 가능한 가장 강력한 오라클 — 를 구동하며, 처음부터 작성한 결과와 직접 비교할 수 있도록 그 분류 결과를 이름 붙은 개념들 사이에서만 다시 읽어 들입니다(reasoner_classification, reasoners.py 94–113번째 줄). 그런 다음 HermiT의 출력을 classify()와 항목별로 비교합니다. 그 비교는 파이썬으로 작성된 빈 대칭 차집합 검사입니다(reasoners.py 145–151번째 줄):
subs_agree = r_subs == el_subs
unsat_agree = r_unsat == el_unsat
print(f"\n subsumptions agree : {subs_agree}")
print(f" unsatisfiable agree: {unsat_agree}")
assert subs_agree, ("subsumption mismatch", r_subs ^ el_subs)
assert unsat_agree, ("unsat mismatch", r_unsat ^ el_unsat)
코드에서 두 축을 읽어내십시오. 각 ==는 검사 입니다 — 한 번은 포섭 집합에 대해, 한 번은 충족 불가능한 클래스 집합에 대해 — 그리고 각 assert 메시지 안의 ^는 파이썬의 대칭 차집합 연산자 이므로, 실패한다면 어긋난 항목들을 정확히 출력하게 됩니다. 그런 일은 결코 일어나지 않습니다. python3 reasoners.py의 커밋된 출력은 두 항목 모두에서 깔끔한 일치를 보여줍니다:
Reasoner (HermiT via owlready2) vs. from-scratch EL completion
from-scratch subsumptions : 8
HermiT subsumptions : 8
from-scratch unsatisfiable: ['TenuredStudent', 'TenuredStudentAdvisor']
HermiT unsatisfiable : ['TenuredStudent', 'TenuredStudentAdvisor']
subsumptions agree : True
unsatisfiable agree: True
AGREEMENT CONFIRMED — the from-scratch reasoner matches HermiT.
이를 벤치마크 어휘 위에 겹쳐 놓으면 이것은 축소판 벤치마크입니다. 데이터셋은 14개 공리로 이루어진 하나의 온톨로지입니다; 작업은 ORE의 분류 트랙에 충족 가능성 검사를 더한 것입니다 — 두 개의 충족 불가능한 개념 TenuredStudent와 TenuredStudentAdvisor가 classify()의 충족 가능성 판정입니다; 골드 스탠다드는 다수결이 아니라 HermiT이며, 이는 ORE가 신뢰할 수 있는 추론기의 출력을 참조로 삼을 때와 똑같은 조치입니다; 그리고 정확성 점수는 8개의 포섭 관계와 2개의 충족 불가능한 클래스 양쪽 모두에서 완벽한 입니다. 이 하나의 온톨로지, 두 추론기짜리 벤치마크가 부하 시험을 하지 않는 것은 성능 축입니다 — 14개의 공리는 확장에 대해 아무것도 말해 주지 않습니다 — 그렇다 해도 비용 쪽 측면은 여기서도 희미하게나마 엿보입니다: classify()는 3라운드 만에 고정점에 도달하며, 이는 EL이 실제 용어 체계로 확장될 수 있게 해 주는 다항식적 상승입니다. 여기서 정확성이 인증되고, 속도는 그것을 담당하는 프로파일에게 미루어집니다: 이는 모든 진지한 벤치마크가 보고하는 것과 똑같은 분리입니다.
세 개의 벤치마크, 세 개의 데이터셋, 하나의 점수판: LUBM은 데이터를 확장하고, OWL2Bench는 프로파일로 관문을 걸며, ORE는 실제 온톨로지 위에서 순위를 매깁니다 — 그리고 모든 레인은 정확성과 시간이라는 같은 두 칸으로 귀결되며, 이는 동반 코드가 HermiT를 상대로 축소판에서 검사하는 바로 그 쌍입니다.
저자가 AI의 도움을 받아 직접 제작한 원본 도해.
아직 풀리지 않은 부분
이 페이지의 모든 벤치마크는 순수한 함의(plain entailment)를 채점합니다: 가 따라 나오는가, 온톨로지가 일관적인가, 클래스가 충족 가능한가 — 시간이 재어지고 집계되는 명확한 사실들입니다. 바로 그 점이 이들을 재현 가능하게 만들며, 동시에 바로 그 점이 이들을 어떤 사실이 참이라는 것 외에 지니고 있는 모든 것에 대해 눈멀게 만듭니다. 실제 지식은 주석이 달려 있습니다. 도출된 포섭 관계에는 유래(provenance) — 그것이 따라 나오려면 어떤 공리들이, 어떤 출처로부터, 성립해야 했는가 — 가 있습니다. 단언된 사실에는 신뢰도(confidence) — 큐레이터의 0.9, 학습된 모델의 소프트 점수 — 가 있습니다. 관계에는 시간(time) — 학위 과정 동안에는 참, 졸업 후에는 거짓 — 이 있습니다. LUBM도, OWL2Bench도, ORE도 이 중 어느 것도 측정하지 않는데, 그들의 골드 스탠다드가 불리언(Boolean)이기 때문입니다: 잘못된 이유로 옳은 답을 반환하는 추론기, 혹은 자신이 얼마나 확신하는지 말할 수 없는 추론기, 혹은 어떤 사실이 언제 성립했는지를 무시하는 추론기도 여전히 만점을 받습니다. 이 벤치마크들은 어떤 엔진이 메타데이터가 벗겨진 지식 위에서 정확하게 추론한다는 것을 정직하게 인증합니다 — 의도적으로 좁혀진 작업에 대한 충실한 측정입니다. 유래를 인식하고, 신뢰도를 인식하며, 시간을 인식하는 함의에 대해 골드 스탠다드를 정의하는 것조차 가능한지, 하물며 그것을 채점하는 벤치마크를 만드는 것이 가능한지는 아직 열려 있는 문제입니다 — 그리고 바로 그곳이 5부의 명확한 예-아니오가 6부의 주석 달린 추론에게 자리를 내주는 지점입니다.
왜 중요한가
벤치마크는 한 분야가 스스로 정직함을 유지하는 방법이며, 상징적 절반에 대한 정직함이야말로 신경-기호(neuro-symbolic) 프로그램이 정확히 필요로 하는 것입니다. 이후 권의 신경망 또는 미분 가능한 추론기가 포섭 관계를 그럴듯함(plausibility)으로 순위 매길 때, 그것이 얼마나 좋은지를 결정하는 질문은 무엇에 비추어 정확한가?이며 — 그 답은 벤치마크의 골드 스탠다드입니다: 건전하고 완전한(sound-and-complete) 추론기가 산출하는 정확한 분류로, 근사의 비용이 무엇인지 알 수 있도록 시간까지 재어진 것입니다. 두 축은 소프트 추론기에 대해서도 변함없이 되풀이되지만, 한 가지 반전이 있습니다. 신경망 모델은 HermiT와 달리 을 좀처럼 얻지 못하므로, 흥미로운 측정은 정확한 일치이기를 멈추고 그것이 얼마나 벗어나는지(에 대한 정밀도와 재현율)와 얼마나 빠른지가 됩니다. 그 벗어남은 그것을 빼서 구할 정확한 답 없이는 보고할 수 없으며, 그 정확한 답이야말로 동반 코드의 HermiT 교차 검증 — 그리고 그것이 축소판으로 보여주는 벤치마크들 — 이 존재하여 공급하는 것입니다. 벤치마크는 학습하는 절반이 그것에 비추어 측정되는 명세(specification)입니다; 그것이 없다면, 유창하지만 틀린 답은 옳은 답과 구별할 수 없습니다.
핵심 용어
- 벤치마크(Benchmark) — 추론기 비교를 정확성과 성능이라는 두 개의 재현 가능한 숫자로 환원하는, 고정된 (데이터셋, 작업, 프로토콜) 삼중항입니다.
- LUBM(리하이 대학교 벤치마크, Lehigh University Benchmark) — 열네 개의 고정된 질의 뒤에서 임의의 규모로 대학 도메인 ABox를 찍어내는 생성기입니다; 고전적인 확장성 시험이며, 학계 세계의 규모를 키운 사촌입니다.
- OWL2Bench — 각 OWL 2 프로파일(EL, QL, RL, DL)마다 TBox와 ABox를 갖춘, 프로파일을 인식하는 벤치마크로, 추론기는 오직 자신이 지원한다고 주장하는 것에 대해서만 평가받습니다.
- ORE(OWL 추론기 평가, OWL Reasoner Evaluation) — 실제 온톨로지 말뭉치 위에서 분류, 일관성, 충족 가능성에 대해 추론기의 점수를 매기는 경연으로, 정확성과 시간으로 순위가 매겨집니다.
- 정확성(Correctness) — 골드 스탠다드와의 정확한 일치로, 집합값 작업의 경우 이며, 질의 응답의 경우 건전성과 완전성(정밀도와 재현율)입니다.
- 성능(Performance) — 실제 경과 시간, 최대 메모리, 그리고 이들이 입력 크기 에 따라 어떻게 확장되는가입니다; 오라클이 필요 없으므로 측정하기 쉽습니다.
- 골드 스탠다드(Gold standard) — 정확성이 그것에 비추어 채점되는 신뢰할 수 있는 참조 답으로, LUBM의 합성 데이터에서는 구성 그 자체로부터 알려져 있고, ORE의 다수결로 근사되며, 동반 코드에서는 HermiT가 그 역할을 맡습니다.
- 대칭 차집합 (Symmetric difference) — 두 답 집합이 의견을 달리하는 항목들입니다; 추론기가 정확할 때 정확히 비어 있습니다.
이 장이 이끄는 곳
이 벤치마크들은 발가벗겨진 함의 — 옳은가 그른가, 빠른가 느린가 — 를 인증하며, 그렇게 함으로써 이들이 빠뜨리는 모든 것을 생생하게 드러냅니다: 어떤 사실이 왜 성립하는지, 우리가 그것을 얼마나 확신하는지, 그것이 언제 참인지 말입니다. 다음 장인 유래 반환은 그 세 가지 중 첫 번째를 이어받습니다. 이는 도출된 각 사실 곁에 그것을 만들어 낸 공리들의 대수적 기록을 지니게 하면서도 똑같은 고정점 추론을 실행하는 방법을 보여줍니다 — 그래서 reach(p3, p1)은 단순히 True만이 아니라, 그 배후의 두 가지 유도를 이름 붙인 다항식 t + r·s가 함께 태그되어 돌아옵니다. 추론은 발가벗은 예가 되기를 멈추고 주석이 달린 예가 되며, 5부의 명확한 세계는 6부의 더 풍요로운 세계로 열립니다.