REVIEW 25 cited by
Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems
read the original abstract
Ensuring that AI systems reliably and robustly avoid harmful or dangerous behaviours is a crucial challenge, especially for AI systems with a high degree of autonomy and general intelligence, or systems used in safety-critical contexts. In this paper, we will introduce and define a family of approaches to AI safety, which we will refer to as guaranteed safe (GS) AI. The core feature of these approaches is that they aim to produce AI systems which are equipped with high-assurance quantitative safety guarantees. This is achieved by the interplay of three core components: a world model (which provides a mathematical description of how the AI system affects the outside world), a safety specification (which is a mathematical description of what effects are acceptable), and a verifier (which provides an auditable proof certificate that the AI satisfies the safety specification relative to the world model). We outline a number of approaches for creating each of these three core components, describe the main technical challenges, and suggest a number of potential solutions to them. We also argue for the necessity of this approach to AI safety, and for the inadequacy of the main alternative approaches.
Forward citations
Cited by 25 Pith papers
-
Are Flat Minima an Illusion?
Flat minima are illusory; generalization is driven by weakness, a reparameterization-invariant measure of compatible completions that predicts performance better than sharpness on MNIST and Fashion-MNIST.
-
FVSpec: Real-World Property-Based Tests as Lean Challenges
A new benchmark of 9,415 Lean 4 specifications derived from 2,772 scraped Python property-based tests, plus a three-agent LLM transpilation pipeline and proof-generation baselines.
-
Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries
Machine-checked model in Rocq establishes that governance is coterminous with expressibility via four primitive constructors in a symmetric monoidal category with capability bounds and verified coherence.
-
The Two Boundaries: Why Behavioral AI Governance Fails Structurally
Behavioral governance of AI effects is undecidable for Turing-complete systems, so systems must achieve coterminous governance by separating computation from effects rather than adding governance afterward.
-
Mining Verdict Boundaries for Neural Network Verification
BMiner speeds up Branch-and-Bound neural network verification by using exponential and gradient-guided search to skip subproblems on the way to each path's verdict boundary, cutting average verification time by 17–30%.
-
Towards chemistries in dynamical systems
A finite dynamical system can be described as a Petri-net chemistry when a token map and transition map are compatible; an optional uniqueness criterion restricts when this description is least ambiguous.
-
Tensor-Based Batch Fuzzing with Adaptive Perturbation Scaling for Deep Neural Networks
A tensor-based batch fuzzing framework with adaptive perturbation scaling from specification ranges achieves up to 40X higher throughput and 4X more detected violations than sequential baselines on DNN benchmarks.
-
Interactions Between Crosscoder Features: A Compact Proofs Perspective
Derives an interaction measure between crosscoder features from reconstruction error in compact proofs and applies it to produce computationally sparse crosscoders retaining 60% MLP performance with single-feature sel...
-
Toward Pre-Deployment Assurance for Enterprise AI Agents: Ontology-Grounded Simulation and Trust Certification
The authors introduce a three-part ontology-based verification system for AI agents that generates regulatory and adversarial test scenarios and issues machine-verifiable trust certificates, with pilot results indicat...
-
Positive Alignment: Artificial Intelligence for Human Flourishing
Positive Alignment introduces AI systems that support human flourishing pluralistically and proactively while remaining safe, as a necessary complement to traditional safety-focused alignment research.
-
Stable Agentic Control: Tool-Mediated LLM Architecture for Autonomous Cyber Defense
Tool-mediated LLM agents with deterministic tools and a machine-checked Lyapunov certificate achieve stable control in cyber defense, reducing attacker game value by 59% on real attack graphs.
-
Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries
Governed execution is defined via a three-axiom GovernanceAlgebra that induces a symmetric monoidal category where expressible programs are exactly the governed ones, with all properties machine-checked in Rocq.
-
Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries
A 12,000-line Rocq development proves that effect-level governance on AI workflows is semantically transparent, preserves expressivity, and separates decidable governance predicates from undecidable semantic properties.
-
Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries
A Rocq formalization of 12,000 lines proves that effect governance in AI workflows preserves Turing completeness, expressivity, and observational equivalence to ungoverned executions.
-
The Two Boundaries: Why Behavioral AI Governance Fails Structurally
Behavioral governance of AI effects is undecidable for Turing-complete architectures, making coterminous boundaries via computation-effect separation the only structural solution rather than post-hoc layers.
-
EmbodiedGovBench: A Benchmark for Governance, Recovery, and Upgrade Safety in Embodied Agent Systems
EmbodiedGovBench is a new benchmark framework that measures embodied agent systems on seven governance dimensions including policy adherence, recovery success, and upgrade safety.
-
BarrierSteer: LLM Safety via Learning Barrier Steering
BarrierSteer applies control barrier functions to LLM latent states for constraint-guided steering that reduces unsafe generations while preserving utility.
-
Chimera: Neuro-Symbolic Attention Primitives for Trustworthy Dataplane Intelligence
Chimera combines kernelized attention approximations with symbolic fusion mechanisms to enable high-fidelity neuro-symbolic inference inside commodity programmable switches.
-
From Refusal to Recovery: A Control-Theoretic Approach to Generative AI Guardrails
Control-theoretic guardrails enable proactive correction of risky LLM agent actions in latent space, preventing catastrophes like collisions or bankruptcy while preserving task performance in simulated environments.
-
Positive Alignment: Artificial Intelligence for Human Flourishing
Positive Alignment is defined as AI systems that support human flourishing pluralistically while staying safe and cooperative, presented as a necessary complement to existing safety-focused alignment research.
-
Are Flat Minima an Illusion?
The paper argues flat minima are an illusion and that a reparameterization-invariant 'weakness' score predicts generalization where raw sharpness fails.
-
From monoliths to modules: Decomposing transducers for efficient world modelling
A framework for decomposing transducers into sub-transducers on distinct subspaces to enable parallel and interpretable world models.
-
Positive Alignment: Artificial Intelligence for Human Flourishing
Positive Alignment is introduced as a distinct AI agenda that supports human flourishing through pluralistic and context-sensitive design, complementing traditional safety-focused alignment.
-
Compiled AI: Deterministic Code Generation for LLM-Based Workflow Automation
Compiled AI generates deterministic code artifacts from LLMs in a one-time compilation step, enabling reliable workflow execution with zero runtime tokens after break-even.
-
Towards provable probabilistic safety for scalable embodied AI systems
The paper proposes a paradigm of provable probabilistic safety to enable scalable, safe deployment of embodied AI in critical applications.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.