定理证明器漏洞引担忧：LLM 批量写证明时代的安全隐患
ethanbodzioney · x · 2026-11-11
ethanbodzioney 回应关于定理证明器 bug 的讨论：他认为漏洞本身确实是个坏消息，但随机的人发现这些漏洞并不太令人担心，真正的问题在于 LLM 正被越来越多地用来批量撰写证明——从代码安全属性的形式化验证到密码学协议验证——可能不经意间依赖有缺陷的证明器来「证明」他关心的软件性质。他不太担心有人恶意构造证明，更担心 LLM 无意识地使用坏工具。
原帖作者 OwariDa 对此表示认同，认为随着 LLM 的使用，这个问题会越来越重要。