본 논문은 인공지능(AI) 시스템의 윤리적 행동을 공식적으로 정의하고 평가하기 위한 탈온톨로지 기반의 형식화 방법을 제안한다. 시스템 수준의 명세에 초점을 맞춰 공정성과 설명 가능성과 관련된 윤리적 요구사항을 포착하는 공리와 정리를 제시하고, 시간적 연산자를 통합하여 시간에 따른 AI 시스템의 윤리적 행동을 추론한다. COMPAS와 대출 예측 AI 시스템을 실제 사례로 활용하여 제안된 형식화의 효과를 평가한다. 탈온톨로지 논리 공식을 사용하여 해당 시스템의 다양한 윤리적 속성을 인코딩하고, 자동 정리 증명기를 사용하여 시스템이 정의된 속성을 만족하는지 확인한다. 형식적 검증 결과, 두 시스템 모두 공정성 및 차별 금지와 관련된 핵심 윤리적 속성을 충족하지 못함을 보여주며, 제안된 형식화가 실제 AI 애플리케이션의 잠재적 윤리적 문제를 식별하는 데 효과적임을 입증한다.
