定理证明作为逻辑与计算机科学的交汇点,不仅奠定了现代数学推理的形式化基础,也是衡量人工智能逻辑推理能力的试金石,更支撑着软件工程对高可靠性的根本需求。然而,传统定理证明依赖严谨的逻辑推理与繁琐的人机交互,长期面临自动化程度有限、推理效率不足以及对专家经验高度依赖等难题。随着大语言模型(LLM)的快速发展,其在自然语言理解、代码生成和逻辑推理等方面展现出突破性能力,为提升自动定理证明的自动化与智能化水平提供了新的契机。为此,系统梳理了大模型驱动的形式化定理证明的研究现状与趋势,重点聚焦于两个主要应用场景。1)在交互式定理证明方面,分析了现有工作是如何缓解其手动开销巨大的难题,并以Lean语言中的Prover系列工作为例,系统总结了其技术演化路径。2)在自动定理证明方面,探讨了大模型如何结合静态分析、验证器反馈等技术,自动生成函数合约、循环不变式等形式化规约,从而显著降低验证门槛。最后,归纳了该领域中面临的共性挑战,包括规约完备性、推理可靠性、数据稀缺性以及工具链集成等,并展望了未来的发展方向。

聚类是机器学习中的经典任务,旨在根据相似度度量将数据划分为若干簇。k-均值聚类作为最基本的聚类模型,自提出以来已被深入研究并在众多领域得到广泛应用。聚焦k-均值模型的求解问题,从理论计算机科学的视角出发,介绍k-均值的(接近)线性时间的快速近似算法的研究进展。此外,简要讨论其他相关大数据计算模型中的聚类算法的相关进展,包括动态、数据流与并行计算等计算模型。

深度神经网络在具备强大的表达能力的同时展现出优异的泛化性能,这与统计学习理论中“模型复杂度损害泛化”的经典论断存在本质冲突,导致传统框架下的深度泛化机制分析陷入困境。经典一致收敛界理论具有依赖参数空间维度、忽略算法隐式偏置等局限,难以直接适配深度网络核心特性。针对这一理论裂隙,构建了融合深度模型关键特征的新型统计学习理论框架,重构了一致收敛理论对深度模型泛化机制的解释范式。通过构建保留深度网络过参数化结构与高维噪声扰动特征的代理线性模型,首次推导出有效的一致收敛界,揭示了高维特征空间中噪声扰动对泛化性能的良性作用机制,突破了传统低维学习理论框架的局限性;基于深度泛化机制构造了数据规模敏感的规范化训练过程,揭示一致收敛界与泛化误差随样本复杂度增长呈现同步衰减的规律,证实了一致收敛理论对深度模型泛化机制的解释能力。基于理论与实验双重证据,突破了一致收敛泛化界的适配瓶颈,重新打开了一致收敛理论分析深度模型泛化性这扇即将被关闭的大门。

预训练语言模型在 Metamath 等形式化环境中,在证明定理方面展现出显著潜力。然而,这种潜力尚难以稳定转化为可靠的推理能力。现有方法通常要求语言模型直接预测替换项,而这些替换项来自一个开放且潜在无限的表达式空间,缺乏逻辑约束,导致模型泛化能力受限。为此,提出一种新的证明范式:在推理过程中引入工作变量以临时替代具体项,并通过合一算法推导出其具体实例。该设计使得模型能够聚焦于定理选择,而无需生成缺乏逻辑指导的替换。基于这一范式,从 Metamath 数学库中提取数据并构建 UnProver(Unification-Driven Prover),并在此数据上对其进行训练。此外,设计多种数据增强策略,进一步提升 UnProver 的性能。实验结果表明,UnProver 在测试集上整体优于包括 GPT-4o 在内的基线方法,在证明能力与效率方面均取得更优表现。此外,UnProver 还发现了 6 个新的、更简洁的证明,这些证明已被正式收录至 Metamath 官方数学库。

在高维小样本分类任务中,宽度学习系统(Broad Learning System,BLS)因其高效的特性而备受关注。然而,原始的单层BLS的特征提取能力有限,难以处理复杂的高维数据。随机节点生成机制导致直接堆叠BLS隐层时出现节点冗余,模型性能难以提升。为解决上述问题,提出了一种集成堆叠BLS算法。所提算法利用前一层BLS的输出作为增强特征,将其与按分类置信度加权的原始特征进行拼接后输入下一层BLS,不断提高深层特征表达能力。通过元学习器池集成多个BLS层的输出,增强了原始单层BLS的高维特征提取能力,从而提升了模型的泛化性能。此外,考虑到高维数据复杂多变的特性,设计了动态集成框架,根据数据难度动态调整模型的复杂度。所提方法在保持模型性能的同时,进一步提升了集成效率。消融实验证明了所提算法的各个模块的有效性,对比实验证明了所提算法在高维疾病数据上的优越分类性能。

作为Bent函数的重要推广,Plateaued 函数继承了很多Bent函数的优良密码学性质,具有重要的应用价值。由于传统构造Plateaued 函数的方法存在计算复杂度高、灵活性不足等问题,因此提出一种基于深度 Q 网络(Deep Q-Network,DQN)增强的自适应遗传算法。该算法深度融合 DQN 与遗传算法,构建多维状态空间感知种群进化特征,通过群体共识机制智能选择6种交叉与变异策略组合,实现遗传参数的自适应调控。实验结果表明,该算法的适应度提升幅度达 0.20~0.35,收敛速度更快,稳定性更高,平均可生成 230~300 个有效 Plateaued 函数真值序列,显著优于标准遗传算法和基础 Q-learning 遗传算法。算法能智能调节变异率(0.235~0.276)与交叉操作使用率(70%~90%),在优化 Walsh 谱分布的同时保持种群多样性。尽管计算开销略有增加,但所提算法在解的质量、收敛性能和策略自适应能力上具有显著优势,验证了深度强化学习在密码学函数构造中的有效性,为布尔函数智能化设计提供了新方案。

深度学习模型由于其“黑盒”特性,特征表示缺乏可解释性。现有的解耦表征学习方法虽然在一定程度上能够通过识别数据中的独立因素来增强模型的解释能力,但它们通常忽视了数据中的复杂关联性及潜在因果结构,从而限制了模型在自动驾驶、医疗诊断等关键领域的应用,特别是在需要理解和干预因果关系的场景中表现不佳。针对当前解耦表征学习中因果关系建模不足的问题,提出了一种融合稀疏编码与因果推断的解耦表征学习框架。该框架在适当监督下通过因果推断机制精准建模数据中的因果关系,不仅能够生成高质量结构化表征,更具备对潜在因果机制的建模与干预能力,进而显著提升模型在因果任务中的适应性与鲁棒性;同时通过嵌入的卷积稀疏编码层施加稀疏性约束,有效筛选与因果结构高度相关的关键表征,进一步强化模型对高阶因果关系的敏感度与表达能力。实验结果表明,该框架在Pendulum和CelebA数据集上表现出色。样本效率在Pendulum数据集上达98.65%,在CelebA数据集上达99.55%,此外,在因果干预有效性和分布鲁棒性方面优于现有方法,证实了该方法在复杂因果场景下的优越性。

随着复杂障碍物环境下移动机器人的全覆盖路径规划在生产巡检、家庭卫生等领域的应用越来越广泛,现有方法存在的重复覆盖率高、子区域间转换路径复杂以及对凹多边形障碍物适应性不足等问题愈发凸显。因此,提出一种融合Maklink图论、改进蚁群算法和Boustrophedon路径的移动机器人全覆盖路径规划方法。该方法首先利用Maklink图论构建环境模型,生成链接线,利用链接线将二维空间划分为多个凸多边形子区域并构建初步可行路径网络;其次,将子区域访问顺序建模为广义的TSP问题,利用一维蚁群算法获取子区域间的访问序列;然后,结合求最小函数值的蚁群算法与三角剪枝几何优化,得到子区域间最优转换路径;最后,按照访问顺序在各子区域内采用Boustrophedon路径进行“弓”字形路径遍历,形成全局覆盖路径。在多个不同二维复杂度环境中的仿真实验表明,所提方法可有效适应存在多种多边形障碍物的环境,覆盖率均可达100%,重复率为0。与传统蚁群算法和改进蚁群算法两种单一算法的对比实验表明,该算法在转换路径长度、遍历路径长度及重复率三方面均具有较好的表现;与传统利用栅格法构建环境模型的全遍历方法的对比结果表明,该算法建模精度高,存储效率优。

研究仓储路径规划对智能仓储具有重要意义,合理的路径规划能够有效避免仓储路径冲突,提升仓库内货物运输效率。针对当前仓储布局较为简单、缺乏针对复杂仓储布局的路径冲突策略问题,提出基于AGV坐标保留表和冲突分类的多目标AGV路径规划算法。首先,构建基于网格法的智能仓储鱼骨布局方案,并根据分区机制,给出存储节点间的距离计算模型,构成单一单向的仓储路径网络有向图。其次,建立AGV坐标保留表方法和路径冲突分类方法,制定路径冲突解决策略和算法。然后,建立以最小化总运输距离、最小化最大运输距离、最小化冲突解决等待时间为目标的多目标智能仓储路径规划模型。最后,结合所提路径冲突解决算法,设计基于进化遗传搜索算法的突变操作,在基于学习的多目标组合优化求解算法P-MOCO的基础上,通过构建偏好条件随机策略,借助多目标降维和强化学习方法,提出改进P-MOCO的无冲突多目标智能仓储路径优化算法CF-MOWVRP,求解无冲突的多目标规划模型的近似帕累托解。实验结果表明,所提算法具备更快的收敛速度和更优的解,能够解决路径冲突,给出无冲突的路径规划方案。

基因调控网络(Gene Regulatory Network,GRN)推断对于解析细胞发育机制及推动精准医学研究至关重要,但是现有深度学习方法面临计算复杂度高与全局特征捕捉不足的挑战。为此,提出一种融合Kolmogorov-Arnold 网络(KAN)驱动的图卷积网络(KGCN)与 Mamba 模块的高效预测模型。首先,以 KAN特有的可学习样条函数,取代图卷积网络中的多层感知器(MLP)模块。该改进在完整保留邻居节点局部特征提取能力的基础上,通过重构计算逻辑降低特征处理的冗余度,使模型计算复杂度较传统图卷积架构实现显著优化。其次,创新性地引入 Mamba 模块,通过其选择性机制优先关注对全局调控起关键作用的基因节点。两者结合实现了局部特征提取效率与全局依赖建模能力的协同优化。在公开数据集上与另外6种深度学习模型进行实验比较,结果显示,该模型在AUC和AUPR性能指标上都优于其他模型,同时展现出显著的鲁棒性优势和计算效率。

在噪声中等规模量子(Noisy Intermediate-Scale Quantum,NISQ)时代,考虑硬件耦合约束限制,并非所有量子门均可直接执行,通常需要利用额外引入的SWAP操作实现量子比特交换后,逻辑线路才能直接运行于物理硬件上。为了避免传统量子线路映射过程中SWAP操作带来的额外开销,对量子比特频度进行定义,提出一种高频-密集量子门集策略(High Frequency-Dense Quantum Gate Set Strategy,HF-DQGS),并将其应用于量子线路映射。基于量子比特频度,对CNOT门进行优先级划分,定义高频-密集量子门集;利用多变量成本函数对候选SWAP门的实际开销进行评估,确定待执行的SWAP操作;根据基于量子比特频度的最优SWAP门评价准则,SWAP操作后对评价函数进行比较,筛选出最优的SWAP门。实验结果表明,HF-DQGS能够显著减少附加SWAP门的数量,并在一定程度上减少CNOT门的数量。具体而言,在t|ket〉和Qiskit 编译器上的测试结果显示,额外SWAP门的数量平均分别减少了36.6%和47.8%,CNOT门的数量平均分别减少了13%和13.4%。