Inverting the Shield: Systematically Generating Safety Tests from Policy Specifications
Xiaoyue Lu, Xianglin Yang, Haijun Liu, Jiahao Liu, Kuntai Cai, Yan Xiao, Jin Song Dong
Abstract
The widespread integration of Large Language Models (LLMs) necessitates rigorous and systematic safety evaluation. Existing paradigms either rely on constructed benchmarks to assess safety from predefined perspectives, or employ dynamic red-teaming to probe potential vulnerabilities. While effective, these approaches face challenges, as they depend heavily on expert domain knowledge, offer limited systematic guarantees, and are vulnerable to rapid obsolescence. To address these limitations, we introduce a novel framework POLARIS that brings the rigor of specification-based software testing to AI safety. POLARIS first compiles unstructured natural-language policies into First-Order Logic (FOL) representations, establishing a traceable link between high-level rules and concrete test cases. This formalization enables the construction of a Semantic Policy Graph, where complex policy violation scenarios are encoded as traversable paths. By systematically exploring this graph, POLARIS uncovers compositional violation patterns, which are then instantiated into executable natural-language test queries, enabling coverage-driven and reproducible safety testing. Experiments demonstrate that POLARIS achieves higher policy coverage and attack success counts compared to established baselines. Crucially, by bridging formal methods and AI safety, POLARIS provides a principled, automated approach to ensuring LLMs adhere to safety-critical policies with verifiable traceability. We release our code at https://github.com/huac-lxy/POLARIS.
AI Impact Assessments
(1 models)Scientific Impact Assessment: POLARIS – Inverting the Shield
1. Core Contribution
POLARIS introduces a specification-based testing paradigm for LLM safety evaluation, bridging formal methods from software engineering with AI red-teaming. The core idea is compelling: rather than relying on ad hoc benchmark construction or heuristic red-teaming, safety policies themselves are formalized into First-Order Logic (FOL) axioms called Abstract Violation Templates (AVTs), which are then organized into a Semantic Policy Graph. Systematic graph traversal discovers compositional violation pathways that are instantiated into natural-language adversarial queries. This provides three theoretically valuable properties: traceability (each test case maps to a specific policy clause), coverage guarantees (systematic exploration of the policy space), and reproducibility (the process is deterministic given the graph structure).
The conceptual contribution—treating safety policies as formal specifications and inverting them into test cases—is genuinely novel in the LLM safety space. The analogy to specification-based testing and software fuzzing is well-drawn and provides a principled foundation that most red-teaming work lacks.
2. Methodological Rigor
The methodology has both notable strengths and significant concerns:
Strengths: The three-stage pipeline (policy-to-logic compilation → semantic graph construction → query instantiation) is well-structured and clearly presented. The validation of intermediate components (Section 4.5) is a responsible addition—verifying that the FOL translation achieves 92.06% binary accuracy and 9.10/10 fine-grained score, and that entity extraction achieves 84.7% exact match and 90.1% semantic match, provides useful confidence bounds.
Concerns:
3. Potential Impact
The framework addresses a genuine need in the LLM safety ecosystem. As organizations deploy LLMs with specific usage policies, the ability to automatically generate compliance test suites from those policies has clear practical value. Several impact dimensions stand out:
However, the dual-use concern is significant—the paper essentially provides an automated system for generating harmful queries at scale. The authors briefly distinguish their work from "jailbreak" prompts but don't deeply engage with responsible disclosure considerations.
4. Timeliness & Relevance
The paper is highly timely. The gap between the proliferation of LLM safety policies and the ability to systematically verify compliance is a real and growing problem. The approach of treating policies as formal specifications addresses a recognized bottleneck. The incorporation of multiple corporate and regulatory policies (16 policies from 9 companies + 4 regulatory documents) demonstrates practical grounding.
5. Strengths & Limitations
Key Strengths:
Key Limitations:
Summary
POLARIS makes a meaningful conceptual contribution by introducing specification-based testing to LLM safety evaluation, with a well-engineered pipeline and thorough experimental evaluation. The traceability and coverage properties are genuinely valuable. However, the reliance on LLMs for the formalization step introduces circularity concerns, the evaluation methodology has notable gaps (especially regarding false positive analysis and human evaluation), and the practical gains over simpler approaches appear moderate in some dimensions. The work opens an interesting research direction but leaves important questions about the fidelity and completeness of LLM-generated formal specifications unresolved.
Generated May 26, 2026
Comparison History (19)
Paper 1 introduces a general RL optimization framework for LLM-based multi-agent systems, addressing a critical bottleneck in the transition from manually prompted agents to optimized, trainable agentic workflows. By providing a reusable infrastructure for multi-agent RL, it has the potential to become a foundational tool for a rapidly expanding field, leading to widespread adoption and high citation impact. While Paper 2 offers a rigorous approach to AI safety, Paper 1's contribution as a structural framework for agent optimization offers broader utility across various domains.
Paper 2 introduces a broadly relevant and timely problem in retrieval-augmented generation—distinguishing parametric memory use from reliance on retrieved evidence—framed as the “attribution blind spot.” Its proposed CRM method targets internal-representation signals rather than output, and is evaluated across multiple model families with mechanistic interventions and generalization tests, suggesting stronger methodological rigor and wider cross-domain implications (RAG reliability, provenance, auditing, safety). Paper 1 is practically valuable for safety testing, but depends on policy-to-logic compilation accuracy and is more narrowly scoped to policy compliance evaluation.
Paper 2 likely has higher impact: it introduces a general, formal-methods-inspired framework (POLARIS) that compiles natural-language policies into logic, enabling coverage-driven, reproducible safety testing with traceable guarantees. This is timely given regulatory and deployment pressure around LLM safety, and has broad applicability across domains requiring policy compliance (health, finance, enterprise, gov) and across fields (AI safety, formal methods, software testing). Paper 1 is novel and useful for agent reliability, but is narrower to long-lived agent memory/harness dynamics and benchmarking.
Paper 1 offers a highly timely and innovative integration of formal methods with AI safety. By translating natural-language policies into First-Order Logic, it transforms LLM safety evaluation from ad-hoc red-teaming into a rigorous, coverage-driven software testing paradigm. This methodological leap addresses a critical bottleneck in deploying safe AI systems across all domains. While Paper 2 presents a valuable neuro-symbolic approach for healthcare, Paper 1's framework is fundamentally more broadly applicable to the entire foundation model ecosystem and tackles the urgent, cross-disciplinary challenge of verifiable AI alignment.
Paper 2 (Shepherd) has higher likely impact: it delivers a general-purpose runtime substrate with formalized semantics (Lean mechanization), efficient fork/replay execution traces, and demonstrated gains across multiple meta-agent applications (supervision, counterfactual optimization, RL training). This infrastructure can be reused broadly across agent systems, verification, debugging, and training workflows, giving it wider cross-field applicability and timeliness as agentic LLMs proliferate. Paper 1 is novel and valuable for safety testing, but its impact is narrower to policy-spec safety evaluation and depends on policy-to-logic compilation fidelity.
While Paper 1 offers a highly novel formal approach to AI safety testing, Paper 2 proposes a fundamental architectural advancement in linear attention by decoupling erase and write gates. By outperforming state-of-the-art sub-quadratic models like Mamba-2 and Mamba-3 on long-context tasks, it addresses a critical bottleneck in foundation model efficiency and scaling, which will likely drive broader adoption and foundational impact across the deep learning community.
Paper 2 likely has higher scientific impact. It introduces a broadly novel bridge between formal methods (FOL, specification-based testing) and LLM safety evaluation, enabling systematic, coverage-driven, reproducible safety tests with traceability—an approach that can generalize across models, domains, and policy regimes. Its real-world applicability is immediate for compliance and safety auditing, and its impact spans AI safety, NLP, software testing, and formal verification. Paper 1 is valuable and timely for LVLM hallucinations, but is more incremental within a narrower subarea and may have less cross-field reach.
Paper 1 addresses a fundamental efficiency bottleneck in LLM inference with broad implications for architecture design, training, and deployment. Its extensive empirical study across 20 models, five families, and multiple task types, combined with theoretical grounding and demonstrated 10x hardware speedups, positions it to influence both systems research and model design. The finding that extreme context sparsity is principled rather than heuristic could reshape how the field approaches long-context LLM inference. Paper 2, while valuable for AI safety testing, addresses a narrower problem with a more incremental contribution combining existing techniques (FOL, graph traversal) for test generation.
Paper 1 likely has higher scientific impact due to a more concrete, broadly applicable, and timely methodology: compiling natural-language policies into formal logic, constructing a semantic graph, and generating coverage-driven, reproducible safety tests with traceability—bridging formal methods and LLM safety evaluation. It offers clear real-world utility (standardized safety testing pipelines) and measurable gains over baselines, supporting rigor and adoption. Paper 2 addresses an important emerging area (multi-agent misalignment) with an appealing framing, but its proposed paradigm appears less operationalized/standardizable and may be harder to validate and generalize across settings.
MemQ introduces a fundamentally novel theoretical framework (Exogenous-Context MDP, provenance DAGs with TD(λ) eligibility traces for memory credit assignment) that bridges reinforcement learning theory with LLM memory systems. This offers broader impact across multiple fields (RL, agent systems, memory architectures) and addresses a foundational limitation in how LLM agents manage episodic memory. While POLARIS is a solid engineering contribution applying existing formal methods to LLM safety testing, MemQ's theoretical novelty, formalization of a new MDP class, and demonstrated gains across six diverse benchmarks suggest deeper and more lasting scientific influence.
Paper 2 (POLARIS) introduces a novel, principled framework bridging formal methods and AI safety evaluation—a highly timely and broadly impactful contribution. Its systematic approach using First-Order Logic and Semantic Policy Graphs for coverage-driven safety testing offers strong methodological rigor, reproducibility, and practical applicability across diverse LLM deployments. While Paper 1 addresses an important gap in context learning, Paper 2's combination of novelty (specification-based testing for AI safety), broad cross-field relevance (formal methods + AI safety), and immediate real-world utility gives it higher estimated impact.
Paper 1 addresses a fundamental and broadly applicable challenge—enabling LLM agents to discover and reason about implicit rules through interaction—introducing a novel RL training pipeline and demonstrating significant performance gains. This has wide applicability across embodied AI, game-playing, and autonomous agents. Paper 2 presents a valuable but more niche contribution to LLM safety testing through formal specification methods. While rigorous, safety testing frameworks tend to have narrower impact compared to foundational reasoning advances. Paper 1's approach to test-time reasoning and exploration represents a more transformative contribution to the field.
Paper 1 addresses the critical and highly timely issue of LLM safety by innovatively bridging formal methods with AI testing. Its approach offers verifiable traceability and systematic guarantees, which are urgently needed as LLM integration expands across all sectors. While Paper 2 offers a strong contribution to optimization and routing, Paper 1's focus on AI safety grants it a much broader potential impact across multiple disciplines and real-world applications.
Paper 2 provides fundamental theoretical bounds and impossibility guarantees for human-AI teaming, solving a pervasive empirical puzzle. Its mathematical rigor, high predictive accuracy on real datasets, and broad applicability across decision-making domains offer lasting scientific impact. In contrast, Paper 1 offers a highly timely and practical engineering framework for LLM safety, but its contribution is more specialized and applied compared to the foundational theoretical advancements of Paper 2.
Paper 2 (POLARIS) likely has higher scientific impact because it introduces a more broadly applicable, formally grounded methodology: compiling natural-language policies into logic, building a semantic graph, and enabling systematic, coverage-driven safety testing with traceability. This bridges formal methods and AI safety, offering reusable tooling for evaluation across models, domains, and evolving policies—high timeliness and cross-field relevance. Paper 1 is practically valuable for controlled safety relaxation, but its impact is narrower (deployment/authorization settings) and more tightly coupled to specific model adaptation techniques.
Paper 1 addresses the critical and highly timely challenge of LLM safety. By integrating formal methods with AI safety, it offers a rigorous, automated, and reproducible framework for red-teaming, directly impacting the safe deployment of foundational models. While Paper 2 presents profound theoretical insights into decision-making and RL, Paper 1's immediate real-world applicability in the rapidly expanding AI sector gives it a higher potential for rapid, widespread scientific and industrial impact.
Paper 1 likely has higher impact due to a more novel, methodologically rigorous bridge between formal methods (FOL compilation, traceable specification-based testing) and LLM safety, yielding automated, coverage-driven, reproducible evaluations with direct real-world governance/compliance applications. It proposes a concrete framework with systematic guarantees and code release, addressing a timely bottleneck in safety assessment. Paper 2 is valuable and broad as a lifecycle evaluation study with practical insights, but is primarily diagnostic/empirical; its core contribution is less fundamentally new than a formalized testing paradigm for safety-critical policy adherence.
Paper 1 introduces a rigorous, formal methods-based approach to LLM safety testing, addressing a critical bottleneck in AI deployment. By bridging First-Order Logic with AI safety policies, it provides a traceable, systematic, and concrete methodological innovation with immediate real-world applications. While Paper 2 offers a valuable comprehensive survey of AI in scientific discovery, Paper 1's actionable framework and empirical guarantees offer a more direct and substantial technical impact on the rapidly growing field of AI safety.
Paper 2 likely has higher impact due to stronger novelty and broader, timely applicability: it connects formal specification-based testing (FOL, coverage, traceability) to LLM safety evaluation, a rapidly evolving and high-stakes area with wide cross-domain relevance (ML, security, formal methods, policy/compliance). Its framework can generalize to many models and policy sets, enabling systematic, reproducible safety testing. Paper 1 is methodologically important and improves rigor in learning analytics, but its scope and cross-field reach are narrower and primarily incremental protocol refinement within an established application area.