开发者质疑 Anthropic 把定理证明器漏洞列为网络安全风险

ethanbodzioney · x · 2026-11-10

一位开发者公开质疑 Anthropic 的安全分类：为什么在定理证明器里找 bug 会被当作「网络安全问题」？他调侃说，最坏结果不过是「证明出 false，让数学家头疼一下」。

随后有回应指出，随着 LLM 越来越多地被用于撰写形式化证明——从代码安全属性的形式化验证到密码学协议验证——定理证明器的漏洞确实可能构成真实的安全隐患；也有评论者认同原帖，认为 Anthropic 的所谓「cyber safeguards」在这类场景下弊大于利。