Towards Neuro-symbolic Causal Rule Synthesis, Verification, and Evaluation Grounded in Legal and Safety Principles

"법적 및 안전 원칙에 기반한 신경-상징적 인과 규칙 합성, 검증 및 평가를 위한 연구"에 대한 상세한 기술 요약입니다.

1. 문제 제기

이 논문은 자율 주행, 산업 제어 등 안전-중요 분야에서 사용되는 규칙 기반 시스템의 치명적인 한계를 다룹니다:

• 취약성과 확장성: 전통적인 규칙 기반 시스템은 유지보수에 어려움을 겪습니다. 사소한 요구사항 변경이 종종 상호 의존적인 규칙 전반에 걸쳐 연쇄적인 수정을 유발하여 '지식 획득 병목 현상'을 초래합니다.
• 목표 오지정: AI 시스템은 종종 인간 설계자의 진정한 의도보다는 좁고 문자 그대로의 목표 (보상 해킹) 를 최적화합니다. 이는 인간의 목표가 종종 모호하고, 문맥에 의존하며, 비공식적인 반면, AI 는 정밀하고 형식적인 명세가 필요하기 때문에 발생합니다.
• 추적성 부재: 기존 방법들은 종종 고수준의 인간 원칙 (법적/안전) 과 시스템 행동을 지배하는 저수준의 논리 규칙 간의 명확하고 추적 가능한 연결고리가 부족합니다.

핵심 과제는 자연어 목표와 원칙에서 파생된 형식 규칙을 점진적으로 합성, 검증, 평가할 수 있는 시스템을 구축하여, 해당 규칙이 최소적, 필수적, 충분적이며 안전하도록 보장하는 것입니다.

2. 방법론

저자들은 이전의 신경 - 상징적 (NeSy) 인과 프레임워크를 확장한 것을 제안합니다. 새로운 아키텍처는 표준 MAPE-K(모니터 - 분석 - 계획 - 실행) 피드백 루프 위에 메타 레벨 합성 및 검증 계층을 도입합니다.

A. 핵심 아키텍처

이 시스템은 세 가지 표현 공간을 통합합니다:

1. 상징적 귀납 트리 (SAT): 도메인 지식을 인코딩하고 위반 사항을 설명하기 위한 1 차 논리 (FOL).
2. 구조적 인과 모델 (SCM): 의존성을 표현하고 반사실적 추론을 지원하기 위함.
3. 심층 강화 학습 (DRL): 운영적 의사결정을 위해 사용됨.

새로운 합성 및 검증 계층은 인간의 입력과 이상 탐지에 기반하여 시스템을 지배하는 FOL 이론을 업데이트하는 폐쇄된 메타 루프 역할을 합니다.

B. 합성 파이프라인 (목표/규칙 합성기)

이 파이프라인은 **대형 언어 모델 (LLM)**을 활용하여 자연어 목표를 형식 규칙으로 변환하는 네 단계를 거칩니다:

1. 원인 분해: LLM 은 안전 및 법적 원칙에 제약을 받아 달성하기 위해 필요한 조건/행동 (원인) 으로 고수준 목표 (결과) 를 분해합니다.
2. 의미 통합: LLM 은 중복되거나 반복되는 원인을 식별하고 병합하여 고유한 조건 집합을 생성함으로써 모호성을 줄입니다.
3. 상징적 번역: 통합된 자연어 원인은 1 차 논리 (FOL) 술어 및 규칙으로 번역됩니다. LLM 은 이러한 번역에 대한 설명을 제공하여 의미 정렬을 보장합니다.
4. 필요성 및 충분성 평가: 시스템은 원인 조합을 분석하여 다음을 결정합니다:
   • 개별 필요성: 특정 원인이 그 자체로 필수적인가?
   • 최소 필요 집합: 제거 시 결과를 불가능하게 만드는 데 필요한 최소한의 원인 집합은 무엇인가?
   • 최소 충분 집합: 어떤 원인 조합이 결과 발생을 보장하는가?

C. 검증 파이프라인 (규칙 검증 엔진)

규칙이 지식 베이스에 통합되기 전에 3 단계 자동 검증을 거칩니다:

1. 구문 및 스키마 유효성 검사: 규칙이 논리 언어 및 도메인 온톨로지에 부합하는지 확인합니다.
2. 논리적 일관성 분석: 기존 FOL 지식 베이스와의 모순 여부를 점검합니다.
3. 안전 및 불변성 검증: Z3 와 같은 솔버를 사용하여 규칙이 충돌 회피와 같은 중요한 시스템 속성을 보존하는지 형식적으로 검증합니다.

모든 단계를 통과한 규칙만 지식 베이스에 커밋되어 향후 적응을 안내합니다.

3. 주요 기여

• 메타 레벨 합성 루프: 규칙 유지보수를 점진적이고 추적 가능한 과정으로 취급하는 새로운 아키텍처로, 단일 블록 규칙 베이스에서 모듈화되고 목표와 연결된 규칙 세트로의 전환을 도모합니다.
• LLM 기반 인과 귀납: LLM 이 특정 법적 및 안전 도메인에 기반하여 구조화된 귀납적 추론 (결과로부터 원인 생성) 과 연역적 추론 (필요성/충분성 평가) 을 수행하도록 제약을 가할 수 있음을 입증합니다.
• "필요하고 충분한" 집합의 형식화: AI 목표의 과도 명세 또는 미명세 문제를 해결하고 안전 목표를 보장하는 최소 규칙 세트를 체계적으로 유도하는 방법.
• 추적성: 합성된 모든 규칙은 명시적으로 기원한 인간 목표 및 법적 원칙과 연결되어 감사 가능성과 설명 가능성을 향상시킵니다.

4. 결과 (개념 증명)

저자들은 OpenAI 의 GPT-4o Mini 와 독일 교통 규정 및 물리적 안전 원칙의 선별된 세트를 활용하여 두 가지 자율 주행 시나리오에서 개념 증명 구현을 통해 접근법을 평가했습니다.

• 시나리오 1: 혼잡한 교통으로의 합류
  • 시스템은 목표를 4 개의 고유한 통합 원인으로 성공적으로 분해했습니다.
  • 일부 원인은 개별적으로 필수적이지 않았지만, 특정 최소 필요 집합 내에서는 필수적임을 식별했습니다.
  • 안전한 합류를 보장하는 4 개의 모든 원인을 포함하는 단일 최소 충분 집합을 도출했습니다.
• 시나리오 2: 고속도로에서 일정 속도 유지
  • 시스템은 6 개의 고유한 원인을 식별하여 제어, 속도 제한, 마찰과 같은 3 개의 개별 필요 조건으로 축소했습니다.
  • 장애물 유무 vs 교통 변화와 같은 서로 다른 조건 조합이 목표를 충족할 수 있음을 보여주는 두 가지 다른 최소 충분 집합을 생성했습니다.
• 상징적 번역: LLM 은 "충분한 거리"와 같은 복잡한 자연어 조건을 ∀x(sd_front(x) ∧ sd_rear(x) ← ¬dense(x))와 같은 정밀한 FOL 규칙으로 성공적으로 매핑했습니다.

결과: 파이프라인은 고수준 목표에서 최소적, 필수적, 충분적인 규칙 세트를 성공적으로 유도하여, 안전하지 않은 행동을 착각 (할루시네이션) 없이 논리적 제약으로 형식화했습니다.

5. 의의 및 향후 작업

• 격차 해소: 이 연구는 모호한 인간의 의도와 엄격한 형식 검증 사이의 격차를 해소하여, AI 의 '보상 해킹' 및 목표 오지정을 완화할 수 있는 경로를 제시합니다.
• 확장성: 규칙 변경을 특정 목표 연결 모듈로 국한함으로써 대규모 규칙 세트에서의 유지보수 부담과 연쇄 실패 위험을 줄입니다.
• 안전 보장: 검증 엔진의 통합은 논리적 일관성이 있고 안전을 보존하는 규칙만 배포되도록 보장하여 안전-중요 시스템에 필수적입니다.

한계 및 향후 방향:

• 현재 접근법은 사전 정의된 규정 세트에 의존하며, 향후 연구는 도메인 범위를 확장하는 것을 목표로 합니다.
• LLM 은 '블랙박스'로 작용하며, 프롬프트 민감성은 여전히 과제입니다.
• 향후 계획에는 새로운 규칙과 기존 규칙 간의 충돌을 탐지하기 위한 자동 솔버 통합 및 불확실성을 더 견고하게 처리하기 위한 확률적 추론 도입이 포함됩니다.

결론적으로, 이 논문은 신경 - 상징적 인과 규칙 합성을 위한 강력한 프레임워크를 제시하며, LLM 과 형식 논리 및 인과 추론을 결합함으로써 인간의 법적 및 안전 원칙에 기반한 적응형, 설명 가능, 안전한 AI 시스템을 구축할 수 있음을 보여줍니다.