理论计算机科学专题前言

理论计算机科学是整个计算机科学的理论根基。自从Alonzo Church和Alan Turing分别使用形式语言与自动机来为人类的计算行为进行理论建模开始,理论计算机科学领域的学者们就将计算本身作为一种客观存在,以“格物,致知”的态度来探究计算的本质原理。现代计算机科学与技术及其相应工程与应用的蓬勃发展,为这一基础学科提供了创新的舞台,使其充满了活力。

微内核操作系统互斥量模块功能正确性的形式化验证

操作系统在许多安全攸关领域为软件系统提供关键性底层支撑,操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障,造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生,对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误,因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中,互斥量可协调多任务对资源的访问,是一种常用的任务同步方式,其功能正确性对于保障多任务应用的正确性十分关键.基于定理证明方法,在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模,给出其接口函数的形式化规范,并实现这些接口函数的功能正确性验证.

在线影响力最大化研究综述

影响力最大化是指在给定的影响力传播模型下选取种子节点使其传播信息范围最广。此问题的应用场景十分广泛,包括推荐系统、病毒营销、信息扩散和链接预测等。在实际应用中,信息传播模型中的点对点传播概率通常是未知的,而在线学习算法可以在交互过程中自主学习未知参数,逐步逼近最优解。文中首先讨论了影响力最大化问题的定义,介绍了常用的影响力传播模型,归纳了常见的离线影响力最大化算法;随后介绍了经典的在线学习框架——多臂老虎机问题,分析了在线影响力最大化问题的研究现状,并通过实验对常见的在线影响力最大化算法在真实社交网络中的性能表现进行对比;最后总结了该课题面临的挑战并展望了未来的研究方向。

铁磁性双态自旋系统配分函数的可近似性

双态自旋系统是统计物理学在处理互作用粒子系统时所建立的简化模型,计算该系统的配分函数(partition function)在统计物理及计算机科学中均有重要意义。对于一般的系统,配分函数的精确计算已被证明是#P难的,但其是否能被高效地近似计算一直是理论计算机科学关注的问题。近年来,这一领域取得了较大的突破。研究者建立了配分函数的可近似性与该物理系统相变的联系,并且在很大的参数范围内理解了可近似性。文中对铁磁性双态自旋系统配分函数的可近似性研究进行了综述,介绍了目前针对该问题设计近似算法的三类技巧的主要思想,并把这些算法的结果与该问题在不可近似方面的结果进行了比较。

基于神经网络模型预测宫颈癌淋巴结转移

目的探索基于多参数MRI的放射组学特征和神经网络模型在区分宫颈癌淋巴结转移的效能。材料与方法回顾性分析178例宫颈癌并提取9个临床及病理特征,经过方差分析进而提取3个特征进入模型。两位观察者分别用软件勾勒得到感兴趣容积,提取到428个放射组学特征。放射组学特征结合临床及病理特征建模:分别组成428维、437维、431维模型。通过Python库的torch和sklearn构建并评价神经网络模型和支持向量机模型。组内相关系数(intraclass correlation coefficient,ICC)来评估观察者之间的信度,使用分类准确率、敏感度、特异度和受试者特征曲线下面积(area under the receiver operating characteristics curve,AUC)用来衡量检测模型性能。使用sklearn中的metrics.roc_curve函数绘制ROC曲线,通过最大约登指数(Youden index)确定最佳界值,并进行诊断效能评估。结果两位观察者ICC为0.819、观察者内ICC为0.796。431维神经网络模型AUC为0.882,在测试集中该模型的分类准确率、敏感度和特异度分别为0.810、0.840和0.741,优于其他模型。结论基于多参数MRI的神经网络模型可有效地预测宫颈癌淋巴结转移。

基于优化反馈的组合在线学习

组合在线学习问题研究如何在与环境的交互过程中学习未知参数,逐步找到最优的目标组合。该问题有丰富的应用场景,如广告投放、搜索和推荐等。首先阐述了组合在线学习问题的定义及其框架——组合多臂老虎机问题,归纳了此框架下的经典算法和研究进展;然后具体介绍了该问题的两个实际应用——在线影响力最大化和在线排序学习问题,以及其研究进展;最后展望了组合在线学习问题的未来研究方向。