Karina Hong 探讨了基于形式验证和数学的验证式 AI 如何实现人机协作和 AI 间协作，以扩展智慧，而不仅仅是满足封闭行业的需求。
Karina Hong discusses how verified AI, grounded in formal verification and math, enables human-AI and AI-AI collaboration to scale brilliance, not just meet closed industry requirements.
要点 · TL;DR
形式验证通过实现可靠的 AI 协作来扩展智慧。 Formal verification scales brilliance by enabling reliable AI collaboration.
验证生成在性能和样本效率上优于非正式方法。 Verified generation outperforms informal methods in performance and sample efficiency.
AI 领域的碎片化是形式验证可以解决的主要瓶颈。 Fragmentation in AI is a major bottleneck that formal verification can address.
核心观点 · Key points
形式验证关乎扩展智慧，而不仅仅是消除错误。 Formal verification is about scaling brilliance, not just eliminating errors.
验证生成在性能和样本效率上优于非正式方法。 Verified generation yields performance gains and sample efficiency over informal methods.
基于 Lean 的系统在代数等结构化数学领域表现出色，但在组合数学等创造性领域存在困难。 Lean-based systems excel in structured math domains like algebra but struggle in creative areas like combinatorics.
编程的未来是将非正式推理与形式验证相结合以确保可靠性。 The future of coding involves combining informal reasoning with formal verification for reliability.
数学发现工具对于在形式证明之前形成猜想至关重要。 Mathematical discovery tools are essential for forming conjectures before formal proof.
AI 领域的碎片化是进展的主要瓶颈。 Fragmentation in the AI landscape is a major bottleneck for progress.
反共识 · Contrarian takes
形式验证不仅适用于安全关键行业，也适用于开放协作。 Formal verification is not just for safety-critical industries but for open collaboration.
仅靠非正式数学系统无法扩展到超级智能；形式方法是必要的。 Informal math systems alone cannot scale to superintelligence; formal methods are necessary.
验证应被视为性能提升，而非痛苦的负担。 Verification should be seen as a performance gain, not a painful requirement.
形式验证的市场从利基领域扩展到所有 AI 生成的代码。 The market for formal verification extends beyond niche domains to all AI-generated code.
由于缺乏基础，自动形式化比自动非形式化更难。 Auto-formalization is harder than auto-informalization due to lack of grounding.
即使有超人类 AI 证明定理，人类的品味和直觉仍然至关重要。 Human taste and intuition remain crucial even with superhuman AI proving theorems.
本期章节 · Chapters（共 34）
验证型AI助力协作与卓越扩展Verified AI for Collaboration and Scaling Brilliance
引言与Axiom里程碑Introduction and Axiom's Milestones
市场潜力与横向迁移Market Potential and Horizontal Transfer
前沿实验室与形式验证Frontier Labs and Formal Verification
形式验证：从安全到卓越扩展Formal verification: from safety to scaling brilliance
超级智能与形式验证Superintelligence and Formal Verification
数学发现vs形式证明Mathematical Discovery vs. Formal Proof
形式验证与理论极限Formal Verification and Theoretical Limits
愿景：可规范即可证明Vision: Anything specifiable can be proven
AI辅助证明中的猜想与规范Conjecture and Specification in AI-Assisted Proof
Lean证明扩展与LLM局限Scaling of Lean Proofs and LLM Limitations
人类好奇心vs AI证明Human curiosity vs. AI proofs
商业模式与验证Business model and verification
硬件验证痛点Hardware verification pain point
投资者信念与超级智能之路Investor belief and the path to superintelligence
Axiom独特之处What makes Axiom special
神经科学背景Neuroscience background
法学院与数学博士Law school and math PhD
关于已解决问题之争议Controversy about solved problems
溯源与搜索挑战Provenance and Search Challenges
知识图谱与数据积累Knowledge Graph and Data Accumulation
数学领域的AlphaZero与自我改进AlphaZero for Math and Self-Improvement
推理中的验证器与形式验证Verifiers in Inference and Formal Verification
初创聚焦vs科技巨头Startup Focus vs Big Tech
Axel简介Introduction to Axel
协作与蓝图编写Collaboration and Blueprint Writing
非专家的价值Value for Non-Experts
强化学习的奖励Reward for Reinforcement Learning
前沿实验室的价值主张Value Proposition of Frontier Labs
为何创立AxiomWhy Start Axiom
性能提升与验证Performance gain and verification
数学视角与迁移学习Mathematical perspective and transfer learning
最大瓶颈：碎片化Biggest bottleneck: fragmentation
市场条件与深度技术碎片化Market conditions and fragmentation in deep tech