@geoffreyirving: 与Gopal Sarma、Rachel Steratore、Sunny Bhatt和我合著的新论文，调查形式化方法从业者对AI安全应用重要性的看法…

新论文与Gopal Sarma、Rachel Steratore、Sunny Bhatt及我合作，调查了形式化方法领域从业者对AI安全应用的重要性和可处理性的看法。我非常兴奋这篇论文终于发布了！

在此更广泛地呼吁大家以极其宏大的目标来验证软件！

AI辅助的形式化证明（尤其是在Lean中）正变得非常出色！我担心的是，人们会未能充分认识到这些工具的强大潜力，从而不敢着手足够庞大的项目。

因此，以下是一些预测！到2027年底，我们将拥有以下所有内容的形式化证明*：

1. clang和gcc的正确性
2. Linux中不存在内存错误
3. 至少一家主要硬件公司（例如英特尔、苹果或英伟达）内部，整个芯片的正确性

*当然，这些证明将基于规范，而单靠人类努力不足以按时编写这些规范。因此，规范将部分由AI生成，从而只能提供对软件实际正确性的部分置信度。

还有一个细微之处：为什么我没有说“Linux的正确性”。两个更详细的声明：

1. Linux与一个没有内存错误的Linux版本稀疏接近
2. Linux与任何没有拒绝服务攻击的版本稀疏远离

也就是说，在不进行重大转向（如改用从零开始设计、更难出现此类错误的seL4之类系统）的情况下，无法实现操作系统针对某些漏洞的正确性。对于内存错误，我们可以在证明构建过程中局部发现并修复；而分布式拒绝服务（DDoS）问题则更为全局性。

正确的clang + 正确的gcc + 内存安全的Linux将意义重大！当然，还有许多其他值得押注的巨大项目！形式化方法具有美妙的防御优势；让我们将其规模化！

哎呀，忘了给这些预测加上具体概率：我对1、2、3每一条的置信度都超过80%。