- FVEL：基于定理证明的大型语言模型互动式形式验证环境
提出了 FVEL，一种与大型语言模型一起进行交互式形式验证的环境，通过将给定的代码转化为 Isabelle 并利用神经自动定理证明来进行验证，利用 Isabelle 中的规则和定理，通过 FVELER 数据集进行评估，结果表明 FVEL 可 - miniCodeProps：证明代码属性的最小基准
利用神经网络的数学定理证明、代码验证和自动化定理证明等领域的研究，提出了一个测试用例，旨在进一步发展形式验证代码的自动定理证明。
- 递归证明定理
POETRY 使用逐级递归的方式在 Isabelle 定理证明机中证明定理，通过在每一级搜索可验证的证明草图并专注于解决当前级别的定理或猜想，从而解决了自动定理证明中的挑战。
- ACL借鉴失败：使用试错数据对直觉命题逻辑证明进行微调的 LLM
通过从失败的搜索路径中学习，我们展示了训练模型的益处。我们与仅使用正确路径训练的模型进行比较，并发现前者以更少的搜索次数解决了更多未见过的定理。
- 吴氏方法可使符号人工智能超越银牌，AlphaGeometry 在 IMO 几何竞赛中表现优异，超过金牌得主
利用自动定理证明方法解决国际数学奥林匹克竞赛（IMO）几何问题的研究中，AlphaGeometry 模型与 Wu 的方法的结合超越了 IMO 金牌得主的表现，解决了 30 个问题中的 27 个。
- 增强形式定理证明：一个用于训练 Coq 代码 AI 模型的综合数据集
该研究论文介绍了一个专门设计用于提高大型语言模型在解释和生成 Coq 代码方面能力的全面数据集，通过亦包含源引用和许可信息的数千个 Coq 源代码文件，初步实验表明使用该数据集训练的模型在 Coq 代码生成方面具有显著的潜力。
- 统一合成定理与证明数据的 MUSTARD 方法
该研究论文提出了 MUSTARD，一个数据生成框架，通过三个步骤合成高质量和多样化的定理和证明数据，用于理解大型语言模型在数学推理和定理证明方面的能力。利用 MUSTARD 生成的数据进行 Fine-tuning，可以在自动定理证明和数学问 - 抽象代数中的初等证明的自动规划技术
该研究探索了自动规划在自动定理证明中的应用，研究了利用规划构建抽象代数中的基础证明，证明自动规划技术在自动定理证明领域是可行的。
- EMNLPTRIGO：用于生成语言模型的形式化数学证明简化的基准测试
我们提出了 TRIGO，一个自动定理证明基准测试，要求模型能够逐步证明简化三角表达式，并评估生成型语言模型在公式推理、数字项操作、分组和因式分解方面的推理能力。我们从互联网收集三角表达式及其简化形式，并用 ``Lean'' 形式语言系统注释 - 数学游戏
Holophrasm 是使用 MCTS 和神经网络进行策略和评估的神经定理证明器，本文旨在通过其他游戏树搜索算法提高 Holophrasm 定理证明器的性能。
- FIMO：用于自动定理证明的挑战性形式化数据集
FIMO 是一个数据集，包括了国际数学奥林匹克竞赛的正式数学问题陈述，旨在促进 IMO 水平的高级自动定理证明。初始实验证明了目前方法的局限性，表明在实现令人满意的 IMO 水平自动定理证明结果之前还有很长的路要走。
- IJCAI基于高效不变名称的图神经网络表示的自动定理证明集成方法
使用强化学习和集成方法，借助改进的图神经网络和改良的公式表示方法，成功地构建了一种名称不变的公式表示方法，显着提高了自动定理证明的性能和泛化能力。
- 神经网络能做算术吗？对当今深度学习模型基本数学技能的调查
本文回顾了近年来关于深度学习在数学领域的研究，认为当前即使是最先进的深度学习模型在面对简单的数学和算术任务时也表现出较大局限性。
- MizAR 60 适用于 Mizar 50
我们发展出了一种 AI/TP 系统，通过使用基于学习的前提选择方法和增量训练方法，可以自动验证大量 Mizar 定理，证明效率高达 60％和 75％。
- 引理：生成、选择、应用
本研究中，我们探讨引理在自动定理证明中的重要作用，提出了一种结合学习技术的系统，该系统能够生成有用的引理来协助自动定理证明，并通过试验验证了该系统在几个代表性问题的解决方面的优越性，特别是成功解决了一系列难题，这些难题在过去 20 年间都未 - Magnushammer: 基于 Transformer 的前提选择方法
本文介绍了一个基于神经变换器的自动定理证明方法 Magnushammer，使用 PISA 基准测试，证明率达到 59.5％，超过了目前最成熟和最流行的基于符号的求解器 Sledgehammer 的 38.3％，并通过与基于语言模型的神经形式 - 证明结构研究
提出并阐述了一种新的证明操纵和分析形式主义，为证明检索方式提高了效率，实现了较短证明的自动化，特别是在首阶问题上的历史证明中进行了一项全面的形式重建分析。
- 将 QMLTP 问题翻译为高阶逻辑以求解
本文对自动证明系统 (Automated Theorem Proving, ATP) 在一阶模态逻辑问题的 QMLTP 库中的表现进行了评估，主要采取了嵌入法将问题转换为 TPTP 语言中的高阶逻辑，使用高阶逻辑 ATP 系统进行求解，并将 - 通过学习细化搜索策略来学习查找证明和定理 - 循环不变式合成的案例
我们提出了一种新的自动定理证明方法，其中使用 AlphaZero 风格智能体自我训练来改进表达为非确定性程序的通用高级专家策略，同时具有类似的教师代理机自我训练来生成适当相关性和难度的任务以供学习者解决，利用最小领域知识来解决合成训练数据不 - 奇妙的布丁：使用自动定理证明生成烹饪食谱
本文提出了 FASTFOOD，一种基于规则的自然语言生成程序，可用于烹饪食谱。该程序使用自动定理证明程序来选择成分和指示，具有一个时间优化模块，可以使其更加高效，并使用一种框架将自然语言生成分为 4 个阶段：内容生产，内容选择，内容组织和内