Specification Problem
Critical challenge in verified-ai systems where the bottleneck shifts from proof generation to accurately specifying what needs to be proven. As carina-hong of axiom-math puts it: "Anything that can be specified can be proven. Humans are bad at specifying everything we want."
Core Challenge
Human Specification Difficulty: While formal-verification can mechanically check correctness once problems are properly specified, translating real-world requirements into formal specifications remains a fundamental human bottleneck.
Gap Between Intent and Formalization: The challenge lies not in proving correctness, but in capturing the full scope of what "correct" means in formal mathematical language.
Implications for Verified AI
Bottleneck Shift: As AI systems become better at generating lean-proofs, the limiting factor becomes humans' ability to specify requirements with mathematical precision.
New Skills Required: Success in verified-ai may require developing better tools and methodologies for specification rather than just proof generation.
Business Implications: Companies implementing verified AI systems may need to invest heavily in specification expertise alongside verification capabilities.
Relationship to Current AI
Informal vs Formal Gap: Current AI systems work well with informal specifications but struggle when requirements must be formalized for verification.
Human-AI Collaboration: May require new paradigms where humans focus on specification while AI handles proof generation and verification.
Potential Solutions
Specification Tools: Development of better interfaces and languages for capturing human intent in formal specifications.
Iterative Refinement: Approaches where specifications can be refined through interaction with verification systems.
Domain-Specific Languages: Creating specialized specification languages for particular application domains.
See also
- verified-ai
- formal-verification
- axiom-math
- lean-proofs