64 篇论文
本文研究了概率测度余密度单子（codensity monads）的交换性与 Kleisli 定律，通过推导其到 Giry 单子的 Kleisli 定律建立了与可测概率的正式联系，给出了若干概率单子作为 Giry 单子终端提升的新普适性质，并提供了单子为仿射和松弛幺半的充分条件，特别是通过日卷积（Day convolution）刻画了 Radon 单子等恰好点式幺半的余密度单子，同时揭示了 Giry 单子仅在标准博雷尔空间上才具有该性质的原因。
本文通过引入依赖型有向接线图算子，构建了能够处理输出直接依赖输入（如 Mealy 机和参数化辅助变量的库存流图）的瞬时系统组合代数，并给出了其到 Mealy 机的语义解释。
本文提出了名为 Preguss 的模块化细粒度框架，通过结合静态分析与大语言模型，利用潜在运行时错误引导验证单元构建与优先级排序，成功实现了对千行代码级大规模程序的高度自动化形式化验证，显著降低了人工验证成本。
本文提出了一种基于无量化位向量逻辑的符号化量子比特抽象方法，成功实现了对包含多达 1,024 个相位量子比特的量子相位估计电路的高效形式化验证，且内存占用低于 3.5 GB。
该论文明确给出了在任意固定有限完备基下，真值表单点扰动导致电路规模变化不超过 的构造性上界，并通过 telescoping 论证将其推广至一般汉明距离，同时利用 SAT 求解器在 时对 AIG 基的穷举验证确认了该上界的紧性。
本文提出了 RoadLogic 这一开源工具，它通过结合答案集编程、运动规划及规范监控技术，成功将声明式的 OpenSCENARIO 规范自动转化为符合约束且多样化的可执行自动驾驶仿真场景，从而填补了现有方案在系统化实例化方面的空白。
该论文提出了一种将 d-DNNF 知识编译技术扩展至 SMT 层面的通用框架，通过结合预计算理论引理将 SMT 查询转化为命题逻辑问题，从而利用现有的 d-DNNF 编译器实现多项式时间的 SMT 查询。
本文提出了 BemaGANv2，一种通过引入 AMP 生成模块和 MED 判别器，并系统评估多种判别器组合策略，以实现高保真、长时程音频生成（如文本转音乐/音频）的先进 GAN 语音合成器。
本文提出了名为 FATE 的新基准系列（包含 FATE-H 和 FATE-X），旨在填补大型语言模型在竞赛数学与研究级抽象代数形式化证明之间的能力鸿沟，评估结果显示当前最先进模型在该领域表现极差，且其将自然语言推理转化为形式化证明的能力远弱于推理本身。
本文在齐次类型理论中形式化了覆盖空间与基本群子群之间的伽罗瓦对应，发展了覆盖空间的 n 维推广，并以此分类了透镜空间的覆盖及构造了庞加莱同调球。
本文提出了一种结合语法引导合成（SyGuS）与扩展了谓词和函数更新的时序流逻辑（TSL）的新方法，通过从执行轨迹中挖掘数据转换与时序规范，实现了比被动学习基线更鲁棒且样本效率更高的反应式程序合成。
本文比较了固定有限维希尔伯特空间上量子逻辑的三种可满足性语义，证明了标准语义蕴含局部偏布尔语义，后者又蕴含全局对易投影语义，并构造了一个显式公式作为标准语义可满足但后两者不可满足的分离实例，从而严格区分了这三种语义的可满足性类。
该论文提出了一种名为"Agent Hunt"的基于赏金机制的协作式自动形式化框架，通过让多个大语言模型代理在交互式定理证明环境中动态发布、竞标并完成代数拓扑领域的证明任务，从而探索去中心化的协作证明搜索与理论构建方法。
本文介绍了名为 Twitch 的工具，该工具利用 Stitch 自动从部分失败证明或相关定理的成功证明中发现等式定理证明中有用的抽象模式，并通过扩展 Twee 求解器，在 TPTP 单位等式问题上实现了 12 个难度为 1 的问题证明及显著的速度提升。
该论文展示了一个大语言模型编码代理在零人工代码参与下，成功构建了一个具备预处理、同余闭包算法及反例证明生成能力的完整 DPLL(T) 风格 SMT 求解器，且其在 SMT-LIB 基准测试中表现具有竞争力。
本文提出了名为 Elenchus 的对话系统，该系统基于推论主义语义，通过人类专家与大型语言模型之间的“证明者 - 质疑者”对话来构建知识基，并将对话状态映射到 Hlobil 和 Brandom 的非单调多后继逻辑（NMMS）中，从而在 W3C PROV-O 本体等案例中实现了从对话协商到形式化推理的端到端集成。
该论文提出了一种利用图神经网络预测 SAT 求解器初始分支顺序的预处理方法，在随机 3-CNF 和伪工业基准测试中显著提升了求解速度并展现出良好的泛化能力，但在更复杂的工业实例上因求解器动态启发式策略的覆盖及实例复杂性而效果有限。
该论文提出了基于有限极限草图的“草图导向数据库”范畴框架，将图数据库范式统一建模为集合值模型，并通过局部化器实现路径的惰性计算，同时引入“停顿草图”以支持模块化组合与可扩展模型增长。
本文提出了一种针对离散数学中一阶语言证明题的自动化生成方法，通过基于无逻辑符号的割基表证明来形式化捕捉解题难度，从而能够生成具有可比证明复杂度的新练习题。
本文介绍了 2025 年 6 月 6 日至 2 日在佛罗里达大学举办的第八届应用范畴论国际会议（ACT2025）的概况，包括其会议形式、涵盖的跨学科主题（如计算机科学、量子计算等）以及收录的会议论文集内容。