AI4Math · Invited Talk 04 · Sorrachai Yingchareonthawornchai

来源： Invited Talk 04 · Sorrachai Yingchareonthawornchai 播客： ICML 2026 · AI4Math 分类： AI 研究 原文发表： 2026-07-11 纪要生成： 2026-07-13

基本信息

• Workshop：3rd AI for Math Workshop — Toward Self-Evolving Scientific Agents
• 类型：Invited Talk（下午 invited talk 环节首场；下午共 4 场 invited talk）
• 题目：CSLib: Towards a Lean Computer Science Library（迈向 Lean 计算机科学库）
• 讲者：Sorrachai Yingchareonthawornchai（ETH Zurich 理论研究所 Junior Fellow；CSLib 技术负责人 Tech Lead；快速图算法、组合优化、计算之组合数学专家）
• 真实时段：约 13:35–13:58（KST，7/11）
• 时间轴说明：录音 0:00 ≈ 真实 07:28；part2 文件起点为原录音 05:20:00，故真实时间 ≈ 07:28 + 05:20:00 + 段内时间。主持人开场时点明"下午 invited talk 累计只有 4 场，第一场给 Sorachai"，并介绍 CSLib 是"对 CS 算法/数据结构做正确性与计算量验证"的项目。

一句话概括

介绍 CSLib——对标 mathlib 的开源 Lean 计算机科学库：两大支柱（形式化 CS 理论基础 + 为日常代码推理提供基础设施），并现场演示如何用其 Time Monad + 自动化（grind / functional induction / simp lemma），以极短、干净的证明验证排序算法的正确性与时间复杂度。核心信条："好的库 + 好的自动化 → 证明可以很短很干净。"

背景与动机

起点在 2025 年：CS 与编程领域的形式化验证需要"扩规模"，因此需要一个大家都能用的良好公共基础设施 / 中央库。CSLib 是开源仓库，目标像 mathlib 之于数学那样在 CS 领域产生影响：收录 CS 的基础定义、主要结论、可验证软件组件与基础设施；以 mathlib 为依赖；由领域专家 curated；与 Lean 社区合作。治理结构：

• Steering group（给愿景、策略、资金）：Clark、Leo、Fabrizio 等；
• Maintainer group（技术领导与监督）：Fabrizio、Alexander、本人（Sorachai）、Chris、Kim 等。
• 在 Zulip 上有活跃讨论，欢迎所有贡献者。

主要内容

CSLib 面向谁

• 研究者：用 CSLib 基础设施验证自己的程序，用其 API 加速开发。
• 教育者与学习者：在 CS 里有统一语言，与将提供的工具交互。
• 程序员：用 CSLib 组件写可靠软件，用验证基础设施验证代码。
• AI 开发者：希望把 CSLib 做大，服务其"生产/规范程序"。
• 跨学科研究者同样适用。

两大支柱（pillar）

• Pillar 1：形式化 CS 的理论基础——应包含计算模型、逻辑、算法与数据结构的可验证分析（理论层面）。当前 CSLib 已含算法、可计算性、基础、逻辑等多个方面（可在 Lean Together 的相关报告了解更多）；增长很快，主题包括模型与逻辑、算法、数据结构、图算法等。
• Pillar 2：为"日常代码推理"提供基础设施——提供一个中间验证语言 Boo（命令式语言），支持 Lean 规范，并给出"从 Boo 代码生成验证条件（verification condition）"的机制。愿景：把 Rust 等代码翻译成 Boo，再用 Shredder 作后端生成验证语言，从而用该基础设施验证代码。使用场景：写程序时写规范 → 用 Lean 表达 → 翻译成 Boo → Boo 自动生成验证条件 → 再用 Pillar 1 的 CSLib API 做最终证明、给出 Lean 证明。

设计关键：Time Monad —— 把时间复杂度当"副作用"

设计的关键原则是在稳健性（robustness）与工效（ergonomics）间平衡。为此提供一个非常简单的 API：Time Monad——一个带大量配套 simp lemma 的 writer monad。它允许你标注（annotate）函数式代码、插入 tick 来计数程序中的操作数，从而把时间复杂度当作"副作用（side effect）"。这样做的关键优势是关注点分离（separation of concern）：正确性证明与时间复杂度证明完全独立、互不干扰，代码干净。

time m 的结构：把值的结构、返回类型、以及"时间（一个自然数）"包在一起；有 pure、bind 等基本操作（都在 CSLib 里、你无需了解细节）。要点是配套大量 simp lemma，用它时可自动化、化简。用法：先写普通 Lean 代码，再用 time m 标注，即可陈述正确性与时间复杂度定理，让 simp lemma 替你做重活。

例子（归并排序 merge sort）：从 CSLib 导入复杂度 API，把 merge sort 写成"接受两个 list、输出一个 list"，但输出放进 time m 以追踪时间（这里追踪比较次数）——在 merge 内部追踪比较次数、其余代码与普通程序一模一样。然后可陈述正确性定理（merge sort 输出是输入的排列、且有序），再单独陈述时间复杂度（如 merge sort 时间 ≤ n log n）。还计划加入更多验证技术：如用 PMF monad（概率质量函数）+ monad transformer 叠加 time monad 来表达随机算法（如 quicksort）的期望复杂度——同样保持"正确性与时间复杂度分开分析"的原则，例如展示期望代价是 n log n（如调和数）。这些陈述后续会做得更易读。

现场演示：insertion sort（functional induction + grind + Time Monad）

讲者花了一段时间走了一个 insertion sort 的现场 demo（基于其上学期教学的 tutorial），要点是"若有好的公式化与库，证明可以很短很干净"：

1. 定义 insertion sort 为函数：取一个 list，递归地把队首元素插入到已排序的其余部分；可 #eval 得到排序结果。
2. 证正确性 + 用 grind 自动化：用归纳类型定义"有序（sorted）"（空 list 有序；若 a 是列表最小元、则 a 接在有序尾部仍有序）。用functional induction（函数式归纳）——最自然的按归纳思路——证"insertion sort 输出有序"。演示中先展示"手写要多少行代码"，再展示 grind（Lean 里基于 SMT 求解器的自动化 tactic）能把这些消掉：某些目标 grind 直接闭合，一些需要给点提示（如告诉 grind 该调用某函数）后也能闭合。结论：会用 grind/自动化后，可擦掉大量手写行——原来三条引理的证明用一行"全部 grind"搞定。功能归纳 + grind 让验证 quicksort 之类用几十行（约 50 行级）即可、不需要很多行。
3. 加时间复杂度（Time Monad）：用 CSLib.Algorithm.… 的 time m。把普通 insertion sort 的输出改成 time m：把 time 想成一个"盒子"，盒里含"计数的数字"和输出；只需在做比较处插入一个 tick（+1），其余代码与之前完全一样，但现在也追踪运行时间（比较次数）。#eval 可看到它同时给出输出与时间。还能证"带时间版程序的输出与不带时间版一致"（用 functional induction）。最后分析时间复杂度：陈述"insertion sort 在 list x 上的时间复杂度是 n²（length × length）"，用同样的 functional induction 得到一个初看"有点吓人、含多部分"的目标，但用 CSLib API（time m 会给出可展开的东西）自动展开后目标变得可控，再补几条中间引理即可；simp lemma 替你把正确性那部分处理掉。要点：证时间复杂度时无需操心正确性，可进一步压缩证明。"用大量自动化写短证明"是通向更简洁、更可扩展证明的方向。

现状与征集贡献

demo 结束后小结：想让大家看到 Lean 的能力与 CSLib 已提供的基础功能。CSLib 在多个方向有进行中的活动、也欢迎新贡献：

• Pillar 1：算法、图算法、自动机等；
• Pillar 2：基础设施——欢迎规范、以及把真实编程语言翻成 Boo 的前端、和"接收 Boo 程序 + 形式规范、在 Lean 里构造证明义务"的后端。 方向都很开放，欢迎更多贡献。

关键结论 / Takeaways

• CSLib 志在成为"CS 领域的 mathlib"：Pillar 1（理论基础）+ Pillar 2（Boo/代码推理基础设施）两条腿走路，以 mathlib 为依赖、专家 curated。
• Time Monad 用"副作用"思路把时间复杂度与正确性证明解耦（关注点分离），配合 grind / functional induction / simp lemma 让证明短而干净（如 insertion sort：正确性靠归纳+grind，复杂度 n²）。
• 计划用 monad transformer 叠加（PMF + Time）支持随机算法期望复杂度。
• 处于早期快速成长、开放征集贡献阶段。

Q&A / 讨论亮点

• Q（一位做 CS 自动形式化的研究者，提两个问题）： ① CSLib 对"自动形式化产物"（相对传统人工手写规范）持什么态度？这类贡献会被 CSLib 接受吗？ ② CSLib 的长期发展方向——更偏理论 CS，还是也向机器学习等更广的实用方向延伸？ A： ① 若用 AI 自动形式化某物、能否给 CSLib 提 PR？总体上 CSLib 与 mathlib 政策一致：不禁止用 AI，但代码质量要足够好、达到 reviewer 认可的标准；是否 AI 生成并不重要，质量够好就会接受。 ② 长期目标：Pillar 1 是 CS 的理论基础（广义解读），计划扩到量子计算乃至密码学（正在找愿意领导 CSLib 密码学方向的负责人），该方向很开放；Pillar 2 偏实用，关于"真实世界编程语言的代码推理与验证"。（讲者致谢结束。）

名词 / 引用

• CSLib / mathlib：Lean 计算机科学库 / 数学库（CSLib 以 mathlib 为依赖）。
• Boo / Shredder：中间验证语言（命令式）/ 生成验证语言的后端。
• Time Monad / tick / time m / writer monad / PMF monad：把复杂度当副作用的 API 与随机算法扩展。
• grind / functional induction / simp lemma：Lean 的 SMT 自动化 tactic、函数式归纳、化简引理。
• Pillar 1 / Pillar 2：理论基础 / 代码推理基础设施两大支柱。
• 讲者个人主页底部有可交互 demo 链接（现场用的即此）。

原文发表：2026-07-11  ·  纪要生成：2026-07-13