- 证明奥林匹克代数不等式无需人类演示
提出了一种名为 AIPS 的代数不等式证明系统,它能够自动生成复杂的不等式定理,并有效地解决奥林匹克等级的不等式问题,而无需人工演示。在混合推理方式下,通过生成的数据集实施价值课程学习策略来提高推理性能,展示出强大的数学直觉。在测试集上,A - 学习引导的自动推理:简要调查
自动定理证明器和形式证明助手是理论上能够证明任意难题的一般推理系统,但在实践中面临组合爆炸所以包括很多启发式算法和选择点来影响系统性能。机器学习预测器可以引导这些推理系统的工作。本文概述了几个自动推理和定理证明领域及目前对它们进行的学习和人 - 抽象代数中的初等证明的自动规划技术
该研究探索了自动规划在自动定理证明中的应用,研究了利用规划构建抽象代数中的基础证明,证明自动规划技术在自动定理证明领域是可行的。
- 建立对自动推理的信任
自从上世纪 40 年代起,计算机的自动推理逐渐成为科学研究中越来越重要的工具。现阶段,通过机器学习技术从大量数据中推导出的规则成为了一种互补的方法,并在积极发展中。然而,我们对于为何应该相信这些系统以及通过其帮助获得的结果的问题,在科学哲学 - 基于 And-Or 递归器和细化神谕的目标驱动 LLM 对话线程全自动化
我们介绍了一种使用基于 Horn 子句解释器的经验性语言模型,自动执行深层次的、逐步的推理任务来细化对话线程来实现任务特定的对话。
- 高效人工智能方法用于(交互式)调试:不要只治疗症状,查找根本原因!
本论文介绍了基于模型的诊断,探讨了该领域的主要挑战,并讨论了一些应对这些问题的研究方法。
- BoardgameQA: 自然语言推理与矛盾信息处理数据集
该论文探讨了利用自然语言处理技术进行非结构化文本的自动推理。研究表明,语言模型具有复杂的推理能力。然而,当推理真实世界中不一致或矛盾的信息时,需要采用一种策略来解决这种冲突。采用对信息来源的偏好以及执行更高偏好的源的方式来解决冲突是一种普遍 - 自动推理中相关问题集的轻量级在线学习
自驱动策略学习是一种轻量级在线学习方法,适用于解决一组相关问题的自动化推理任务。它使用机器学习模型根据数据集调整后续问题的解决策略,从而实现更好的边界模型检查性能。
- 构建可逆的语义保留逻辑公式嵌入
该研究工作探讨了如何使用基于图变分自编码器 (Graph Variational Autoencoder) 的深度架构来训练学习逻辑嵌入,以实现对逻辑嵌入的反向推理,即将嵌入空间中的逻辑公式反向映射回语法空间,进而提高机器学习中学习逻辑规则 - 使用 Isabelle 证明助手进行考试
本文介绍一种使用 Isabelle 证明助手对自动推理课程学习成果进行测试的方法,该方法允许测试不同逻辑证明系统中形式证明的一般理解和特别是在 Isabelle/HOL 高阶逻辑中证明的理解,最终讨论了使用该方法考试并进行评分的经验和未来潜 - Peano: 学习形式化数学推理
本研究探讨在数学中的程序抽象结构,定案例研究并且说明通过 Peano 定理证明环境和可重用抽象的能力,加上恰当的教学大纲,是保障自动化数学推理的长期文化传播的有效方法。
- 自动规范推理中从 LegalRuleML 到 TPTP 的桥梁(扩展版)
本文提出了一种基于 TPTP 格式的伦理多元化推理语言,并提供了 LegalRuleML 与该语言之间的翻译模式,基于该模式提出了一种灵活的自动化伦理推理架构。
- MM非布尔形式主义优化统一框架
该论文提出了一种名为扩展权重系统的统一框架,可消除不同自动推理语言之间的句法区别,并研究了所提出系统的形式属性,即可在该框架内捕获的范例的形式属性。
- 命题框架中优化的抽象视角
提出了一种名为权重系统的统一框架,该框架消除了自动推理和知识表示中的语法差异,并解释了不同范例所提供的优化语句之间的异同,从而方便了翻译程序的开发和证明了不同框架的形式属性。
- Thor: 锤炼联合语言模型和自动定理证明器
该论文介绍了 Thor,一个集成语言模型和自动定理证明器的框架,它采用一种称为 “hammers” 的方法来选择前提,从而增加了语言模型在 PISA 数据集上的成功率并解决了相当一部分问题,同时比现有最佳方法在 MiniF2F 数据集上具有 - AAAI一项针对科学图表的目标检测网络系统评估
研究了不同的目标检测网络在 PlotQA 数据集上检测科学图中文本和视觉元素的准确性,提出了使用 Laplacian 边缘探测器的区域建议方法、包括相邻信息的特征表示、连接组件和自定义损失函数等优化方案,改进了当前模型的效率和准确度,并对自 - 基于数据驱动的布尔函数合成方法 Manthan
Manthan 是一种基于数据驱动的方法,将布尔函数综合视为分类问题,依赖于约束采样和自动推理等技术,通过对 609 个基准测试案例的评估,证明了其在现有技术上的显著改进,解决了当前技术不能解决的 60 个基准测试案例。
- 通过深度强化学习学习量化布尔公式的启发式
本文介绍了一种基于深度强化学习的高效启发式算法来自动推理量化 Boolean 公式。针对回溯搜索算法,在一类具有挑战性的问题集上,该算法能够解决比现有手写算法更多的公式。
- 神经网络自动验证:进展、挑战和展望
本文讨论了神经网络在安全和保密方面应用的局限性,提出了一些自动推理技术来提供神经网络性能的保障,并且对现有的神经网络自动验证方法进行了综合分类和阐述,同时讨论了存在的局限性以及未来研究的方向。
- 可解释人工智能的真正含义是什么?对于本质视角的新概念
本论文通过分析 NIPS,ACL,COGSCI 以及 ICCV/ECCV 论文标题的语料库来比较透明系统、可解释系统、理解系统和真正可以解释的系统之间的区别,并介绍了第四种概念:真正可解释的系统,其中自动推理是生成解释的关键步骤。