Theorem 创始人:AI 已攻克形式验证最难的一环
burny_tech · x · 2026-09-23
形式验证初创公司 Theorem 联合创始人 Rajashree 把形式验证拆成三个子问题,并断言 AI 已经解决了公认最难的第一个:
- 定理陈述生成:把程序塞进证明助手、正确表述待证命题,这一步曾被认为最难,如今 AI 已经解决;
- 证明生成:AI 能对程序进行推理,完整生成证明;
- 证明检查:瓶颈反而在这里——证明助手的检查是 CPU 密集型工作,速度太慢,即使写出了证明,验证耗时也长到无法实际得出答案。
这一判断意味着 AI 在形式化数学/程序验证中的短板已经从"会不会证"转移到"验得快不快",计算架构(而非模型能力)成了新的瓶颈。
「公司和人」频道最新
- PrimeIntellect 迎来新实习生，专注优化推理推理栈 — willcb · 2026-09-23
- OpenAI 垂直化难成功：行业默认格局与社会切换成本是壁垒 — nicolechirps · 2026-09-23
- Cloudflare CTO 入选 TIME 年度高管：为 agent 时代重建互联网 — dinasaur_404 · 2026-09-23
- tszzl:做漂亮 3D 动画已是新模型营销最重要的技能 — tszzl · 2026-09-23
- Sam Altman 回顾高回报的空窗期:读几十本教材、帮人做事埋下种子 — a16z · 2026-09-23
- 从荒诞想法到影院银幕：AI 视频首映活动 WVLNGTH 四天后登陆布莱顿 — Loo_Atreides · 2026-09-23