Christian Szegedy 预测：2030 年前主流软件将全部被形式化验证
AlexKontorovich · x · 2026-09-22
Google 研究员 Christian Szegedy 转发并背书了一个他坚持十年的预测：数学对世界最大的影响不是千禧年难题，而是大规模软件证明。
核心论点：
- 到 2030 年，所有主流软件都将经过形式化验证，届时你可能不会再接触未经验证的代码库。
- 规格形式化（formalization of specs）和在十亿行代码规模上做验证，是最适合 AI 自动研究/自我改进循环的攻关目标。
- 他认为这一判断很笃定：如果这没发生，要么 AI 发展停滞，要么世界已经终结。
所属事件:Szegedy 预测 2030 年主流软件将全部被形式化验证(3 条相关)→
「漫话AGI」频道最新
- 蒸馏对中国大厂贡献多大?Nat Lambert 播客激辩:无硬证据支撑大幅领先说 — xeophon · 2026-09-23
- 研究者：我担心的不是 AI 进步，而是接住它的社会与制度 — generativist · 2026-09-23
- Dario 发文呼吁放缓后,Anthropic 二级市场估值应声下跌约 5% — trevposts · 2026-09-23
- 递归自我改进不等于指数起飞，速率与性质更关键 — hargup13 · 2026-09-23
- 意识能否被测量与证伪？物理系统现象体验之问 — burny_tech · 2026-09-23
- 「已解 100 道难题但不说是哪些」，数学家该慌吗？ — basedjensen · 2026-09-23