受访者：邓玉欣（上海财经大学教授，CCF杰出会员）
采访时间：2025年11月7日星期五
采访人：王劲博
序
2025年10月9日下午，中国科大高新校区GT-B211教室内，华夏计算机科技英才班第41期学术讲座如期举行。上海财经大学教授、CCF杰出会员邓玉欣老师以《形式化方法及其应用》为题，为师生们揭示了如何用严密的逻辑系统为计算机软硬件构建安全基石，让人意犹未尽。
为此，2025年11月7日，我们对邓玉欣教授进行了一次深度回访。在这篇访谈中，邓教授不仅回应了同学们关于“邓引理”与概率语义的学术追问，更将视野延伸至自动驾驶、卫星网络等前沿应用，深入探讨了形式化方法与大模型、量子计算的跨界碰撞，并对科大学子提出了“厚积薄发”的殷切期望。
【形式化方法篇】
一、数字世界的“安检员”：从自动驾驶到卫星网络
Q1：
第一个问题和TCS（理论计算机）和软硬件系统的结合有关系。科大计算机学院的一个传统的方向是体系结构。不过，近些年来，学院同样非常注重TCS方向的发展，并在去年创立了TCS方向的英才班，吸引了不少同学们的兴趣。有同学提了这样一个问题：您是否认为把计算机的软硬件系统利用逻辑系统转化为数学对象进行研究这件事情，在今天会比以往更加重要呢？
邓玉欣：
这个领域一直都很重要。形式化方法这个领域，我上次也着重介绍过，从80年代开始，大家就在探索如何验证程序的正确性。到今天，它仍然同样重要，甚至更为重要，因为现在的软件产品、硬件产品和信息系统无处不在，其重要性在多个层面都有所提升。
许多安全攸关的领域，例如火车、汽车的控制系统，以及现在的自动驾驶技术，这些在以前并不存在。还有火箭、卫星等领域，虽然以前也有，但现在应用更广泛。随着低轨卫星的发射增加，互联网正在向卫星网络扩展，这个领域将来仍然非常重要，因为这些系统需要尽可能避免错误，一旦发生错误，后果可能非常严重。总之，现在应用场景更多，因此显得更为重要，依然有很多工作要做。
二、理论的幽微：从“邓引理”到概率语义
Q2：
在您进行报告之前，科大计算机学院为您的报告制作了一张宣传海报。有些同学读了海报后，特别关注上面列出的学术成果，但您的讲座中似乎没有怎么提及这些内容，因此同学们感到有些遗憾，并向我提出了几个问题。同学们的问题主要围绕两个方面：第一个问题是关于您提出的“邓引理”（Deng Lemma），有的同学好奇它解决了并发系统中的哪些形式化问题？
邓玉欣：
形式化方法中有一种称为CCS（Calculus of Communicating Systems）的建模语言，是爱丁堡大学的Robin Milner在上世纪80年代提出的。CCS是一种形式化语言，可以描述并发系统，比如说网络通信协议中的消息交换与握手过程。
描述完成后，一般还需要验证所描述协议的正确性。通常，我们会将实际实现与规约进行等价性验证，即判断两者在语义上是否等价。在CCS中，Milner提出了互模拟（bisimulation）的概念，并设计了一套等式公理系统，用于通过语法推导来验证语义等价性。
此后，还出现了多种互模拟的变体，特别是在弱互模拟（weak bisimulation）中，至少出现了五种不同的互模拟关系，并分别对应了各自的公理化系统。我在2007年的一项工作中指出，这五种关系的完备性证明，实际上可以在一个统一的框架内完成。只需在证明过程中根据不同的互模拟关系替换部分公理，整体框架就可以保证是一致的。
这项工作的潜在应用在于，其可以为形式化工具提供支持，例如在定理证明器，比如说Coq中实现等式推导的自动化。通过将公理编码到系统中并制定相应策略，可以将手工推导过程转化为机械化操作，从而提高效率。
Q3：
海报上除了提到“邓引理”，还提及您的一本英文专著《概率进程语义：一种操作式方法》，我了解到这本书系统推进了概率并发理论。第二个问题是：如果您要向一位对TCS领域了解不多的低年级同学介绍这本书的核心思想，您会如何概括？
邓玉欣：
我经常喜欢拿网络通信协议来做例子，大家也总喜欢用这个作为并发系统的例子。早期，大家一般只考虑系统做或不做某件事情，也就是确定性行为。实际上，现实情况可能更复杂一点。比方说，从主机A到主机B发送一个数据包，可能这个数据包有一定概率会丢失，假设数据包有99%的概率顺利到达主机B，有1%的概率丢包。那万一丢了以后该怎么办？可能需要重新发送。为了更精确地描述这类系统，肯定需要在模型中引入概率信息。
有了这种概率协议以后，它的规范和最后的实现之间是不是等价的？这本书主要研究对象是概率互模拟（probabilistic bisimulation），就是在考虑概率信息的情况下，怎么验证规约与实现之间的等价性。
追问：
我的理解是，您在高并发的环境下加入了更符合实际的概率信息，这样一来形式化系统里的规约和现实中的实现会更接近？
邓玉欣：
是的，可以这么理解。以前的工作不是很重视概率，现在这个描述更准确了一点
【前沿趋势篇】
一、新范式的碰撞：形式化方法与AI、量子的融合
Q4：
有的同学注意您长期活跃在各大TCS顶会的编委会，同学们想问一下，从国际前沿的方向来看，您觉得形式化方法最近几年的几个重大趋势是什么呢？
这几年大家受到AI的影响确实都比较大。我觉得可能有两个大趋势，一个是形式化方法和和AI结合，另一个是形式化方法和量子计算结合，这两个方向目前较为活跃。
形式化方法与AI的结合，特别是“可信AI”方向，主要是将传统的形式化方法和AI结合起来，确保AI系统的安全与可靠性，不过我本人并不做这一方面的工作。
另外一个趋势是形式化方法与量子计算的结合，包括量子编程语言的设计、形式化语义以及量子程序正确性验证。我们之前和一些同行合作设计了量子编程语言，这几年也做了一些和量子程序的形式化语义相关的工作。比方说，一个量子程序，或者一个量子算法写下来，在给定的一个前置条件下执行这个量子程序，如何验证它是否正确的？这个问题也可以用形式化方法去解决。
二、产业落地：国产软硬件的安全屏障
Q5：
计算机科学的传统方向除了体系结构之外，还有操作系统、软件工程以及数据库等诸多比较老牌的方向。在目前一个国产基础软硬件系统兴起的浪潮下，比如说自研的操作系统内核这些领域，您觉得形式化方法最先产生可量化收益的几处突破口，可能会在哪个领域？
邓玉欣：
嗯，很好的问题，这几年这些领域其实已经有实际的应用了。比如说，华为的鸿蒙内核开发中就采用了形式化验证的方法，一边开发一边验证。还有一个方面就是航空航天，一些航天领域的操作系统确实也在使用形式化方法。
除了我刚才说的操作系统验证，在汽车电子和航空领域，某些国际标准（如ISO 26262、DO-178C）也要求对载具的控制系统进行形式化验证并达到一定标准，以满足安全认证要求。随着国产飞机、汽车等产业的发展，形式化方法在这些领域的需求会进一步增加。
【量子计算篇】
一、跨界量子：计算机学子的数学底气
Q6：
科大量子计算的研究氛围浓厚，激发了多专业学生的兴趣。您在讲座中没有太多涉及量子计算内容，一些同学觉得有一些遗憾，提了很多问题。接下来的两个问题都是和量子计算相关的。第一个问题是，计算机专业的学生可能较好地掌握计算机相关地知识，但是物理学知识储备相对物理专业的学生而言较少。您认为，计算机背景的同学而言，理解量子计算的关键难点在哪里？
邓玉欣：
我觉得，传统TCS的学生其实不必害怕。如果想涉足量子计算领域，更重要的可能是数学基础课，比方说线性代数，高等数学。线性代数这些课程学好了之后，后面再学量子力学相关的东西，不会是大问题。
大学主要培养的是学习能力，并不是也不可能在大学里面就把将来要要用的东西都学会，这太难了。另外，事情都是在变化的，工作中或者研究中的兴趣和题目，也是会慢慢发生变化的，所以最主要的是打好专业基础和培养学习能力，做到碰到新鲜的事物不害怕。其实，我原来也不懂量子计算，直到差不多2011年左右才开始看相关的一些资料，我现在也是在边学边做这方面的一些研究，我觉得这是很正常的。
所以说，在本科阶段，我倒是建议把基础打好，那些数学课要认真学一学；因为经常要读英文的文献，外语也要学好，这样就可以了。
二、赛道选择：编程语言、算法与ISA
Q7：
第二个问题是，量子计算的哪些方向最值得他们投入精力去结合自身优势来探索呢？
邓玉欣：
在量子计算这个场景下，传统的一些问题，比如说计算复杂性问题可能和传统TCS比较接近。设计量子编程语言，研究他们的形式化语义，和传统的程序语言研究也比较类似。我觉得传统做TCS的人没问题，完全可以切入进来做量子计算。不过TCS背景的研究者对硬件方面可能没有太多的了解，所以可能在一些偏硬的方向上稍微有些难入手。
当然，如果体系结构学得好的话，在量子计算领域也可以设计指令集，然后研究高效的编译方法，我觉得这也是比较重要，而且很有意思的一个方向，同学们也可以考虑。
另外，量子算法也是很重要的一个方向，我刚才没有提及。现在量子计算机究竟能做什么也是大家关心的问题，研究设计好的量子算法，解决传统计算机难以解决的一些问题，也是一个重要方向。
三、尺度之辩：微观物理与宏观架构的差异
Q8：
刚才听到您的回答，我突发奇想：微观的量子领域，和宏观的物理世界有很大不同，您认为在量子尺度和计算机体系结构方向传统的寄存器传输级别的尺度这两个尺度下，两个ISA（指令集架构）的设计会不会有什么差异呢？
邓玉欣：
肯定还是有很大的差别的。目前，量子计算的很多基本操作，偏硬件的方面，都是物理学家在实现，比如操控单个原子和读写量子信息。很多时候，我们是在他们工作的基础上，再去做后面其他的一些设计。
追问：
可不可以这么理解，有比较良好的体系结构基础的计算机科学家把ISA提出来，然后物理学家去把这个ISA实现出来？
邓玉欣：
可以的。比方说，要实现单个指令，需要如何控制单个量个比特，这些知识对后面怎么去设计和优化ISA，我觉得是很有帮助的。
【未来展望】
一、AI辅助证明：大模型的机遇与陷阱
Q9：
最后是两个比较“发展性”的问题。最近半年到一年，知名数学家陶哲轩用大语言模型辅助证明数学定理的事情屡屡刷爆了热搜，您认为这个大模型在形式化证明这一领域将来会占据一席之地吗？
邓玉欣：
会的，这方面已经有一些研究了。传统形式化证明还是一个比较困难的过程，大语言模型在这个过程中可以给一些证明步骤建议，辅助人类完成证明。
人能想到的东西肯定是和以前积累的知识相关的，但人看的东西肯定是很有限的，而大语言模型已经学了很多的知识，所以大模型建议的东西可能有时候比我们自己的思维开阔很多，有些可能的确是有帮助性的。
不过，这个东西也不能全信，还是需要人去验证的。我曾经尝试让大语言模型去证明一个定理，它给出的证明貌似是正确的，但是等到我一步步去验证的时候，发现其中从一步跳到另外一步的过程实际上是过不去的，这个证明实际上是一个伪证。
二、寄语学子：厚积薄发，静待花开
Q10：
最后一个问题。以一位前辈的角度说，您有没有什么想送给科大学子们，尤其是将来想要投身计算机基础研究领域的华夏计算机英才班的同学们的话呢？
邓玉欣：
我建议本科阶段还是要打好基础，我觉得这个其实很重要。将来找到合适的方向，然后再去钻研，我觉得这个是比较好的一个做法。本科阶段都去找合适的方向然后做科研，可能不一定适合所有人。
希望大家本科阶段先把基础打得更扎实一点。有时候，你学的东西可能不光只是专业要用到的或者课程培养方案里有的东西，有些跟你兴趣相关的东西同样可以考虑一下。
我举个例子，我最近在和我的学生在做一个量子化学模拟的项目，概括一下就是用量子计算的手段去模拟计算分子的基态能量，比方说计算一个苯环的能量。这就需要你知道有机化学里面的分子轨道模型，这一部分内容就是化学专业的。一个计算机出身的人大概率是不会学那么深的东西，所以我的意思是，如果你真的感兴趣，完全可以去看看这方面的东西。
对比较年轻的学生，我很喜欢和他们这样说：“不一定现在非要急着出多少成果。现在打好基础，对将来做研究，从长期来讲是更有竞争力的。”