数学与计算
数、证明、图和机器,不仅通过演绎,也通过计算来研究。
数学和计算机科学现在也通过模拟来检验自己的想法。它们生成数百万个随机图,看什么是典型的。它们运行一台机器,看一个算法实际做了什么。它们一次又一次地攻击一个密码,以了解它如何失效。这些都不是在描述物理世界。它探索的是数、结构和计算本身的空间。这种做法的跨度很大,从几个世纪以来手工进行的实验数学,到今天在设计建成之前就对每一个可达状态进行检查的验证工具。
随机矩阵实验
填满随机数的大矩阵,反复对角化,以研究其本征值的统计特性。
它回答的问题: 随机矩阵的本征值会稳定成什么样的图案,它与数学和物理的其他领域吻合吗?
略去了: 只对无穷多种可能矩阵中极小的一角进行采样。
运行于:约 1012 FLOPS 粗略 大学集群,生成并对角化许多大型矩阵自: 1955 Wigner 对随机矩阵本征值统计的早期工作
随机图实验
按随机规则逐个节点或逐条边生成图,看哪些性质(如连通性或聚类)通常会出现。
它回答的问题: 在这种添加节点和边的规则下,“典型”的网络是什么样子?
略去了: 真实世界的网络很少像生成模型的规则那样干净。
运行于:约 1010 FLOPS 粗略 在台式机上运行,可处理多达数百万个节点的图自: 1959 Erdős 和 Rényi 的随机图模型
渗流模拟
一个晶格或网络,其中的格点或键被随机打开,观察连通路径在哪个点突然贯穿整个系统。
它回答的问题: 在多大的密度下,一个随机网络会突然变得首尾连通?
略去了: 理想化的晶格比任何真实的多孔材料或网络都更规整。
运行于:约 1010 FLOPS 粗略 一台台式机,用于大规模格点扫描自: 1957 Broadbent 和 Hammersley 提出渗流理论
实验数学搜索
对模式、反例或数字间精确关系的暴力数值搜索,规模远远超出人工所能检查的范围。
它回答的问题: 这个猜想对所有人有条件逐一检验的情形都成立吗,是否会出现某种规律?
略去了: 无论检验过多少个成立的案例,都不能算证明。
运行于:约 1011 FLOPS 粗略 大学集群,一次搜索运行数天自: 1963 到 1963 年,计算机搜索整数关系和素数规律
常数的蒙特卡罗估计
用随机抽样来估计数学常数或积分,例如撒点来估计面积,这是练习,而不是物理模型。
它回答的问题: 仅靠盲目的随机抽样,能多准确地确定一个精确的数学量?
略去了: 收敛速度比几乎任何更复杂的数值方法都慢得多。
运行于:约 109 FLOPS 粗略 在笔记本电脑上运行数秒到数分钟自: 1946 Ulam 在 1946 年的想法;冯·诺依曼在 1947 年 3 月提出了电子计算机版本,该方法于 1949 年首次发表 来源在模拟树中: 蒙特卡罗方法
计算数论搜索
对大数进行素性检验、分解质因数,或搜索完全数等特殊性质,用的是大规模运行的算法,而不是手算。
它回答的问题: 这个巨大的数是否具有我们要找的性质,搜索又能把纪录推进多远?
略去了: 破纪录的搜索,对没有人想到去检验的数几乎没有说明。
运行于:约 1013 FLOPS 粗略 一个分布式志愿计算项目,分布在许多捐赠出来的机器上自: 1951 Lucas 的梅森素数手工检验,1951 年首次由计算机运行
混沌吸引子数值计算
一小组非线性方程被逐步积分,展现对初始条件的敏感依赖和分形吸引子。
它回答的问题: 为什么一个简单的确定性系统会变得不可预测?
略去了: 数值舍入意味着一条长轨迹不是真正的轨道,只是一条始终贴近某条真轨道的轨迹。
运行于:约 103 FLOPS 粗略 几个方程,在笔记本电脑上数秒。自: 1963 Lorenz 的确定性非周期流,一个在计算机上运行的对流模型。 来源在模拟树中: 洛伦茨的混沌对流
非线性晶格实验
一串用非线性弹簧相连的质量块,从单一模式启动,观察能量是否像热力学所预期的那样均匀扩散。
它回答的问题: 非线性链会不会把能量平均分给它所有的运动?
略去了: 结果取决于所选的链和初始状态。
运行于:约 103 FLOPS 粗略 按现代标准来看微不足道;最初的版本用了几十个质量块。自: 1955 Fermi、Pasta 和 Ulam 在早期数字计算机上对非线性问题的研究。 来源
孤子数值实验
在网格上求解非线性波动方程,观察脉冲相互穿过后仍保持形状,线性波做不到这一点。
它回答的问题: 为什么有些非线性波会彼此穿过而保持不变?
略去了: 它展示的是一族方程,而不是非线性波的一般行为。
运行于:约 104 FLOPS 粗略 一维网格,今天轻而易举。自: 1965 Zabusky 和 Kruskal 关于无碰撞等离子体中孤子相互作用与初始状态回归的研究。 来源
分形集渲染
在复平面的每个位置上检验一个简单的迭代公式,看它是否发散,由此画出稳定点集合的边界。
它回答的问题: 一个简单迭代保持有界的那个集合是什么形状?
略去了: 逃逸检验只能提示一个点是否属于该集合,而这幅图只是对一个无限精细的集合做的有限分辨率采样。
运行于:约 109 FLOPS 粗略 深度缩放需要在数百万个点上做扩展精度的迭代。自: 1980 Mandelbrot 的 z 到 lambda z(1-z) 迭代的分形特征,曼德博集合的首批计算机图像。 来源
沙堆自组织临界性
把沙粒投到网格上,坡度太陡就会倒塌,无需调参就能产生各种大小的雪崩,用来模拟系统如何达到临界状态。
它回答的问题: 为什么各种大小的雪崩无需任何调节就会出现?
略去了: 真实系统是否共享同样的标度,存在争议。
运行于:约 109 FLOPS 粗略 在大型网格上做长时间运行,以观察缩放规律。自: 1987 Bak、Tang 和 Wiesenfeld 的自组织临界性:对 1/f 噪声的一种解释。 来源
黎曼 zeta 零点计算
计算黎曼 zeta 函数沿其临界线的取值,以定位并数出它的零点,检查它们是否都落在猜想所说的位置。
它回答的问题: ζ 函数所有的非平凡零点是否都在同一条直线上?
略去了: 无论多长的有限检验,都无法证明在它之外不存在偏离临界线的零点。
运行于:约 1018 FLOPS 粗略 最大规模的搜索要花数十年的 CPU 时间。自: 1953 图灵对黎曼 zeta 函数的计算。 来源
用计算机算 π 的位数
用精确算术把 pi 的级数求和到极其庞大的位数,既检验这个数,也检验这台机器。
它回答的问题: π 的各位数字看起来是随机的吗,这台机器在这个规模上可信吗?
略去了: 这些数字并不能回答任何悬而未决的问题,而只有方法相互独立,核对才能发现硬件错误。
运行于:约 1017 FLOPS 粗略 在服务器上花数月,计算数百万亿位数字。自: 1950 Reitwiesner 在 ENIAC 上把 pi 和 e 算到 2000 多位小数(1950 年发表,重印于《Pi: A Source Book》)。 来源
AI 引导的猜想发现
机器学习分析大型数学对象表格,找出哪些性质相互关联,提出一个猜想,再由数学家去尝试证明。
它回答的问题: 这些数学量之间有哪些尚未看到的关系,值得去证明?
略去了: 它只能提示规律,本身什么也证明不了,而且数据中的某些规律可能是数据产生方式造成的假象。
运行于:约 1015 FLOPS 粗略 每个数据集在几块 GPU 上数天。自: 2021 Davies 及其同事用 AI 引导人类直觉来推进数学。 来源
学习型算法与构造搜索
一个会玩游戏的系统或语言模型系统搜索新的流程或数学对象,由计算机检查每个候选是否正确。
它回答的问题: 程序能否发现比人类找到的更快的算法或更大的例子?
略去了: 每个结果都只是一个新例子,而且搜索只涵盖设计者把它设定成游戏的那类对象。
运行于:约 1017 FLOPS 粗略 在加速器集群上数天到数周。自: 2022 Fawzi 及其同事的 AlphaTensor,用强化学习发现更快的矩阵乘法算法。 来源
模型检验
有限系统(比如协议或电路设计)的每一个可达状态,由计算机穷举,检验某个性质在所有状态下都成立。
它回答的问题: 有没有任何可达的状态,使这个设计违反自己的规则?
略去了: 状态空间的膨胀超出了可检验的范围,所以实际设计要先做简化。
运行于:约 1012 FLOPS 粗略 大学集群,穷尽一个庞大但有界的状态空间自: 1981 Clarke 和 Emerson 提出模型检验
自动定理证明搜索
在逻辑推理链上做搜索,由计算机逐步生成,寻找一个数学命题的证明或反证。
它回答的问题: 从公理到这个命题,是否存在一条有效的逻辑推理链?
略去了: 找到没有人会选的证明,有时在可及范围内连一个也找不到。
运行于:约 1011 FLOPS 粗略 大学集群,搜索数小时到数天自: 1956 逻辑理论家,一个早期的自动证明搜索程序
SAT 与约束求解
系统地搜索数百万种真假值的组合,以满足一大组逻辑约束,用于调度、布线或验证设计。
它回答的问题: 有没有一种赋值方式,能同时满足所有这些约束?
略去了: 有些实例难到无论多好的求解器,都无法在时限内算完。
运行于:约 1011 FLOPS 粗略 工作站到集群,视问题规模而定自: 1962 用于可满足性搜索的 Davis-Putnam 过程
密码攻击建模
一种密码或密钥交换方案在模拟中被攻击数百万次,手段包括暴力破解、统计偏差或建模出的弱点,以衡量破解它实际需要多少功夫。
它回答的问题: 要破解这个,实际上需要多少次运算,这个数字是否仍然大得安全?
略去了: 只检验分析员想到去建模的攻击,而不是还没有人发现的那一种。
运行于:约 1014 FLOPS 粗略 由许多机器组成的分布式集群,运行攻击试验自: 1976 到 1976 年,对密码和密钥交换强度的计算分析
旁路泄漏模拟
在设备执行密码运算时,对它的功耗、时序或电磁辐射建模,看外面的窃听者能从中得知什么。
它回答的问题: 有多少密钥信息通过设备的物理行为而不是数学泄漏出去?
略去了: 实验室条件捕捉到的信号,比一台有噪声的真实设备通常泄露的更干净。
运行于:约 1010 FLOPS 粗略 工作站,为一个器件的功耗或时序轨迹建模自: 1996 Kocher 对密码实现的计时攻击的演示
安全协议验证
通信协议中攻击者可能发送、重放或伪造的每一条消息,由计算机穷举,检验能否从中逼出秘密或身份。
它回答的问题: 有没有任何一串消息能骗过这个协议,让它泄露秘密或接受伪造的身份?
略去了: 它验证的是按规定描述的协议,而不是真实实现所走的捷径。
运行于:约 1011 FLOPS 粗略 工作站到集群,检查一个协议的消息空间自: 1989 Dolev-Yao 模型,协议验证的奠基性基础
通过穷尽情形检查的计算机辅助证明
一个定理被归结为有限个情形,每一个都由程序验证,因为没有哪个人能把它们全部检查一遍。
它回答的问题: 能否由机器逐一检查每一种情形,来完成一个证明?
略去了: 信任转移到程序、硬件和案例化简的论证上。
运行于:约 109 FLOPS 粗略 原版在大型机上约需一千小时;如今少得多。自: 1977 Appel 和 Haken 证明每张平面地图都可以四色着色,用的是由计算机验证的可约性。 来源
可验证数值计算
带有保证界限的计算,因此一个数值结果可以证明一个数学命题,比如混沌吸引子的存在。
它回答的问题: 计算得出的答案能否被证明是正确的,而不只是大概准确?
略去了: 界限在长时间后可能爆炸式增大,使证明只限于短时间或行为良好的问题。
运行于:约 109 FLOPS 粗略 区间算术把成本乘以一个不大的系数。自: 2002 Tucker 的严格常微分方程求解器和 Smale 第 14 问题,证明了洛伦兹吸引子的存在。 来源
图灵机枚举
让一台极简机器的每一个小程序都运行一遍,看哪些会停机、哪些永远运行,找出每种规模中运行最久的停机程序。
它回答的问题: 一个很小的程序在停止之前最多能运行多久?
略去了: 不可判定性意味着有些机器无论运行多久,都永远无法归类。
运行于:约 1015 FLOPS 粗略 数十亿台机器,对不停机的那些给出证明。自: 1965 Lin 和 Rado 对图灵机问题的计算机研究。 来源
统计模型检验
对一个带有随机行为的系统多次模拟,以有把握地估计它违反某个性质的可能性有多大。
它回答的问题: 一个随机系统违反安全规则的可能性有多大?
略去了: 统计运行给出的是带置信水平的概率,而不是证明;罕见的故障需要用重要性抽样。
运行于:约 109 FLOPS 粗略 数千到数百万次采样执行。自: 2002 Younes 和 Simmons 用接受抽样对离散事件系统做的概率验证。 来源
模糊测试
给程序输入海量的随机或变异输入,找出会让它崩溃的那些,实际上是在模拟一个充满敌意或粗心的世界。
它回答的问题: 什么样的输入会让这个软件出故障?
略去了: 它只能找出随机输入触及的故障,而一个程序可能多年通过测试,却把缺陷藏在罕见的情形后面。
运行于:约 1014 FLOPS 粗略 一个大型代码库需要数机器年的 CPU 时间。自: 1990 Miller、Fredriksen 和 So 对 UNIX 工具可靠性的实证研究。 来源
符号执行
用符号写出未知输入来运行程序,收集每条路径上的条件,再由求解器找出能走到每个分支的取值。
它回答的问题: 哪些输入能让这个程序的每条路径运行起来,其中有没有一条会触及漏洞?
略去了: 路径数随程序规模呈指数增长,所以大型程序只能覆盖一部分。
运行于:约 1012 FLOPS 粗略 每个程序数小时的求解时间,随路径数量急剧增长。自: 1976 King 的符号执行与程序测试。 来源
抽象解释
在一组可能的取值(比如区间)而非单个值上运行程序,以证明对每一个输入都成立的性质。
它回答的问题: 这个程序对于任何输入,会不会出现除以零或溢出?
略去了: 安全近似会引发误报,所以人们仍然必须检查每一条警告。
运行于:约 1011 FLOPS 粗略 大型航电代码库需要在工作站上数小时。自: 1977 Cousot 和 Cousot 的抽象解释,一种用于程序静态分析的统一格模型。 来源
有界模型检验
一个设计在固定步数以内的行为被写成逻辑公式,交给可满足性求解器,去找通向漏洞的任何一条短路径。
它回答的问题: 这个电路或程序能否在给定的步数内到达错误状态?
略去了: 除非另有论证表明这个界足够,否则它除了步数上限之外什么也证明不了。
运行于:约 1013 FLOPS 粗略 每处房产在服务器上数小时。自: 1999 Biere, Cimatti, Clarke and Zhu's symbolic model checking without BDDs. 来源
基于性质的随机测试
陈述一条应当始终成立的规则,由计算机生成许多随机用例,并把任何失败缩小成一个很小的反例。
它回答的问题: 这段代码在广泛的输入下,是否遵守它自己的规范?
略去了: 随机案例可能永远碰不到罕见的情形,而且写下的性质未必是真正重要的那个。
运行于:约 109 FLOPS 粗略 在笔记本电脑上数分钟,处理数千个案例。自: 2000 Claessen 和 Hughes 的 QuickCheck,一个用于 Haskell 程序随机测试的轻量工具。 来源
神经网络验证
约束求解器证明,对某个区域内的每个输入,神经网络的输出都保持在界限之内,而不是用样本去测试。
它回答的问题: 对输入做一点小改动,网络是否可能给出错误的答案?
略去了: 证明只能扩展到小型网络,而且可以检验的扰动集合很窄。
运行于:约 1013 FLOPS 粗略 在服务器上数小时到数天,用于一个小型网络。自: 2017 Katz 及同事的 Reluplex,一个用于验证深度神经网络的 SMT 求解器。 来源
计算机体系结构模拟
按指令逐条为一个拟议处理器的流水线、缓存和分支预测器建模,在芯片造出之前估算它的速度。
它回答的问题: 在真正流片之前,这种处理器设计运行真实程序能有多快?
略去了: 对真实芯片简化得足够多,所以最终的硅片总会和模型有些差异。
运行于:约 1011 FLOPS 粗略 大学集群,让基准程序在模型上运行自: 1990 到 1990 年,用于体系结构研究的周期精确处理器模拟器
分布式系统与共识模拟
许多台计算机被建模为彼此发送消息,消息有延迟、丢失和故障,用来检验分布式算法是否仍能就正确答案达成一致。
它回答的问题: 当消息丢失、延迟或节点崩溃时,这个算法是否仍能达成正确的一致?
略去了: 注入的故障是设计者预料到的,而不是生产中意外出现的。
运行于:约 1010 FLOPS 粗略 模拟数百个虚拟节点的集群自: 1978 Lamport 早期关于分布式系统中排序与故障的研究
存储系统模拟
对磁盘、驱动器和文件系统如何排布数据、出故障和恢复进行建模,在购买真实驱动器并写满之前测试存储设计。
它回答的问题: 这种存储设计的性能和抗故障能力如何,而规模大到先做真实测试代价太高?
略去了: 真实的硬盘失效方式比模型的随机失效率更杂乱、更相关。
运行于:约 1010 FLOPS 粗略 工作站到小型集群,为一个存储阵列建模自: 1988 到 1988 年,磁盘阵列可靠性的模拟模型
操作系统调度器模拟
对一连串计算任务到达并争夺处理器的过程建模,在不同的调度规则下运行,看哪种最公平或最快。
它回答的问题: 哪种给任务队列排序的方式能完成最多的工作,或对每个任务最公平?
略去了: 合成的工作负载很少能与真实机器遇到的那种不规则的任务组合相符。
运行于:约 109 FLOPS 粗略 在笔记本电脑或工作站上运行数秒到数分钟自: 1968 到 1968 年,对处理器调度策略的模拟研究
编译器与程序优化搜索
对一段代码尝试并测量海量的小变体,寻找完成同样工作的最快或最短版本。
它回答的问题: 在所有等价的写法中,这一小段代码究竟哪一种最快?
略去了: 找到的程序有时非常古怪,以至于无法解释它们为什么管用。
运行于:约 1010 FLOPS 粗略 在庞大的代码变体空间中搜索的集群自: 2006 到 2006 年,对短指令序列的超级优化搜索
算法性能的经验测试
让一个算法在随机生成的或真实世界的、规模逐渐增大的输入上运行数千次,测量它的运行时间实际上如何增长,而不是在纸上证明。
它回答的问题: 在它真正会遇到的输入上,这个算法的运行时间在实践中究竟如何增长?
略去了: 测试输入里没有出现的最坏情况,在它发生之前一直不会被发现。
运行于:约 109 FLOPS 粗略 在工作站上对许多生成的测试输入运行自: 1970 到 1970 年,对算法运行时间的系统性经验测试
语言模型程序执行
语言模型在追踪一个程序会算出什么时,逐步写出中间状态。
它回答的问题: 语言模型能否模拟代码的运行?
略去了: 输出不保证正确,长程序会失败。
运行于:约 1014 FLOPS 粗略 每次查询推理自: 2021 Show your work: scratchpads for intermediate computation with language models (2021) 来源
区块链共识模拟
一个节点网络在延迟下产生并共享区块,用来测试区块大小、时序和攻击者如何影响安全性与吞吐量。
它回答的问题: 在网络延迟和攻击下,区块链有多安全、多快?
略去了: 真实的节点行为和网络拓扑只测到了一部分。
运行于:约 108 FLOPS 粗略 对数千个节点做事件驱动的运行。自: 2016 Gervais 及其同事用模拟器对工作量证明区块链的安全性和性能所做的分析。 来源
并行离散事件模拟
一个按时间推进的事件模拟被分散到许多处理器上,各自推进自己的时钟,有处理器来晚了就回滚。
它回答的问题: 像网络或战场这样庞大的事件驱动模拟,怎样才能在许多台机器上快速运行?
略去了: 回滚可能连锁发生,而加速的程度在很大程度上取决于事件之间耦合得有多紧。
运行于:约 1014 FLOPS 粗略 在超级计算机上数小时,处理数十亿个事件。自: 1985 Jefferson 的虚拟时间,即用于乐观同步的 Time Warp 机制。 来源
图形处理器架构模拟
一块图形处理器的核心、线程束和内存被逐周期建模,运行真实程序,在制造之前评估设计。
它回答的问题: 设计的改变会如何影响图形芯片上并行程序的速度?
略去了: 真实芯片的细节是保密的或未知的,所以模型只是大致匹配现有设计的数字。
运行于:约 1012 FLOPS 粗略 每模拟一秒的执行,需要数小时到数天的主机时间。自: 2009 Bakhoda 及其同事用详细的 GPU 模拟器对 CUDA 工作负载所做的分析。 来源
FPGA 加速的系统模拟
把芯片设计载入许多可重构电路,以兆赫的速度逐周期精确运行,模拟整台服务器以及由它们组成的网络。
它回答的问题: 这个处理器及其集群运行真实软件时会有怎样的表现,在它被造出来之前?
略去了: 它比真实芯片慢得多,而且放不进电路的设计就运行不了。
运行于:约 1015 FLOPS 粗略 在数百个可重构电路组成的云上运行数天。自: 2018 Karandikar 及同事的 FireSim,在公有云中用 FPGA 加速的周期精确横向扩展系统模拟。 来源
全系统模拟
整台计算机,包括处理器、内存、磁盘和网卡,被模拟得足够好,能启动未经修改的操作系统并运行其中的程序。
它回答的问题: 真实的软件在一台尚不存在的机器上会有怎样的表现,或者在可以随意暂停和重放的机器上呢?
略去了: 为了速度,时序是近似处理的,所以它给不出精确的性能,只能给出功能行为。
运行于:约 1011 FLOPS 粗略 每台被模拟的机器在服务器上接近实时运行。自: 2002 Magnusson 及同事的 Simics,一个全系统模拟平台。 来源
轻量级网络仿真
数十或数百台虚拟主机和交换机在一台笔记本电脑上运行真实的网络软件,由设定了速度和延迟的仿真线缆连接。
它回答的问题: 这套网络控制程序在部署之前,能在整个拓扑上正常工作吗?
略去了: 宿主自己的处理器由所有虚拟节点共用,所以高速链路会被拖慢。
运行于:约 1010 FLOPS 粗略 在一台工作站上实时运行。自: 2010 Lantz、Heller 和 McKeown 的“A network in a laptop”,软件定义网络的快速原型。 来源
模拟退火
计算机缓慢冷却一个原子模型或一种设计,有时接受更差的排列,从而为困难的优化问题找到好的解。
它回答的问题: 在天文数字般多的可能性中,接近最佳的布局或日程是什么?
略去了: 它不保证得到最优解,结果还取决于降温方案。
运行于:约 1012 FLOPS 粗略 一次芯片布局需要在工作站上数小时。自: 1983 Kirkpatrick、Gelatt 和 Vecchi 的模拟退火优化。 来源
近似贝叶斯计算
用许多试验参数值运行模拟器,保留那些产生的数据接近观测数据的值,从而看出哪些值是合理的。
它回答的问题: 一个复杂模型的哪些设置,可能产生我们观察到的数据?
略去了: 结果取决于用了数据的哪些概括,以及要多接近才算匹配。
运行于:约 1013 FLOPS 粗略 在集群上运行数百万次模拟器。自: 1997 Tavaré 等人用模拟从 DNA 序列数据推断溯祖时间。 来源