蜘蛛式策略发现和调度构建中的正则化
使用基于抽象争议框架（AFs）的模型定义了三种类型的 AFs 来证明或反驳使用者或求解器提出的面向固定用户决策的可行、高效或满意日程安排，从而提高解决约束、效率和决策问题的互动性和可解释性。
Nov, 2018
本文介绍如何在大型知识库的前提下进行自动定理证明，并通过深度强化学习技术中的基于词频 - 逆文档频率的查找开发出了一个混合陈述选择方法，以帮助探索并了解哪些前提适用于新的定理证明。实验表明，使用该方法进行训练的定理证明器优于仅以人类证明为基础的证明器，并可以接近于用模仿和强化学习相结合进行训练的证明器的性能。我们还通过多次实验来理解我们的探索方法背后的假设重要性，并解释了我们的设计选择。
May, 2019
本研究提出了一种新的调度方法，使用 GFlowNet 方法按比例抽样代理指标，通过在推理时间控制所提出的时间表的差异性和优良性之间的权衡以及将 GFlowNet 条件化为计算图，证明了相对于我们的方法，纯优化基线在目标模型上的性能不佳。
Jan, 2023
本文介绍一种用于优化 Datalog 查询的索引技术，通过确定最佳索引方案及 Datalog 规则的适当排列来降低内存消耗并优化查询效率，结果表明在不损失效率的情况下，内存使用显著减少。
Jul, 2019
不依赖于优化停止步骤 T 的现有学习率调度比依赖 T 的学习率调度性能更好。我们提出了一种完全避免使用调度的方法，同时在从凸问题到大规模深度学习问题的广泛问题范围内展示了与调度相比的最先进性能。我们的无调度方法与带有动量的标准优化器没有额外的超参数。我们的方法是我们开发的一种新理论的直接结果，该理论统一了调度和迭代平均化。我们的方法的开源实现可在此 URL 找到。
May, 2024
本文介绍了使用机器学习和 Monte Carlo 树搜索等技术，在 HOL4 交互式定理证明器之上开发自动证明工具 TacticToe 并对其进行了实验评估，结果表明 TacticToe 能够证明 7164 个定理中的 66.4%。
Apr, 2018
我们提出了一种新的自动定理证明方法，其中使用 AlphaZero 风格智能体自我训练来改进表达为非确定性程序的通用高级专家策略，同时具有类似的教师代理机自我训练来生成适当相关性和难度的任务以供学习者解决，利用最小领域知识来解决合成训练数据不可用或难以合成的问题，具体举例来说，我们考虑了用于命令程序的循环不变量合成，并使用神经网络来改进教师和求解策略。
May, 2022
本文使用数种 ATP 和 AI 方法证明了 3000 多个以前未证实的 Mizar/MPTP 问题，并将 ATP 解决的 Mizar 问题的数量从 75％提高到 80％以上。我们首先尝试了 cvc5 SMT 求解器，并使用了几个和超级位置系统不同的基于实例化的启发式方法，从而增加了很多新的解决方案。然后，我们使用自动化策略发明来开发 cvc5 的策略，大大提高了 cvc5 在困难问题上的性能。总之，这些方法解决了 14163 个以前未解决的难题中的 3021 个（21.3％），这是对 Mizar 大型理论基准的新里程碑和对 Mizar 的强化。
Jun, 2024