关键词interactive theorem provers
搜索结果 - 5
- 通过数据增强和动态采样方法提升神经定理证明
DS-Prover 是一个用于定理证明的创新动态抽样方法，通过根据剩余时间和总分配时间来调整探索和开发之间的平衡，以提高证明搜索过程的效率，并通过拆分简化和重写策略为具有单个前提的策略来扩充训练数据集，从而在 MiniF2F 和 Proof - 基于自动正式化的数学和代码正确性研究：基础证明实验
本研究介绍了一种基于 Universal Transformer 体系结构的语义解析方法，可以将基本数学证明转化为 Coq 互动定理证明器中的等效形式，以及将装饰有 Hoare 三元组的简单命令式代码翻译成 Coq 中的形式验证证明。通过人 - 利用神经网络生成正确性证明
本文提出了一个使用机器学习技术的证明搜索系统 Proverbot9001，它能够自动化之前需要手动完成的证明，有效地产生了 27.5% 的证明陈述，在 Coq 中产生了 4 倍的提高。
- TacticToe: 学习使用策略证明
本文介绍了使用机器学习和 Monte Carlo 树搜索等技术，在 HOL4 交互式定理证明器之上开发自动证明工具 TacticToe 并对其进行了实验评估，结果表明 TacticToe 能够证明 7164 个定理中的 66.4%。
- Coq 中的证明模式重用：案例研究
本文开发了机器学习工具 ML4PG，并详细研究了在交互式定理证明器和使用电子库中的定理模式，以便为用户提供指导。