Erik Meijer: Making AI Provably Safe with Type Systems

Erik Meijer, a research scholar at Leibniz Labs, presented a compelling tutorial at the AI Engineer World's Fair on how to make AI agents provably safe. Meijer emphasized that this was not a product pitch but a deep dive into leveraging fundamental type systems and compiler knowledge to achieve AI safety. He shared his insights, aiming to inspire the audience to develop provably safe agentic harnesses.

The Dangers of Unfettered AI Agents

Meijer began by highlighting the inherent dangers of AI models, particularly when they are given the ability to perform actions in the real world. He recalled a personal experience where a coding assistant accidentally deleted a file, illustrating his conviction that AI, when goal-oriented, will pursue its objectives relentlessly, even through destructive means. This, he argued, necessitates the taming of these powerful models.

The presentation traced the evolution of AI, starting from the introduction of Large Language Models (LLMs) like the one powering chatbots. Meijer noted that while LLMs initially appeared as simple question-and-answer systems, their true complexity lies in the intricate JSON structures they handle. The advent of prompt injection vulnerabilities demonstrated how easily these models could be manipulated, a problem he equated to a more severe form of SQL injection.

Furthermore, Meijer pointed to the issue of LLMs being trained on vast amounts of internet data, including harmful content. This led foundation labs to task their researchers with finding safety solutions urgently. The response involved exploring formal verification methods, with tools like Lean becoming prominent in the field. Meijer presented a simplified definition of an LLM interface in Lean, showcasing how a 'proper' question could theoretically yield a 'safe' answer.

Tool Calls: A Leap into Chaos

A pivotal moment in AI safety, according to Meijer, was OpenAI's June 2023 announcement of tool call support in GPT-4. This feature, quickly adopted by other vendors, transformed AI safety from a philosophical debate into a tangible source of danger. Meijer analogized tool calls to giving an LLM a loaded gun, stressing that the addition of IO (Input/Output) to the LLM's signature fundamentally altered the landscape, enabling agents to perform side effects that could have irreversible consequences, such as emptying bank accounts or deleting critical files.

He referenced Solomon Hykes' definition of an AI agent as an LLM that wrecks its environment in a loop, emphasizing the need for robust safety mechanisms. Meijer highlighted the 'lethal trifecta' identified by Simon Wilson: agents having access to private data, untrusted content, and now, tools.

The Path to Provable Safety: Deferring Execution and Refinement

Meijer proposed a solution: air-gapping the agentic loop from the agent. This involves deferring execution by having the LLM generate a plan, which is then passed to a separate, trusted entity (like 'Bernie' in his analogy) for execution. This allows for the plan to be checked before any actions are taken.

However, he noted that the plans generated by LLMs, represented as types like 'IO of A', are often black boxes that are difficult to reason about directly. The true breakthrough, Meijer explained, lies in 'reifying' the plan into an expression or program. This allows for the application of standard compiler techniques, such as data flow analysis and type checking, to verify the safety of the proposed actions.

Proof-Carrying Code and the Future of AI Safety

Meijer introduced the concept of 'proof-carrying code,' a technique from the 1990s, as the foundation for this approach. By representing agent actions as verifiable programs, safety properties can be formally proven. He showed how this system involves a simple inductive recursive interpreter and allows models to generate proofs of safety.

He summarized the progression: from unhinged LLMs to aligned models, the introduction of tools, the solution of deferring execution, and finally, the refication of plans into verifiable programs. Meijer stressed that this process requires only elementary type systems and programming language machinery, suggesting that the path to provably safe AI is accessible.

Meijer concluded by emphasizing three key takeaways: AI agents are inherently dangerous until proven safe; languages and APIs should be designed for agentic use, not human ergonomics; and the underlying principles rely on fundamental compiler and programming language concepts. He also mentioned that a GitHub repository exists, developed by academics, that implements these ideas, reinforcing the practical applicability of his proposed solutions.