# Provably safe systems: the only path to controllable AGI

arXiv: https://arxiv.org/abs/2309.01933 · HTML: https://mlsanity.com/paper/2309.01933/

## Key facts

- Cited by 29 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 81 references that are in the map.
- First posted on arXiv 5 Sep 2023.

## Builds on (most cited first, 11 of 11)

- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [An Overview of Catastrophic AI Risks](https://mlsanity.com/paper/2306.12001/) (2023)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [AI Deception: A Survey of Examples, Risks, and Potential Solutions](https://mlsanity.com/paper/2308.14752/) (2023)
- [Fundamental Limitations of Alignment in Large Language Models](https://mlsanity.com/paper/2304.11082/) (2023)
- [From Word Models to World Models: Translating from Natural Language to the Probabilistic Language of Thought](https://mlsanity.com/paper/2306.12672/) (2023)
- ["Real Attackers Don't Compute Gradients": Bridging the Gap Between Adversarial ML Research and Practice](https://mlsanity.com/paper/2212.14315/) (2022)
- [Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving](https://mlsanity.com/paper/2305.16366/) (2023)
- [The AGI Containment Problem](https://mlsanity.com/paper/1604.00545/) (2016)
- [Precision Machine Learning](https://mlsanity.com/paper/2210.13447/) (2022)

## Built on by (most cited first, 29 of 29)

- [Mechanistic Interpretability for AI Safety -- A Review](https://mlsanity.com/paper/2404.14082/) (2024)
- [Not All Language Model Features Are One-Dimensionally Linear](https://mlsanity.com/paper/2405.14860/) (2024)
- [Can LLM-Generated Misinformation Be Detected?](https://mlsanity.com/paper/2309.13788/) (2023)
- [Black-Box Access is Insufficient for Rigorous AI Audits](https://mlsanity.com/paper/2401.14446/) (2024)
- [A Comprehensive Survey in LLM(-Agent) Full Stack Safety: Data, Training and Deployment](https://mlsanity.com/paper/2504.15585/) (2025)
- [Mechanistic understanding and validation of large AI models with SemanticLens](https://mlsanity.com/paper/2501.05398/) (2025)
- [Nuclear Deployed: Analyzing Catastrophic Risks in Decision-making of Autonomous LLM Agents](https://mlsanity.com/paper/2502.11355/) (2025)
- [Opening the AI black box: program synthesis via mechanistic interpretability](https://mlsanity.com/paper/2402.05110/) (2024)
- [Adaptive Learn-then-Test: Statistically Valid and Efficient Hyperparameter Selection](https://mlsanity.com/paper/2409.15844/) (2024)
- [Distributional AGI Safety](https://mlsanity.com/paper/2512.16856/) (2025)
- [RedDebate: Safer Responses Through Multi-Agent Red Teaming Debates](https://mlsanity.com/paper/2506.11083/) (2025)
- [AI Testing Should Account for Sophisticated Strategic Behaviour](https://mlsanity.com/paper/2508.14927/) (2025)
- [Investigating Representation Universality: Case Study on Genealogical Representations](https://mlsanity.com/paper/2410.08255/) (2024)
- [On the creation of narrow AI: hierarchy and nonlocality of neural network skills](https://mlsanity.com/paper/2505.15811/) (2025)
- [Free Energy Risk Metrics for Systemically Safe AI: Gatekeeping Multi-Agent Study](https://mlsanity.com/paper/2502.04249/) (2025)
- [The Economics of p(doom): Scenarios of Existential Risk and Economic Growth in the Age of Transformative AI](https://mlsanity.com/paper/2503.07341/) (2025)
- [Can Safety Fine-Tuning Be More Principled? Lessons Learned from Cybersecurity](https://mlsanity.com/paper/2501.11183/) (2025)
- [No-Knowledge Alarms for Misaligned LLMs-as-Judges](https://mlsanity.com/paper/2509.08593/) (2025)
- [Bounded PCTL Model Checking of Large Language Model Outputs](https://mlsanity.com/paper/2509.18836/) (2025)
- [ASGuard: Activation-Scaling Guard to Mitigate Targeted Jailbreaking Attack](https://mlsanity.com/paper/2509.25843/) (2025)
- [Verifying Memoryless Sequential Decision-making of Large Language Models](https://mlsanity.com/paper/2510.06756/) (2025)
- [Owner-Harm: A Missing Threat Model for AI Agent Safety](https://mlsanity.com/paper/2604.18658/) (2026)
- [Towards provable probabilistic safety for scalable embodied AI systems](https://mlsanity.com/paper/2506.05171/) (2025)
- [Limitations on Accurate, Trusted, Human-level Reasoning](https://mlsanity.com/paper/2509.21654/) (2025)
- [Logical Consistency Between Disagreeing Experts and Its Role in AI Safety](https://mlsanity.com/paper/2510.00821/) (2025)
- [Provably Secure Agent Guardrail](https://mlsanity.com/paper/2605.29251/) (2026)
- [International Agreements to Limit Frontier AI: Objectives and Exit](https://mlsanity.com/paper/2607.16224/) (2026)
- [Contract monitoring: governing AI via separation of powers](https://mlsanity.com/paper/2609.32061/) (2026)
- [AI Safety Considerations for Agents With Limited Time to Act](https://mlsanity.com/paper/2610.10285/) (2026)

## Abstract (arXiv)

We describe a path to humanity safely thriving with powerful Artificial General Intelligences (AGIs) by building them to provably satisfy human-specified requirements. We argue that this will soon be technically feasible using advanced AI for formal verification and mechanistic interpretability. We further argue that it is the only path which guarantees safe controlled AGI. We end with a list of challenge problems whose solution would contribute to this positive outcome and invite readers to join in this work.