Verified AI
Paradigm advocated by axiom-math and carina-hong that positions formal verification as essential for achieving artificial general intelligence. Rather than traditional approaches focused on statistical learning, Verified AI emphasizes mathematically provable correctness as the foundation for scaling AI capabilities.
Core Philosophy
"Scaling Brilliance, Not Fixing Lousiness": Verification isn't about error correction but about compounding and scaling mathematical insights. Uses srinivasa-ramanujan analogy - when convinced to formalize proofs, Ramanujan's capabilities improved AND others could build upon his work.
Compounding Knowledge: Formally verified proofs create solid foundations that enable:
- Scaling: More people can use and trust the results
- Compounding: Future work can build upon verified foundations
- Transfer: Knowledge transfers reliably across domains
AGI Necessity: carina-hong makes unqualified claim: "We do not believe there is any other possible future" for AGI development.
Technical Implementation
Training Approach:
- Uses Reinforcement Learning with Verification instead of statistical methods
- lean-proofs provide stronger reward signals than GRPO, RLHF
- Higher sample efficiency and maximum performance ceiling
- Growing corpus of verified knowledge for future training
Inference Benefits:
- Verified outputs have reliability comparable to human-generated proofs
- Enables AI systems to build upon previous verified work
- Reduces need for human verification bottlenecks
Cross-Domain Applications
Scientific AI: alex-lupsasca notes verification bottleneck in theoretical physics as AI generates thousands of proofs simultaneously.
Physical Systems: Applied Intuition highlights verification challenges in autonomous systems as models improve.
Critical Systems: Hardware verification, flight control, nuclear power, medical devices require formal correctness guarantees.
Implementation Challenges
Specification Problem: "Anything that can be specified can be proven. Humans are bad at specifying everything we want." - Core challenge of translating real-world requirements into formal specifications.
Generation Difficulty: lean-proofs are "expensive to produce, cheap to verify" - current LLMs struggle with direct Lean generation, requiring specialized training approaches.
Frontier Lab Gap: Current frontier labs reportedly still rely on informal proofs rather than direct Lean generation, creating opportunity for specialized approaches.
Market Positioning
Contrasts with current AI development focused on:
- Statistical learning without verification
- Informal reasoning and code generation
- Scale without formal correctness guarantees