使用类型自然推理系统检查概率计算的可信度
通过整合大型语言模型,Trusta 建立和验证可信度推导树 (TDTs) 进而提升保证案例的构建和评估,实现在安全工程中自动推理的新方法。
Sep, 2023
本文介绍了一种结合了 Evidential Deep Learning、Neural Processes 和 Neural Turing Machines 的概率分类器应用,本分类器能够对目标域数据进行成功拟合并在目标域的困难区域(例如类重叠)提供经过校准的分类概率。同时,在所有五个分类任务中,我们的方法都是唯一能够在单个独立的预测器中胜任三个方面的全面校准的。此方法为深度神经网络中认知感知的研究提供了实现友好的计算有效解决方案,为算法根源的调查提供了智力经济性。
Jun, 2021
本文提出了一种名为 Conditional Theorem Provers(CTPs)的方法,它是 Neural Theorem Provers(NTPs)的扩展,可以通过基于梯度的优化学习出最优规则选择策略以实现可解释性和可扩展性,并且在大规模任务中表现优异。CTPs 在 CLUTRR 数据集上取得了表现最优结果,并在标准基准测试中展现了比其他神经符号模型更好的链接预测结果。
Jul, 2020
本文提出了一种解决人工智能中自然语言和知识库的推理问题的方法,即利用神经定理证明器和共享嵌入空间来实现,该方法被证明的可扩展性更加高效,并取得了较好的预测结果和可解释性。
Dec, 2019
概率编程是一种允许编写统计模型、通过运行这些模型进行模拟,并利用强大的推理引擎分析和改进它们的统计行为的编程范式。本文介绍了将数据 Petri 网(DPNs)系统地转化为使用大多数概率编程系统支持的概率编程语言模型的方法。我们证明了我们的转化方法是可靠的,并可以提供模拟 DPNs 的统计保证。此外,我们讨论了概率编程在过程挖掘任务中的应用,并报告了我们的转化方法的原型实现。我们还讨论了基于所提出的转化方法和现有的概率编程工具可以轻松实现的进一步分析场景。
Jun, 2024
本文介绍了 TADS (紧凑型白盒神经网络表示) 在神经网络验证中的应用,结合 PCA 降维技术,提出了 Precondition Projection 技术用于描述神经网络的行为,可以用于诊断网络错误并提供紧凑和明确的解释,以及用于网络调试和生成新的训练样本。
Apr, 2023
我们引入了一个正式的元语言来进行概率编程,旨在让 AGI 不仅学习相关知识(程序 / 证明),而且学习适当的推理方式(逻辑 / 类型系统)。我们利用立方型类型理论和依赖类型元图的框架来形式化我们的方法。通过这样做,我们展示了元语言中的特定构造可以通过双模拟(意味着路径等效)与它们相应的类型系统相关联,从而为各种类型系统推导出综合指称语义。特别是,我们推导出了纯类型系统(PTS)和概率依赖类型系统(PDTS)的双模拟。我们进一步讨论了 PTS 与非良基础集合论的关系,并在立方保护类型理论类型检查器中实现了双模拟证明的可行性.
Mar, 2022
本文通过在 terms 上创建一个 measure space,定义级别逐步逼近的连续 lambda-Calculus 的典型操作语义,并定义采样基异质的语义来实现 MCMC 的 Tracing,并证明了分布语义与集成所有 Traces 的分布具有等价性,这是第一个针对高阶函数语言 Trace MCMC 的验证正确性的证明。
Dec, 2015
本文介绍概率演绎作为一种概率结构化论证的方法,提出了概率规则(p 规则)的概念,它们构成了概率演绎系统,并且也表示了定义联合概率分布的条件概率。作者介绍了概率演绎的闭世界假设,证明了在此假设下该方法与经典论证方法的完全扩展与最大熵推理方法相一致,并提出了几种计算联合概率分布的方法以达到实用的证明理论。
Sep, 2022