Formal Methods for AI Alignment

Team

Kevin Baum, Lisa Dargasz, Felix Jahn, Yannic Muskalla, Andre Steingrüber

Content

AI alignment is, broadly speaking, the task of ensuring that AI systems act in accordance with human values and goals (though what exactly this means remains contested). Many prevalent alignment approaches, such as RLHF and Constitutional AI, suffer from limited interpretability and lack formal guarantees. Bridging these approaches with formal frameworks, both computational and normative, seems tempting, as it promises more rigorous and interpretable alignment techniques.

In this seminar, we explored a rich repertoire of papers: foundational work on the current state of alignment methods; prima facie suitable formal approaches from computer science (including temporal logics and reward machines) and philosophy (such as deontic logics and theories of reasons); and neuro-symbolic architectures that attempt to combine the strengths of learned systems with formal methods. Participants discussed these different strands of research with one another and with members of our interdisciplinary research group.

Requirements

• Genuine interest in questions related to AI alignment and AI safety
• Familiarity with some of the following areas: agentic AI, reinforcement learning, formal logic and formal methods, practical reasoning, and practical philosophy
• Ability and willingness to read and critically discuss English-language research papers
• Openness to interdisciplinary perspectives and active, engaged participation in seminar discussions

Topics

Block A: State-of-the-Art AI Alignment

• A1, RLHF basics: Deep Reinforcement Learning from Human Preferences; Training Language Models to Follow Instructions with Human Feedback
• A2, RLHF-based alignment and Constitutional AI: Constitutional AI: Harmlessness from AI Feedback; Training a Helpful and Harmless Assistant with Reinforcement Learning from Human Feedback
• A3, LLM guardrails: Symbolic Guardrails for Domain-Specific Agents: Stronger Safety and Security Guarantees Without Sacrificing Utility; AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agents

Block B: Normative Logics

• B1, Normative systems: A Temporal Logic of Normative Systems; On social laws for artificial agent societies: off-line design
• B2, Logic of reasons: Piecemeal Knowledge Acquisition for Computational Normative Reasoning; Precedent and Open Texture
• B3, Deontic temporal logic: Strategic Deontic Temporal Logic as a Reduction to ATL, with an Application to Chisholm’s Scenario; Deontic Temporal Logic for Formal Verification of AI Ethics
• B4, Logic and verification: Formal verification of ethical choices in autonomous systems; Specifying Agent Ethics (Blue Sky Ideas)

Block C: Logic-Based RL

• C1, RL with reward machines: Synthesising Reward Machines for Cooperative Multi-Agent Reinforcement Learning; Reward Machines: Exploiting Reward Function Structure in Reinforcement Learning
• C2, RL with temporal logics: Reinforcement Learning Based Temporal Logic Control with Maximum Probabilistic Satisfaction; Temporal Logic Guided Safe Reinforcement Learning Using Control Barrier Functions
• C3, Ethical RL agents: Enforcing Ethical Goals Over Reinforcement Learning Policies; Learning Normative Behaviour Through Automated Theorem Proving
• C4, Shielding: Safe Reinforcement Learning via Shielding; Safe Reinforcement Learning Using Probabilistic Shields

Block D: Neuro-Symbolic Architectures

• D1, Neurosymbolic AI: Neurosymbolic AI: The 3rd Wave; The Third AI Summer: AAAI Robert S. Engelmore Memorial Lecture
• D2, World models: Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems; The Scientist AI: Safe by Design, by Not Desiring
• D3, Neurosymbolic alignment: Hybrid Approaches for Moral Value Alignment in AI Agents
• D4, GRACE: Breaking Up with Normatively Monolithic Agency with GRACE: A Reason-Based Neuro-Symbolic Architecture for Safe and Ethical AI Alignment

Organization

All information and materials are available in the CMS.