• 针对行人图像数据的差分隐私与k-匿名性：其对跨相机人员重新识别及人口统计预测的影响

  视频摄像头在大城市中非常普遍，但它们在公共安全之外的使用仍受到合法隐私问题的限制。然而，这些摄像头能够捕捉到的信息极其丰富，这使得它们在大规模智慧城市应用中展现出巨大的潜力，因为它们可以作为非常强大且多功能的传感器。这种矛盾引发了这样一个问题：是否可以以负责任的方式使用此类图像数据？基于加密的解决方案假设端服务器可以安全地保存数据，但数据泄露表明这种假设并不总是成立。传统的图像模糊或像素化方法在保留数据实用性和隐私保护方面效果有限。因此，需要一种能够直接在数据本身上提供隐私保护同时保持实际可用性的隐私方法。本文扩展了两种这样的概念，即差分隐私和k-匿名性，并在跨摄像头的人再识别和属性识别数据上

  来源：ACM Transactions on Cyber-Physical Systems

  时间：2025-11-07

• 颜色容错扳手

  在现代网络和系统设计中，容错性是一个至关重要的概念。随着系统复杂性的增加，组件出现故障的概率也随之上升，因此构建能够在某些组件失效后仍能维持关键功能的结构成为研究的热点。在这一背景下，容错跨度图（Fault-Tolerant Spanner）作为一种高效的数据结构，被广泛应用于网络路由、同步、距离估计等多个领域。传统的容错跨度图主要考虑的是单个顶点或边的失效，但随着多层网络和共享资源组的出现，单一的失效模型已无法满足实际需求。本文引入了一种新的容错模型，即颜色容错跨度图（Color Fault-Tolerant Spanner，简称CFT），并探讨了其在不同场景下的性能和构造方法。### 一、

  来源：ACM Transactions on Algorithms

  时间：2025-11-07

• 通过无线网络进行从仿真到实际的迁移以实现估算

  随着无线网络技术的不断发展，越来越多的智能系统开始依赖无线网络进行数据传输和决策。这些系统，例如车联网（V2X）和公共交通应用，通常需要在共享的无线网络上接收来自多个节点的测量数据，以估计环境状态。然而，无线网络环境复杂多变，包括网络拥塞、数据包丢失和延迟等，这些因素会显著影响系统的性能。因此，构建一个能够适应不同网络环境的数据驱动模型成为一项重要的挑战。本文提出了一种将模拟环境中的数据驱动模型转移到现实世界的方法，旨在解决这一问题。在现实世界中，获取广泛覆盖不同网络条件的训练数据既困难又昂贵。此外，真实的网络状态往往难以获得，这使得基于真实数据的模型训练变得不可行。为了克服这些限制，我们设计

  来源：ACM Transactions on Cyber-Physical Systems

  时间：2025-11-07

• 在随机到达或联盟解散情况下的在线联盟形成

  在多智能体系统中，联盟形成是一个富有活力的研究领域。其核心目标是根据智能体之间的偏好，将一组智能体划分为互不重叠的联盟。我们考虑了一个具有基数效用模型的联盟形成问题，其中偏好通过可加分离的方式进行聚合，并研究了在线版本的联盟形成问题。在在线模型中，智能体按顺序到达，必须立即且不可撤销地分配到现有联盟或新建的单人联盟。在这一基本模型中，已知贪心算法可以达到最优的竞争力比，但该比值严重依赖于效用的范围。在本研究中，我们通过考虑两个相关的模型，对这一结果进行了补充。首先，我们研究了随机到达模型，其中敌手的权力被削弱。虽然敌手仍可以固定有害的效用，但智能体的到达顺序是均匀随机的。我们发现，在随机到达模

  来源：ACM Transactions on Algorithms

  时间：2025-11-07

• 平面最长树问题：近似算法与计算复杂性突破

  平面最长生成树问题是计算几何领域的经典NP难问题，其核心目标是在给定平面点集中寻找边长度之和最大的非交叉生成树。近年来，该问题在近似算法设计和计算复杂性分析方面取得了一系列突破性进展。近似算法设计突破研究团队提出了一个创新的多项式时间近似算法，能够以常数因子逼近最优解。该算法基于两个关键观察：首先，最优解往往具有特殊的结构特性；其次，通过精心设计的星型结构和直径约束树可以获得良好的近似效果。算法具体构造两种类型的树：星型树（star trees）和基于最近邻划分的特定树结构。对于任意点集，算法通过比较O(n2)棵候选树的长度，选择其中最长的作为输出。理论分析证明该算法能够达到0.5的近似比，这

  来源：ACM Transactions on Algorithms

  时间：2025-11-07

• 双团自由最大k-权重SAT和最大覆盖问题的参数化近似方案

  引言与背景0和任何函数h，没有h(k)(n+m)^o(k)时间的算法可以将最大覆盖（CC-Max-SAT的单调版本）近似到因子(1-1/e+ε)，即使承诺存在k个集合能完全覆盖整个全集。事实上，即使输入公式是2-CNF，假设唯一游戏猜想（UGC），该问题也难以在0.929因子内近似。这些棘手的结果促使我们探索能够规避这些障碍的公式族。为此，我们考虑Kd,d自由的公式（即公式的子句-变量关联二分图排除Kd,d作为诱导子图）。主要结果概览我们的第一个结果针对Kd,d0，存在一个算法，对于Kd,d自由的公式，以(1-ε)的近似比运行，运行时间为2O((dk/ε)d)(n+m)O(1)（这些算法称为F

  来源：ACM Transactions on Algorithms

  时间：2025-11-07

• 探索对话式虚拟代理中的熟悉感和知识水平

  在虚拟现实（VR）环境中，虚拟代理的熟悉度和知识性对人类与虚拟代理的互动产生了深远的影响。这项研究通过创建两个虚拟代理——一个是熟悉代理（由本部门教授的数字复制品构成），另一个是不熟悉代理（具有相似的人口统计信息，但使用合成外观和声音），并赋予它们高或低的知识性，来探讨熟悉度和知识性如何影响用户对虚拟代理的感知、社交和情感体验以及对话动态。研究结果揭示了熟悉度和知识性之间复杂的相互作用，不仅影响用户对代理知识性的判断，还对信任、类人感、未知谷效应、喜欢程度等变量产生显著影响。### 虚拟代理的熟悉度和知识性对用户感知的影响研究发现，熟悉度对用户感知的知识性具有显著的主效应。参与者普遍认为熟悉代

  来源：ACM Transactions on Applied Perception

  时间：2025-11-07

• 一种多输出BERT框架，用于低资源语言中的恶意评论检测和情感分析

  摘要在现代数字世界中，社交媒体通过促进思想和观点的交流，已成为人际互动不可或缺的一部分。然而，在这种数字环境中也存在一些问题，尤其是粗鲁行为和冒犯性言论的问题。为同时解决这两个问题，本研究重点关注社交媒体互动中的情感分析和辱骂性评论检测。该数据集包含了2019年至2021年的仇恨言论与冒犯性内容识别（HASOC）数据，用于识别各种社交媒体平台上印地语的仇恨言论。为了将评论分为辱骂性和非辱骂性两类，研究人员使用了多种BERT模型，包括mBERT、DistilBERT、RoBERTa、HateBERT和IndicBERT。此外，还对这些贬损性评论进行了全面的情感分析。本研究提出了一种分层集成框架，

  来源：ACM Transactions on Asian and Low-Resource Language Information Processing

  时间：2025-11-07

• 阅读方向影响数据可视化感知：来自从右到左和从左到右用户研究的洞察

  摘要可视化对于研究和传达数据密集型信息至关重要。图表中的微小变化可能会导致截然不同的感知结果，而这在很大程度上取决于用户的先验认知属性。全球有数亿人使用从右到左（RTL）的书写方向，例如阿拉伯语和希伯来语，这类用户对图形信息的感知方式与从左到右（LTR）的读者有所不同。本研究旨在解决为RTL读者设计数据可视化内容的挑战，因为他们的阅读习惯可能导致对时间轴和方向性数据等视觉元素的误解。通过使用具有方向敏感性和无方向性特征的刺激物进行实验，我们分析了RTL读者与LTR读者在视觉解读上的差异。研究结果强调了阅读方向对感知的显著影响，从而凸显了开发支持多种阅读方向的适应性可视化技术的必要性。

  来源：ACM Transactions on Applied Perception

  时间：2025-11-07

• 音乐教育与注意力控制之间的关系：来自一项针对小学生的眼动追踪研究的证据

  摘要本研究采用纵向准实验方法，探讨音乐教育对儿童注意力控制能力发展的影响。通过眼动追踪实验中的抗扫视任务来评估视觉注意力的控制能力。共有50名小学生（6-7岁），其中25名来自音乐学校，他们在流体智力方面与非音乐学校的同龄人相匹配。这些学生分别在入学初期、12个月和24个月后各完成三次抗扫视任务，每次实验都记录了他们的眼球运动数据。随着时间的推移，两组儿童的注意力控制能力都有所提升。音乐学校的学生在抗扫视任务中的表现明显优于普通学校的学生。正如预测的那样，所有学生在整个学习过程中正确完成任务的反应速度逐渐加快，这表明他们的注意力控制能力得到了提升，尤其是音乐学校的学生提升更为显著。只有在音乐学

  来源：ACM Transactions on Applied Perception

  时间：2025-11-07

• 利用Neutrosophic Sets、MuRil和扩展的Hindi SentiWordNet从印地语新闻中检测政治偏见

  摘要媒体被誉为“民主的第四支柱”，对每个人的日常生活都产生着影响。印度在世界新闻自由指数（WPFI）中的排名下降，反映了新闻报道中的偏见，尤其是政治新闻报道。这些带有偏见的标题扭曲了人们对相关议题的看法，使他们充满了无根据的偏见。目前，印度有数千家印地语报纸出版商，其订阅者数量超过了1亿。从新闻中检测政治偏见是一个新兴的研究领域，研究人员尚未考虑过语境分析。这是首个采用中立主义（neutrosophic）理论进行语境词汇分析的政治新闻偏见检测模型，旨在解决信息不一致性和不确定性问题。该模型使用了新升级的印地语SentiWordNet和MuRil语言模型来处理编码输出并进行多类别分类。该模型将输

  来源：ACM Transactions on Asian and Low-Resource Language Information Processing

  时间：2025-11-07

• 基于节点差异隐私的连通分量数量估计

  本文探讨了一种全新的方法，用于在保证节点差分隐私的前提下，对图中的连通分量数量进行近似计算。节点差分隐私是一种严格的隐私保护机制，它确保当数据库仅在单个节点及其相关边的信息上发生微小变化时，输出结果对于外界观察者来说几乎不可区分。然而，设计满足这一隐私要求的算法对于连通分量这一图统计量来说极具挑战性，因为该统计量对添加一个具有任意连接的节点非常敏感，这使得节点差分隐私难以实现。本文提出了一个高效的解决方案，通过构建一个可计算的、基于森林多面体的Lipschitz扩展家族，实现了对连通分量数量的近似估计，并证明了其误差范围在特定条件下接近最优。### 图连通性与隐私保护的挑战图的连通性是理解网络

  来源：ACM Transactions on Algorithms

  时间：2025-11-07

• 模板提取：一种用于从遗留代码中提取模板内核摘要的分层递归提取系统

  摘要我们提出了Stencil-Lifting这一创新系统，该系统能够自动将用低级语言编写的模板内核转换为语义等价的领域特定语言（DSL）实现。针对现有验证提升系统的效率瓶颈，Stencil-Lifting通过两项关键创新实现了模板内核的可扩展抽象。首先，我们提出了一种分层递归提升理论，该理论使用不变子图来表示模板内核（这些模板内核被结构化为嵌套循环），不变子图是定制的数据依赖图，用于捕获循环携带的计算和结构不变量。不变子图中的每个顶点都关联有一个基于谓词的摘要，用于编码其计算语义。通过确保这些摘要之间的自一致性，Stencil-Lifting能够正确推导出嵌套循环的循环不变量和后置条件，从而无

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 检测并解释上下文无关文法的等价性（或不等价性）

  摘要我们提出了一个可扩展的框架，用于判断、证明以及解释上下文无关文法的等价性（或不等价性）。我们实现了该框架，并在教育支持系统中收集的大型数据集上对其进行了评估。尽管一般来说上下文无关语言的等价性问题是无法判定的，但该框架仍能够处理这些数据集中的大部分内容。该框架结合了多个领域的技术，包括一种用于识别等价文法以及相似但不等价文法的抽象文法转换语言、针对大量上下文无关语言的基于理论的比较算法，以及一种受图论启发的文法规范化方法，该方法能够高效地识别出同构文法。

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 用于效果处理器的动态风效果

  摘要效果处理器提供了一种抽象处理具有副作用的计算的便捷方式。此外，支持效果处理器的编程语言通常会静态跟踪这些副作用，从而确保用户能够了解程序不同部分可能产生的所有副作用。与异常处理器类似，效果处理器通过局部定义其行为来执行相应的操作。但与异常处理器的不同之处在于，效果处理器允许程序继续执行，可能是之后某个时刻，甚至可能多次执行。在本文中，我们提出了一种动态“wind”机制的变体，该机制能够很好地与词法效果处理器结合使用。即使在任意位置存在任意控制效果的情况下，该机制也能保持明确的语义。具体来说，捕获和恢复执行流程（无论是在程序的“前奏”部分还是“尾声”部分）的行为都是明确定义的，并且遵循资源管

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 可扩展等价性检查与浅层量子电路的验证

  摘要本文探讨了如何判断两个浅层（即恒定深度）量子电路是否执行等效的计算。等效性检验是一个基本的正确性问题——例如，它用于确保应用于量子电路的变换不会改变其行为。对于量子电路而言，这个问题具有挑战性，因为在一个经典计算机上直接表示每个电路的量子状态可能需要与量子比特数n成指数级的时间和空间。本文提出了“基于投影的等效性检验”（PBEC），它为等效性检验问题的两种变体提供了决策程序。这两种方法都可以在经典计算机上以与n成线性关系的时间和空间复杂度完成。我们的关键见解是，局部投影可以作为完全描述浅层量子电路输出状态的约束条件。输出状态是满足所有约束条件的唯一量子状态。除了等效性检验之外，我们还展示了

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 通过跨语言代码生成器和差异测试发现编译器错误

  摘要编译器在将高级代码转换为可执行程序的过程中起着核心作用，因此其正确性对于确保代码的安全性和可靠性至关重要。虽然已有大量研究致力于验证单一语言编译器的正确性，但跨语言编译的正确性（即涉及两种语言及其相应编译器之间的交互）仍很大程度上未被探索。为填补这一研究空白，我们提出了CrossLangFuzzer这一新型框架，它为基于JVM的语言引入了一种通用的中间表示（IR），并能够自动生成具有多种类型参数和复杂继承结构的跨语言测试程序。在生成初始中间表示后，CrossLangFuzzer应用了三种变异技术——LangShuffler、FunctionRemoval和TypeChanger——来增加程

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 深度神经网络的Mini-Batch鲁棒性验证

  摘要神经网络图像分类器在许多安全关键应用中无处不在。然而，它们容易受到对抗性攻击的影响。为了了解它们对攻击的鲁棒性，已经提出了许多局部鲁棒性验证方法来分析输入数据中的特定区域（称为“є-球”）。然而，现有的验证方法分析时间较长，或者精度损失过多，因此在处理大量输入数据时效果不佳。在这项工作中，我们提出了一种新的局部鲁棒性验证方法：分组局部鲁棒性验证。其核心思想是利用某些є-球在网络计算上的相似性来减少总体分析时间。我们提出了BaVerLy，这是一种可靠且完整的验证工具，它通过动态构建和验证小批量数据来提高对一组є-球的局部鲁棒性验证效率。BaVerLy能够自适应地确定合适的小批量大小，构建具有

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• 宽度无关的位向量谓词的认证决策程序

  摘要位向量是自动推理的基础。一些交互式定理证明器（ITP），如Lean，通过位爆破（bitblasting）技术，能够很好地处理固定宽度的位向量谓词。然而，即便是这些ITP，对于与宽度无关的位向量谓词也几乎没有提供自动化支持。为填补这一空白，我们在Lean中为与宽度无关的位向量谓词贡献了新的、机械化的决策程序。用于判断与宽度无关的位向量理论片段的经典算法可以从模型检查的角度来理解：在这种情况下，公式对应于一个自动机，而公式的正确性则是一种安全属性。然而，我们目前还无法将这些方法应用于机械化证明中，因为还没有可执行、快速且经过形式验证的模型检查算法能够直接在ITP内部使用。为了解决这个问题，我们

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

• LLVM AArch64后端的翻译验证

  摘要LLVM的后端将其中间表示（IR）转换为汇编代码或目标代码。除了寄存器分配和指令选择之外，这些后端还包含许多与编译器中间代码阶段相关的组件：数据流分析、公共子表达式消除、循环不变量代码移动以及一种称为“机器IR”（MIR）的一级中间表示。实际上，这种类型的编译器后端本身就是一个高度优化的编译器，它涉及数百万行复杂C++代码所带来的所有正确性风险。为了增强对LLVM后端工作正确性的信心，我们开发了arm-tv工具，该工具可以正式验证LLVM IR与AArch64（64位ARM）代码之间的转换。虽然这不是针对LLVM的首个转换验证项目，但我们在多个方面推动了技术的发展：arm-tv是一个能够强

  来源：Proceedings of the ACM on Programming Languages

  时间：2025-11-07

知名企业招聘：