∃xProofAI studies the foundations of safe artificial agency.

∃xProofAI studies the foundations of safe artificial agency, to address the challenges posed by AI systems that could lead to catastrophic or existential harm. We work to understand how advanced systems represent the world, form and pursue objectives, and can be made more interpretable and aligned.

Arguments about AI risk rest on concepts such as belief, goal, control, power, and alignment. We give these concepts precise formal treatments, usually decision-theoretic or Bayesian. We then ask what each treatment predicts about trained systems, so that interpretability and evaluations can test it. Our work runs from representation theorems to experiments on transformers.

∃x is read “there exists an x,” and ∃xProof is short for existence proof. The name ∃xProofAI is pronounced “ExProof AI.”

An existence proof is settled by a single witness: one object that satisfies the condition. Here the condition is being a path to safe AI. We are looking for one such path, if one exists.

The animation behind these pages runs the same search on a small scale. A light explores a hidden tree, looking for a path from the left edge to the right. One tree in three has such a path. When the path exists, the search finds it; when it does not, the search exhausts the tree and starts again.

Logic, Bayesian epistemology, decision and game theory, mechanistic interpretability, and philosophical analysis.