我们使用交互式定理证明器 Isabelle/HOL 对一种近似策略迭代算法在因子化马尔可夫决策过程上进行了形式验证。接着，我们展示了如何将形式化的算法细化为可执行的验证实现。所开发的实现方案经过了基准问题的评估，表明其实用性。作为细化的一部分，我们开发了经过验证的软件以认证线性规划解法。该算法基于丰富的形式化数学库，并推动了交互式定理证明器的现有方法的极限。我们讨论了验证项目的过程以及为形式验证所需的算法修改。

Jun, 2024

通过可交互的证明助手，开发者能够证明机器学习系统的正确性，这种方法暴露了所有的实现错误，并通过 Certigrad 实现了优化的随机计算图，并生成了一个机器可验证的证明，证明了系统采样的梯度是数学梯度的无偏估计方法。

Jun, 2017

通过提出一种新的流程，我们利用合成数据来将自然语言数学问题转化为 Lean 4 语句，并相应地进行过滤，从而为解决 LLMs 在理解复杂数学问题和证明上的性能提供有用的训练数据。最终数据集包含约 57K 个正式 - 非正式问题对以及来自数学竞赛论坛的搜索证明和 21 个新的 IMO 问题。

Jun, 2024

这篇论文通过 EvoGPT-f 回答了关于五种形式数学语言（Lean 3、Lean 4、Coq、HOL 4、HOL Light）和四种标记化方法（字符、词级、字节对编码和 StarCoder 标记器）之间的差异化机器学习能力的定量分析，为进一步开展社区间系统定量和定性比较研究奠定了基础。

Feb, 2024

基于大规模合成数据，使用 Lean 4 proof 数据生成方法，我们的模型在定理生成和解决题目方面取得了卓越的成果，证明了合成数据对提高 LLMs 中的定理证明能力的潜力。

May, 2024

本研究使用大型语言模型 (Codex) 探讨将使用自然语言书写的数学（即定义，定理陈述和证明）转化为可以被程序检查正确性的形式语言的能力，并发现对于 120 个定理，Codex 可以在本科水平上以近 75％的准确率进行短数学陈述的形式化。同时在选择合适的输入和后处理策略下，Codex 可以以自然语言形式翻译本科水平的 13 个定理的证明，这些具有两到三自然段长度的证明可以在 12 次中有至少一次完成翻译，这表明大型语言模型是完全或部分自动化形式化的有前景的途径。

Nov, 2022

提出了一种定理证明算法，该算法使用几乎没有领域启发式来指导其连接风格的证明搜索，而是运行许多蒙特卡罗模拟，通过强化学习来指导以前的证明尝试。

May, 2018

本研究使用神经序列模型探讨在自动定理证明的命题选择方面的有效性，提出了一个两级方法，能够在避免现有最先进模型的手工设计功能的同时在 Mizar 语料库上为 premise selection 任务提供良好结果。据我们所知，这是首次在大规模的定理证明中应用深度学习。

Jun, 2016

该研究提出了一种名为学习数学抽象（LEMMA）算法，该算法可以通过引入抽象步骤来增强专家迭代，并利用层次化抽象的思想来帮助强化学习代理人解决数学问题，实验结果表明该算法可以有效提高已有代理人的解决问题能力和泛化能力。

Nov, 2022

本文提出了一种用于高级数学推理的数据集，研究了神经序列到序列模型的推理能力。实验结果表明，该任务具有挑战性，但神经模型能够捕捉到非平凡的数学推理，提出的分层 Transformer 的性能也好于基准 Transformer。

Jun, 2020