Feb, 2024

基于加权模型集成的人工智能系统概率验证的统一框架

PDF
TL;DR用加权模型整合（WMI）为基础，提出了一个统一的 AI 系统的概率形式验证（PFV）框架，它可以处理各种机器学习模型的不同性质验证，如公平性、鲁棒性或单调性，避免了强分布假设，并讨论了与该框架相关的可扩展性挑战和研究方向。
probabilistic formal verificationai systemsweighted model integrationfairnessscalability challenges
发现论文，激发创造
  • 结构感知的 SMT 加权模型集成增强

    本文介绍一种基于 SMT 枚举的新算法，通过对问题结构的有效编码避免生成冗余模型，从而实现与不同整合技术的无缝配合，可以显著扩展可以通过 WMI 技术处理的问题集，而且相比现有的解决方案具有巨大的计算优势，已在合成和真实世界数据集上进行了广泛的实验评估，并在旨在验证概率程序公平性的原型任务中展示了该技术的应用潜力。

    Feb, 2023

  • 基于 SMT 的结构感知加权模型集成

    本文介绍了一种基于 SMT-based enumeration 的算法，对于复杂的混合问题具有显著的计算节约优势，经过实验评估证明该算法优于现有替代方法。

    Jun, 2022

  • 通过利用知识编译在线性和非线性混合领域中扩大概率推断

    本文提出了新的实现方案，利用命题知识编译来扩展推理，使用可处理布尔函数的可决策图作为基础模型计数和列举方案，在非线性势函数上处理非线性约束，并与最先进的 WMI 系统竞争。

    Nov, 2018

  • 深度概率模型的验证

    该文章提出了一种验证深度概率模型的新框架，在模型输出过程中采样潜在变量并考虑其所需的条件输入，以高概率满足线性约束，并能够有效地验证功能空间中感兴趣的属性（单调性、凸性）

    Dec, 2018

  • 分段线性神经网络验证的统一视角

    本文介绍了一种统一的深度学习模型形式验证的框架，利用分段线性结构和形式方法，结合现有方法的优势以实现两个数量级的加速。并提出了一组新的基准数据集，通过实验比较现有算法并确定影响验证问题难度的因素。

    Nov, 2017

  • math-PVS：一种大型语言模型框架，用于将科学论文映射到 PVS 理论

    人工智能在数学领域发现引起了广泛关注，这项研究探索了大型语言模型与定理证明系统的结合，旨在提供一种从研究论文中提取和形式化数学定理的自动化工具。

    Oct, 2023

  • 分段线性前馈神经网络的形式化验证

    本文提出了一种针对具备分段线性激活函数的前向神经网络进行验证的方法，并使用全局线性逼近对 SMT 求解器和 ILP 求解器进行推理，通过专门设计的验证算法利用推理出的相位信息对网络进行冲突检测和安全节点约束，并在碰撞避免和手写数字识别案例研究中进行了评价。

    May, 2017

  • 概率定理证明

    该论文提出了一种将概率论和第一阶逻辑相结合的方法，在有限域内具有 Herbrand 解释的情况下，定义了概率证明定理及其推广问题，然后提出了能够同时拥有图模型推理和一阶定理证明的完整能力的方法，并开发了一种高效算法。实验表明，当逻辑结构存在时，该算法远优于目前已有的方法。

    Feb, 2012

  • 用 GPU 加速的机器学习模型验证在电力系统中的应用

    本文介绍了用于检验大规模机器学习模型的计算工具，重点解决了其应用到电力系统问题时出现的困难；作者提出了一种方法可同时验证多个验证问题，并使用双重化程序将线性等式和不等式约束编码到检验问题中。

    Jun, 2023

  • 验证程序化弱监督的 Fréchet 界限估算

    我们开发了估算（可能是高维的）分布类的 Frechet 界的方法，其中一些变量是连续值。我们在边际约束的不确定性下建立了计算界限的统计正确性，并通过评估训练有程序化弱监督的机器学习模型（PWS）的性能来展示我们算法的有用性。

    Dec, 2023