대규모 언어 모델 (LLMs)의 광범위한 통합은 엄격하고 체계적인 안전성 평가를 필요로 합니다. 기존의 패러다임은 미리 정의된 관점에서 안전성을 평가하기 위해 구축된 벤치마크에 의존하거나, 잠재적인 취약점을 조사하기 위해 동적 레드팀 (red-teaming)을 채택합니다. 이러한 접근 방식은 효과적이긴 하지만, 전문가의 도메인 지식에 크게 의존하고, 제한적인 체계적 보장을 제공하며, 빠르게 구식화될 위험이 있다는 문제에 직면해 있습니다. 이러한 한계를 해결하기 위해, 우리는 명세 기반 소프트웨어 테스트 (specification-based software testing)의 엄격함을 AI 안전성에 도입하는 새로운 프레임워크인 POLARIS를 소개합니다. POLARIS는 먼저 비정형 자연어 정책을 1차 논리 (First-Order Logic, FOL) 표현으로 컴파일하여, 상위 수준의 규칙과 구체적인 테스트 케이스 사이에 추적 가능한 연결 고리를 구축합니다. 이러한 정형화는 복잡한 정책 위반 시나리오가 탐색 가능한 경로로 인코딩되는 의미론적 정책 그래프 (Semantic Policy Graph)의 구축을 가능하게 합니다. 이 그래프를 체계적으로 탐색함으로써, POLARIS는 구성적 위반 패턴 (compositional violation patterns)을 발견하며, 이는 실행 가능한 자연어 테스트 쿼리로 인스턴스화되어 커버리지 기반의 재현 가능한 안전성 테스트를 가능하게 합니다. 실험 결과, POLARIS는 기존의 베이스라인과 비교하여 더 높은 정책 커버리지와 공격 성공 횟수를 달성함을 입증했습니다. 결정적으로, POLARIS는 정형 방법론 (formal methods)과 AI 안전성을 연결함으로써, LLMs가 검증 가능한 추적성을 갖춘 안전 필수 정책을 준수하도록 보장하는 원칙적이고 자동화된 접근 방식을 제공합니다. 우리는 코드를 https://github.com/huac-lxy/POLARIS 에서 공개합니다.