지식그래프에 온도·압력처럼 시간에 따라 변하는 물리 현상을 결합해, 하나의 질의로 '안전하게 도달 가능한지'와 '누가 담당자인지'를 동시에 물어볼 수 있게 했다
지식그래프에 온도·압력처럼 시간에 따라 변하는 물리 현상을 결합해, 하나의 질의로 '안전하게 도달 가능한지'와 '누가 담당자인지'를 동시에 물어볼 수 있게 했다
RDF로 만든 지식그래프는 오븐, 버튼, 담당 기술자 같은 정적인 정보는 잘 표현하지만, 온도가 시간에 따라 어떻게 변하는지 같은 동적인 물리 법칙은 다루지 못한다. 연구팀은 RDF와 미분방정식 기반 검증 언어인 dL(Differential Dynamic Logic)을 연결한 RDFdL 프레임워크를 만들어, 정적 정보와 동적 물리 현상을 하나의 그래프 질의로 함께 물어볼 수 있게 했다. 실제로 오븐, 요거트 생산 라인, 드럼보일러, 탱크 시스템 등 여러 사례에 적용해 검증 결과가 그래프 데이터로 자연스럽게 녹아드는 것을 보였다.
METAL MEDIA 해설 도표
지식그래프에 온도·압력처럼 시간에 따라 변하는 물리 현상을 결합해, 하나의 질의로 '안전하게 도달 가능한지'와 '누가 담당자인지'를 동시에 물어볼 수 있게 했다
- 01오븐이 켜졌을 때 온도가 특정 범위에 안전하게 도달할 수 있는지 같은 질문은 기존 RDF나 SPARQL만으로는 답할 수 없었다. 온도 변화는 미분방정식으로 표현되는데 RDF는 이런 연속적 변화의 의미를 다루지 못하기 때문이다
- 02연구팀은 온도 범위와 장치 모드(켜짐/꺼짐 등)를 조합한 '상태 영역'을 RDF와 SHACL로 표현하고, 이를 dL 수식으로 자동 번역하는 파이프라인을 만들었다. Apache Jena가 RDF 추론을 담당하고, dL 정리증명기인 KeYmaera X가 실제 검증을 수행한다
- 03핵심 아이디어는 두 후보 상태 사이의 전이(transition)를 곧바로 사실로 받아들이지 않고, dL 증명 의무로 바꿔 KeYmaera X에 검증을 맡긴 뒤, 증명에 성공한 전이만 :next, :modeChange라는 관계로 RDF 그래프에 새로 추가(entailment)하는 것이다. 이렇게 되면 SPARQL의 property path 질의로 여러 단계를 거치는 도달 가능성 질문까지 답할 수 있다
- 04오븐, 요거트 생산라인(14단계 상태 변화), 산업용 드럼보일러, 두 개의 탱크가 교차 연결된 비선형 시스템 등 여러 사례로 평가했다. 선형적인 동역학을 가진 사례들은 상태 수가 늘어나도 증명 의무 개수가 거의 선형적으로 증가했고, 비선형 탱크 시스템처럼 복잡한 경우도 모든 증명을 성공적으로 완료했다
- 05SHACL은 실시간으로 들어오는 관측값(예: 현재 온도 185도, 꺼짐 상태)이 어떤 상태 영역에 해당하는지 걸러내는 역할을 하고, 실제 도달 가능성과 안전성 증명은 dL이 담당하는 식으로 역할을 분리했다
무엇을 했나
- 오븐이 켜졌을 때 온도가 특정 범위에 안전하게 도달할 수 있는지 같은 질문은 기존 RDF나 SPARQL만으로는 답할 수 없었다. 온도 변화는 미분방정식으로 표현되는데 RDF는 이런 연속적 변화의 의미를 다루지 못하기 때문이다
- 연구팀은 온도 범위와 장치 모드(켜짐/꺼짐 등)를 조합한 '상태 영역'을 RDF와 SHACL로 표현하고, 이를 dL 수식으로 자동 번역하는 파이프라인을 만들었다. Apache Jena가 RDF 추론을 담당하고, dL 정리증명기인 KeYmaera X가 실제 검증을 수행한다
- 핵심 아이디어는 두 후보 상태 사이의 전이(transition)를 곧바로 사실로 받아들이지 않고, dL 증명 의무로 바꿔 KeYmaera X에 검증을 맡긴 뒤, 증명에 성공한 전이만 :next, :modeChange라는 관계로 RDF 그래프에 새로 추가(entailment)하는 것이다. 이렇게 되면 SPARQL의 property path 질의로 여러 단계를 거치는 도달 가능성 질문까지 답할 수 있다
- 오븐, 요거트 생산라인(14단계 상태 변화), 산업용 드럼보일러, 두 개의 탱크가 교차 연결된 비선형 시스템 등 여러 사례로 평가했다. 선형적인 동역학을 가진 사례들은 상태 수가 늘어나도 증명 의무 개수가 거의 선형적으로 증가했고, 비선형 탱크 시스템처럼 복잡한 경우도 모든 증명을 성공적으로 완료했다
- SHACL은 실시간으로 들어오는 관측값(예: 현재 온도 185도, 꺼짐 상태)이 어떤 상태 영역에 해당하는지 걸러내는 역할을 하고, 실제 도달 가능성과 안전성 증명은 dL이 담당하는 식으로 역할을 분리했다
| dL Formulas (φ,ψ) | |
|---|---|
| Syntax | Meaning |
| [α]φ | After all runs of α, φ holds (safety) |
| ⟨α⟩φ | Some run of α reaches a state where φ holds (liveness) |
| φ∧ψ | Conjunction (and) |
| φ∨ψ | Disjunction (or) |
| φ→ψ | Implication |
| φ↔ψ | Biimplication (equivalence) |
| Hybrid Programs (α,β) | |
| Syntax | Meaning |
| α;β | Sequential: do α then β |
| α∪β | Choice: execute either α or β |
| x:=t | Discrete assignment: set x to the value of t |
| {x′=t,y′=s&Q} | Continuous evolution: x˙=t,y˙=s within domain Q |
| SHACL constraint | dL literal |
|---|---|
| sh:hasValue | x=c |
| sh:minInclusive | x≥c |
| sh:maxInclusive | x≤c |
| sh:minExclusive | x>c |
| sh:maxExclusive | x<c |
| Symbol | Meaning |
|---|---|
| p | URI of a numeric evolving variable, e.g. ex:T |
| f,v | SHACL constraint components and their literal values |
| θf | Comparison operator mapped from f (Table 2) |
| 𝗆𝗈𝖽𝖾d | Current mode of device d |
| Md | Finite set of modes declared for device d |
| 𝐟 | ODE derivatives (:derivative) |
| Q(𝐱) | Evolution-domain constraint |
| Use Case | States | Modes | State Transitions. | Correct Transitions. | dL Obligations. | Sound / Global Inv. |
|---|---|---|---|---|---|---|
| Oven | 4 | 2 | 4 | 4 | 40 | Yes/Yes |
| Empty Tank | 5 | 2 | 4 | 4 | 36 | Yes/Yes |
| Yogurt | 14 | 8 | 18 | 18 | 350 | Yes/Yes |
| Drumboiler | 5 | 2 | 4 | 4 | 40 | Yes/Yes |
| Domain | Real-time State | Matched State |
|---|---|---|
| Oven | Oven: On, x=60 | s12 |
| Oven | Oven: Off, x=150 | s11 |
| Oven | Oven: On, x=190 | s21 |
| Oven | Oven: Off, x=200 | s22 |
| Yogurt | Heater: On, x=45; Homogenizer: Off, p=9 | s112 |
| Yogurt | Heater: Off, x=50; Homogenizer: Off, p=8 | s122 |
| Yogurt | Heater: On, x=60; Homogenizer: On, p=15 | s311 |
| Yogurt | Heater: On, x=110; Homogenizer: Off, p=2 | s212 |
| Tank | Tank1: Off,h1=1.0 ; Tank2: Off,h2=0.1 | s0 |
| Tank | Tank1: On,h1=1.0 ; Tank2: On,h2=0.1 | s1 |
| Tank | Tank1: Off,h1=0.5 ; Tank2: Off,h2=0.5 | s2 |
| Tank | Tank1: On,h1=0.0 ; Tank2: On,h2=1.0 | s3 |
| Tank | Tank1: Off,h1=0.0 ; Tank2: Off,h2=1.0 | s4 |
왜 중요한가
제조 현장의 디지털 트윈처럼 장치 정보와 물리 법칙을 동시에 다뤄야 하는 시스템에서, 지금까지는 '누가 담당자인가' 같은 질문과 '이 전이가 물리적으로 안전한가' 같은 질문을 서로 다른 도구로 따로 물어야 했다. RDFdL은 이 둘을 하나의 질의 언어(SPARQL)로 합쳐, 검증된 물리적 동작을 그래프 데이터처럼 다룰 수 있는 길을 보여준다.
이 논문의 용어
- RDF · 사물과 관계를 '주어-서술어-목적어' 형태의 삼중항으로 표현하는 지식그래프 표준 데이터 모델
- SHACL · RDF 데이터가 특정 조건(모양)을 만족하는지 검증하는 제약 조건 언어
- SPARQL · RDF 그래프에서 원하는 패턴을 검색하는 질의 언어
- Differential Dynamic Logic(dL) · 미분방정식으로 표현되는 연속적 변화와 이산적인 모드 전환이 섞인 하이브리드 시스템의 안전성·도달 가능성을 증명하는 논리 언어
- KeYmaera X · dL 수식을 실제로 증명해주는 정리증명 소프트웨어
- entailment(함의) · 명시적으로 적힌 사실이 아니라 추론을 통해 참이라고 도출된 사실을 그래프에 새로 추가하는 것
최신 논문
- AI 코딩 에이전트에게 과학 소프트웨어 수리를 시켜보니, 절반도 제대로 못 고쳤다AI 코딩 에이전트에게 과학 소프트웨어 수리를 시켜보니, 절반도 제대로 못 고쳤다
- 논문 속 시연이 아니라 실제 서비스에 넣을 수 있는 희소 어텐션 만들기논문 속 시연이 아니라 실제 서비스에 넣을 수 있는 희소 어텐션 만들기
- 고객상담 AI 상담원이 규정을 '한 번의 행동'이 아니라 '전체 절차'로 지키게 만드는 방법고객상담 AI 상담원이 규정을 '한 번의 행동'이 아니라 '전체 절차'로 지키게 만드는 방법
- 로봇 팔에게 사람의 시연 없이 새 일 시키기, 말 잘하는 AI가 대신 가르친다로봇 팔에게 사람의 시연 없이 새 일 시키기, 말 잘하는 AI가 대신 가르친다
- 에이전트 학습용 환경을 새로 만드는 대신, 기존 환경에 '패치 부품'을 씌워 그 에이전트의 약점에 맞게 바꾸는 방법에이전트 학습용 환경을 새로 만드는 대신, 기존 환경에 '패치 부품'을 씌워 그 에이전트의 약점에 맞게 바꾸는 방법
- AI 모델을 '소유'하지 못한 조직은 안전 통제도 절반밖에 못 한다AI 모델을 '소유'하지 못한 조직은 안전 통제도 절반밖에 못 한다
- AI가 선생님 모델을 따라 배우다가, 정답에 다가가는 '좋은 생각'까지 억누르는 문제를 잡아낸다AI가 선생님 모델을 따라 배우다가, 정답에 다가가는 '좋은 생각'까지 억누르는 문제를 잡아낸다
- AI가 특정 사람 말투를 흉내내도록 시켜봤더니, 결국 AI 자신의 말투에서 못 벗어난다AI가 특정 사람 말투를 흉내내도록 시켜봤더니, 결국 AI 자신의 말투에서 못 벗어난다
METAL MEDIA 최신 기사
그림 출처: Yuyang Li et al., arXiv:2608.18165, CC BY 4.0