[Paper] Shapley Values를 이용한 이벤트 로그에서 추출된 계층적 워크플로우의 설명 가능한 검증

Source: arXiv - 2512.09562v1

Overview

이 논문은 자동으로 추출된 계층적 워크플로우를 형식 논리 사양으로 변환하고, 자동 정리 증명기(automated theorem provers)로 검증한 뒤, Shapley 값을 사용해 워크플로우가 안전성, 살아남음(liveness), 혹은 규정 준수와 같은 속성을 만족(또는 위반)하는 이유를 설명하는 새로운 파이프라인을 제시한다. 프로세스 마이닝과 게임 이론적 귀속(attribution)을 결합함으로써, 개발자들이 프로세스의 “좋은” 혹은 “나쁜” 부분을 정확히 찾아낼 수 있는 구체적인 방법을 제공한다.

Key Contributions

• Formal translation: 이벤트 로그에서 추출된 계층적 프로세스‑트리 모델을 자동 추론에 적합한 논리식으로 변환.
• Property verification: 상용 정리 증명기(오프‑더‑쉘프)로 만족성, 살아남음, 안전성 등을 검증하여 체계적인 규정 준수 검사를 가능하게 함.
• Shapley‑value attribution: 워크플로우 요소에 적용된 Shapley 값은 각 노드가 검증 결과에 얼마나 기여했는지를 정량적으로 보여주는 “설명 가능성” 레이어를 제공.
• Empirical validation: 표준 벤치마크 로그에서 이 방법이 전통적인 마이닝 도구가 놓치는 중요한 병목, 중복 분기, 해로운 패턴을 발견함을 입증.
• Prototype toolchain: 프로세스 마이닝, 정리 증명, 게임 이론적 분석을 통합한 프로토타입을 구현해 실제 파이프라인에서의 실현 가능성을 시연.

Methodology

1. Mining hierarchical workflows – 이벤트 로그를 입력으로 최신 프로세스‑트리 마이너(예: Inductive Miner)가 내부 노드에 제어 흐름 연산자(시퀀스, 병렬, 선택, 루프)를, 리프에 활동을 매핑한 중첩 트리를 생성한다.
2. Logical encoding – 각 연산자를 시계열/일차 논리 조각(예: 시퀀스에 대해 “A → ◇B”)에 매핑한다. 전체 트리는 하나의 논리 사양이 된다.
3. Automated verification – 사양을 SMT 또는 SAT 기반 정리 증명기(Z3, CVC5 등)에 전달해 사용자가 정의한 속성(예: “모든 주문은 결국 Ship 단계에 도달한다”)이 유지되는지 확인한다.
4. Shapley‑value computation – 워크플로우 노드 집합을 협력 게임으로 간주한다: 특정 노드 집합만 남겼을 때 속성이 만족되면 그 연합의 “값”은 1, 그렇지 않으면 0. 주변 기여도를 열거(또는 근사)함으로써 각 노드는 최종 검증 결과에 대한 영향을 나타내는 Shapley 점수를 받는다.
5. Interpretation & visualization – 높은 양수 점수를 가진 노드는 정확성을 “보호”하는 요소이며, 높은 음수 점수는 위험하거나 중복된 구성을 나타낸다. 저자들은 이러한 점수를 프로세스 트리 위에 직접 시각화하였다.

Results & Findings

• BPI Challenge 로그에서, 이 접근법은 안전성 속성을 위반하는 핵심 노드를 **≤5 %**만 식별했으며, 이는 수작업으로 발견한 버그와 일치하지만 훨씬 적은 노력으로 가능했다.
• Redundancy detection: 여러 로그에서 병렬 분기가 거의 0에 가까운 Shapley 값을 보여, 정확성을 해치지 않으면서 병합할 수 있음을 시사한다.
• Performance: 검증 + Shapley 분석을 결합한 전체 파이프라인이 200노드 이하의 트리에서 30 초 미만에 실행되어 전형적인 기업 프로세스에 대한 확장성을 입증했다.
• Explainability: 개발자는 실패한 규정 준수 검사를 단일 루프 구문(예기치 않은 데드락을 초래)으로 추적할 수 있었으며, 이는 원시 이벤트 로그 통계만으로는 드러나지 않았다.

Practical Implications

• Compliance automation – 기업은 이 파이프라인을 CI/CD에 삽입해 GDPR 등 규제 규칙 위반을 자동으로 감지할 수 있다.
• Process optimization – 영향력이 낮거나 해로운 노드를 강조함으로써 엔지니어는 워크플로우를 리팩터링하고, 불필요한 분기를 제거해 실행 시간 및 자원 소비를 줄일 수 있다.
• Debugging complex orchestrations – 마이크로서비스 오케스트레이터(BPMN, Camunda, Temporal)에서 생성되는 대규모 실행 그래프에 대해 Shapley 기반 귀속은 살아남음 실패에 책임이 있는 서비스를 “히트맵” 형태로 제공한다.
• Tool‑chain integration – 프로토타입을 REST 서비스로 래핑하면 기존 프로세스 마이닝 플랫폼(ProM, Celonis 등)이 정리 검증 및 설명 가능한 점수를 요청할 수 있다.
• Education & documentation – 신규 팀원이 워크플로우가 안전한 이유를 Shapley 점수를 통해 바로 이해함으로써 온보딩과 지식 전달이 가속화된다.

Limitations & Future Work

• Scalability of exact Shapley computation – 전체 연합을 평가하는 비용이 지수적으로 증가하므로 현재 구현은 Monte‑Carlo 샘플링에 의존한다. 매우 큰 트리에서는 분산도(variance)가 커질 수 있다.
• Property expressiveness – 현재 논리 인코딩은 제한된 시계열 속성만 지원한다. 정량적 시간 제한 등 더 풍부한 사양을 위해서는 인코딩 확장이 필요하다.
• Noise in event logs – 마이닝 오류(누락·오류 이벤트)가 논리 모델에 전파되어 Shapley 점수가 왜곡될 수 있다. 견고한 전처리 기법이 아직 해결 과제이다.
• User‑defined property selection – 프레임워크는 분석가가 올바른 논리 술어를 정의한다는 전제하에 동작한다. 향후 연구는 도메인 온톨로지를 기반으로 관련 속성을 자동 제안하는 방안을 모색한다.

Bottom line: 불투명한 마이닝 워크플로우를 검증 가능하고 설명 가능한 아티팩트로 전환함으로써, 이 연구는 개발자들이 감사, 디버깅, 개선을 코드 수준의 엄격함으로 수행할 수 있는 실용적인 길을 연다.

Authors

• Radoslaw Klimek
• Jakub Blazowski

Paper Information

• arXiv ID: 2512.09562v1
• Categories: cs.SE, cs.IT
• Published: December 10, 2025
• PDF: Download PDF