反转护盾：从策略规范系统性生成安全测试

大语言模型（LLM）的广泛集成需要严格而系统的安全评估。现有范式要么依赖构建好的基准从预定义视角评估安全性，要么采用动态红队测试探测潜在漏洞。这些方法虽然有效，却面临挑战：它们严重依赖专家领域知识，系统性保证有限，且容易迅速过时。为解决这些局限，我们提出新框架POLARIS，将基于规范的软件测试的严谨性引入AI安全。POLARIS首先将非结构化的自然语言策略编译为一阶逻辑（FOL）表示，在高层规则与具体测试用例之间建立可追溯的关联。这种形式化使构建语义策略图成为可能，其中复杂的策略违规场景被编码为可遍历的路径。通过系统地探索该图，POLARIS发现组合式违规模式，随后将其实例化为可执行的自然语言测试查询，从而实现以覆盖率为驱动且可复现的安全测试。实验表明，与既有基线相比，POLARIS取得更高的策略覆盖率和攻击成功次数。至关重要的是，通过连接形式化方法与AI安全，POLARIS提供了一种有原则的自动化途径，以可验证的可追溯性确保LLM遵守安全关键策略。我们在 https://github.com/huac-lxy/POLARIS 发布代码。