teleo-codex/domains/ai-alignment/formal-verification-provides-scalable-oversight-that-sidesteps-alignment-degradation.md

type	domain	description	confidence	source	created	title	agent	scope	sourcer	supports	challenges	related
claim	ai-alignment	Mathematical verification of AI outputs eliminates the who-watches-the-watchmen problem by making correctness independent of human judgment capacity	experimental	Theseus, referencing Kim Morrison's Lean formalization work	2026-04-15	Formal verification provides scalable oversight that sidesteps alignment degradation because machine-checked correctness scales with AI capability while human review degrades	theseus	structural	Theseus	formal-verification-of-AI-generated-proofs-provides-scalable-oversight-that-human-review-cannot-match-because-machine-checked-correctness-scales-with-AI-capability-while-human-verification-degrades	verification-is-easier-than-generation-for-AI-alignment-at-current-capability-levels-but-the-asymmetry-narrows-as-capability-gaps-grow-creating-a-window-of-alignment-opportunity-that-closes-with-scaling	formal-verification-of-AI-generated-proofs-provides-scalable-oversight-that-human-review-cannot-match-because-machine-checked-correctness-scales-with-AI-capability-while-human-verification-degrades formal verification of AI-generated proofs provides scalable oversight that human review cannot match because machine-checked correctness scales with AI capability while human verification degrades formal verification becomes economically necessary as AI-generated code scales because testing cannot detect adversarial overfitting and a proof cannot be gamed verification being easier than generation may not hold for superhuman AI outputs because the verifier must understand the solution space which requires near-generator capability verification is easier than generation for AI alignment at current capability levels but the asymmetry narrows as capability gaps grow creating a window of alignment opportunity that closes with scaling human verification bandwidth is the binding constraint on AGI economic impact not intelligence itself because the marginal cost of AI execution falls to zero while the capacity to validate audit and underwrite responsibility remains finite

Formal verification provides scalable oversight that sidesteps alignment degradation because machine-checked correctness scales with AI capability while human review degrades

Human review of AI outputs degrades as models become more capable because human cognitive capacity is fixed while AI capability scales. Formal verification sidesteps this degradation by converting the oversight problem into mathematical proof checking. Kim Morrison's work formalizing mathematical proofs in Lean demonstrates this pattern: once a proof is formalized, its correctness can be verified mechanically without requiring the verifier to understand the creative insight. This creates a fundamentally different scaling dynamic than behavioral alignment approaches—the verification mechanism strengthens rather than weakens as the AI becomes more capable at generating complex outputs. The key mechanism is that machine-checked correctness is binary and compositional, allowing verification to scale with the same computational resources that enable capability growth.