✨ 要点🔬 技术摘要
想象一下，你正在建造一座宏伟的世界级图书馆。几十年来，数学家们一直在为这座图书馆的一个侧翼填满珍贵的、经过完美验证的数学真理。他们称之为 Mathlib 。它如此有用，以至于已成为进行数学运算的标准，帮助人类解决难题，甚至教会人工智能如何像数学家一样思考。
但问题在于：图书馆的其余部分——即计算机科学 所在的区域——大部分是空的。当然，那里有一些关于计算机如何工作的零散书籍，但它们杂乱无章、未经验证且难以查找。如果你想构建一个安全的软件系统或证明一个新算法有效，你通常必须从零开始，一次又一次地重复造轮子。
于是，CSLib 应运而生。
这篇论文的作者提议在 Mathlib 旁边，为计算机科学建立一个庞大的、有组织的、且经过完美验证的图书馆。他们的目标是让 Lean（一种强大的数学证明检查工具）成为计算机科学家们的首选之地，就像 Mathlib 之于数学家一样。
他们计划通过两个主要的“支柱”或建设工程来实现这一目标：
支柱 1：计算机科学百科全书
你可以将其理解为编写一部关于“计算机如何思考”的权威百科全书。
他们在做什么： 他们正在将计算机科学中每一个核心概念——例如算法如何对列表进行排序、数据如何存储在哈希表中、网络如何通信，甚至量子计算机如何工作——都用一种计算机可以检查其 100% 准确性的语言记录下来。类比： 想象一份汽车维修手册。通常，手册只会说“转动螺栓”。但在 CSLib 中，他们正在编写一份能够从数学上证明该螺栓会固定住、引擎不会爆炸、以及精确计算出消耗多少燃料的手册。他们正在为从简单的排序列表到复杂的网络协议的所有内容，创建一个统一的这些“证明”的集合。为什么重要： 现在，如果你想证明你的代码是安全的，你必须独自完成。有了 CSLib，你可以直接“借用”一个预先验证过的、经过数学证明的构建模块（比如一个排序算法），并将其嵌入到你的项目中，同时确信它运行得完美无缺。
支柱 2：通用翻译器
这是连接 CSLib 那个华丽、完美的理想世界与日常编程那个混乱、真实的现实世界的桥梁。
问题所在： 大多数程序员使用 C++、Python 或 Rust 等语言编写代码。这些语言在构建事物方面非常高效，但由于它们过于复杂且混乱，很难通过形式化验证来“证明”其无误。解决方案： CSLib 正在构建一种新的“中间人”语言，叫做 Boole 。类比： 想象你有一位才华横溢的建筑师（Lean 证明系统），他只能理解用完美几何线条绘制的蓝图。但是，建筑工人（程序员）说的是一种粗糙、充满俚语的方言（C++ 或 Rust）。
Boole 就像是一个翻译官。它将建筑工人们粗糙的俚语翻译成建筑师能理解的完美几何线条。一旦代码被翻译成 Boole，建筑师（Lean）就可以检查其中的错误。如果建筑师说：“这张蓝图是安全的”，那么原始代码也是安全的。
目标： 最终，他们希望能够将使用流行语言编写的大量代码自动翻译成 Boole，并由计算机验证其是否存在漏洞或安全隐患。
为什么要现在做这件事？（AI 的联系）
论文强调了现在构建这个库的两个重大原因，都涉及人工智能：
AI 作为风险： AI 变得越来越擅长编写代码，但它也会犯错，并可能引入安全漏洞。如果坏人利用 AI 来寻找我们软件中的弱点，我们需要一种能够从数学上证明我们的软件是安全的方法。CSLib 为检查 AI 生成的代码提供了“证明引擎”。AI 作为助手： AI 也变得越来越擅长解决数学问题。然而，目前的 AI 受限于其缺乏关于计算机科学概念的“训练数据”。通过构建 CSLib，作者正在创建一个高质量的、海量的计算机科学知识库。这将作为一本“教科书”，用来训练未来的 AI，使其能够更好地验证代码并发现新的算法。
大局观
作者不仅仅是在为少数专家构建一个工具；他们希望改变计算机科学的教学和实践方式。
对于学生： 这将是一种学习计算机背后数学的方法，并且带有一个能立即捕捉错误的防护网。对于工程师： 这将降低构建安全软件的成本，使他们能够构建在数学上保证可靠的系统。对于未来： 他们希望创造一个“飞轮效应”，让人类和 AI 协同工作：人类构建图书馆，AI 帮助完善它，而图书馆反过来帮助 AI 变得更聪明，进而帮助人类构建出更好的系统。
简而言之，CSLib 是一个雄心勃勃的项目，旨在打造“计算机科学版的 Mathlib”——一个经过验证的、庞大的计算机知识库，它架起了理论数学与运行我们世界的现实代码之间的桥梁，同时为我们迈向 AI 驱动的未来做好准备。
技术摘要：CSLib —— 轻量级计算机科学库
问题陈述
尽管 Lean 证明助手通过 Mathlib 在数学领域取得了显著成功，但目前仍缺乏一个全面、统一的用于形式化计算机科学（CS）知识的仓库。现有的 Lean 计算机科学知识基础非常有限，这阻碍了形式化方法在计算机科学教育、研究以及大规模验证系统工程中的广泛应用。此外，AI 在代码生成领域的兴起引入了新的风险：AI 智能体可能会无意中引入漏洞，而恶意攻击者也可能利用 AI 来寻找安全缺陷。形式化验证是应对这些风险的提议方案，但其历史性的采用受到了巨大人力投入的限制（例如，验证 seL4 内核需要 20 多人年）。因此，迫切需要一个能够降低形式化验证门槛、支持日常命令式代码验证，并为面向计算机科学的 AI 辅助推理提供必要基础设施的框架。
方法论
CSLib 提出通过两个支柱的技术路径来解决这些差距：
支柱 1：在 Lean 中形式化计算机科学
该支柱旨在构建一个连贯、集成的形式化 CS 概念库，该库与 Mathlib 既有区别又具有协同效应。
模型与逻辑： CSLib 将形式化多种计算模型（确定性、非确定性、概率性、量子、函数式、在线、交互式）以及规范表示法（时序逻辑、霍尔逻辑、分离逻辑、线性逻辑）。与侧重于纯数学的 Mathlib 不同，CSLib 针对的是 CS 特有的人工制品，如标记转换系统和双模拟（bisimulations）。算法与数据结构： 该库将涵盖形式化验证的算法和数据结构，范围从标准的本科课题（排序、图、哈希表）到高级领域（量子算法、数学优化）。复杂度分析： 一个核心目标是对算法复杂度进行系统性的形式化。论文提出了一个单子 API （受 Writer monad 启发），其中计算过程同时返回一个值和一个时间成本。这种方法将时间复杂度视为一种计算效应，使得正确性和复杂度分析可以相互独立。虽然目前依赖于手动的 tick 注解，但这可以作为实现通用框架的一个轻量级起点，并计划向显式的 RAM 模型和查询模型演进。
支柱 2：日常代码的推理基础设施
该支柱旨在弥合 Lean 的形式化推理与主流命令式编程语言（如 Rust、C++、Python）之间的鸿沟。
Boole 中间验证语言 (IVL)： CSLib 引入了 Boole ，这是一种受 Boogie 启发并嵌入在 Lean 中的新型 IVL。Boole 的设计风格类似于伪代码，支持在 Lean 规范（前置条件、循环不变式、断言）之间穿插经典的命令式构造。验证流水线： 其架构包括：
转译： 将来自主流语言的代码翻译为 Boole。条件生成： 将 Boole 代码和规范转换为 Lean 验证条件 (VCs)。证明自动化： 使用 Lean 自动化工具处理这些 VCs，包括 SMT 求解器（通过 Lean-SMT）、“锤子”（如 smt 等 tactic），以及潜在的基于 AI 的证明器。
设计原则： 系统通过将 Boole 深度嵌入 Lean，优先考虑最小化的可信计算基 (TCB)。验证条件被生成为直观的 Lean 目标，从而允许它们利用支柱 1 中建立的丰富定义宇宙。
核心贡献
CSLib 框架： 引入了一个统一的、开源的用于 Lean 中 CS 形式化的库，旨在成为“计算机科学界的 Mathlib”。Boole IVL： 设计并初步实现了 Boole，这是一种中间语言，通过将命令式代码转换为 Lean 可验证的定理，从而促进命令式代码的验证。复杂度单子 API： 一种在 Lean 内部形式化算法复杂度的创新方法，能够在单一框架内同时证明函数正确性和最坏情况下的时间界限（例如，针对 MergeSort）。验证流水线架构： 一个将主流代码通过 Boole 连接到 Lean 证明的工具链的具体愿景，利用了现有的开源项目，如 Strata （用于方言的深层嵌入）和 Loom （用于浅层嵌入和验证条件生成）。
结果与当前状态
本文是一篇概述愿景和初步进展的白皮书，而非完成大规模实验结果的报告。
初步实现： CSLib 仓库已经包含了操作语义、程序等价性、自动机模型、线性逻辑以及基础排序/搜索算法的初步形式化。原型验证： 已演示了一个原型验证条件生成器。通过一个简单的循环示例（整数求和），系统成功生成了用于入口不变式、循环维护和断言的 Lean 验证条件。这些条件使用 smt tactic 得到了自动求解，该 tactic 将目标转换为 SMT 公式，求解后并在 Lean 中重放证明。路线图： 项目概述了一个 2026–2027 年的初步路线图，目标是在 2026 年底前覆盖本科水平的算法与理论，并在 2027 年底前实现一个实质性现实系统的端到端验证。
意义与主张
本文声称 CSLib 将从两个主要方面从根本上改变计算机科学研究与工程的格局：
对软件可靠性的实际影响： 通过实现从预验证组件中进行可靠系统的组合式推导，并简化 AI 在验证中的使用，CSLib 解决了在 AI 驱动的代码生成和攻击时代对安全软件的紧迫需求。它旨在使形式化验证具备商业采用的可扩展性，超越传统方法（如 seL4）所面临的“成本惩罚”。研究与 AI 的协同作用： CSLib 是 21 世纪 CS 研究的平台，允许进行具有数学基础的发现以及基础概念的大规模复用。至关重要的是，它作为一个高质量的数据仓库，用于训练用于形式化和定理证明的 AI 系统。反之，论文认为 AI 工具将加速 CSLib 本身的发展，形成一种“飞轮效应”，即人类专家与 AI 工具变得越来越高效，共同产出经过验证的知识。
作者强调，虽然 AI 生成的形式化内容存在 Bug 或缺乏人类可理解性的风险，但这些风险将通过保持“人类在环”的代码审查过程来缓解，其中 AI 仅扮演顾问角色。最终目标是实现形式化方法的民主化，使其能够被从理论学家到系统构建者的广泛计算机科学家群体所使用。
每周获取最佳 computer science 论文。
受到斯坦福、剑桥和法国科学院研究人员的信赖。
请查收邮箱确认订阅。
出了点问题，再试一次？
无垃圾邮件，随时退订。