通过使用大型语言模型，我们提出了 PropTest 策略来改进可视化编程，这一策略可生成用于测试可视化属性的代码解决方案，提高可视化推理任务的性能和泛化能力。

Mar, 2024

本文提出了一个使用机器学习技术的证明搜索系统 Proverbot9001，它能够自动化之前需要手动完成的证明，有效地产生了 27.5% 的证明陈述，在 Coq 中产生了 4 倍的提高。

Jul, 2019

该研究论文介绍了一种用于神经网络代码验证的基准测试集 NeuroCodeBench，包含 32 个神经网络和 607 个安全属性，主要研究安全关键系统中的神经网络、验证和软件错误。

Sep, 2023

ProofNet 是一个面向本科级数学自动形式化和形式证明的基准，包括 371 个例子，目的在于推动自动形式化和自动定理证明的进步。 通过上下文学习实现了对陈述自动形式化的基线结果。同时，引入了两种新的陈述自动形式化方法：提示检索和精炼反向翻译。该基准主要涵盖了实数和复数分析，线性代数，抽象代数和拓扑等主题。

Feb, 2023

LangProp 是一个用于大型语言模型（LLMs）生成的代码的迭代优化框架，在监督 / 强化学习环境中使用。LangProp 自动评估代码在输入输出数据集上的性能，并捕获任何异常，然后将结果反馈给 LLM 以在训练循环中迭代改进生成的代码。这是自动驾驶的代码优化的第一个概念验证，表明 LangProp 能够生成可解释和透明的驾驶策略，可以在基于度量和数据的方式上进行验证和改进。

Jan, 2024

本研究介绍了一种基于 Universal Transformer 体系结构的语义解析方法，可以将基本数学证明转化为 Coq 互动定理证明器中的等效形式，以及将装饰有 Hoare 三元组的简单命令式代码翻译成 Coq 中的形式验证证明。通过人工和人工写作证明的有限领域的实验表明，这些模型对于训练期间未看到的中间长度和自然语言变化具有很好的泛化能力。

Jan, 2023

LEGO-Prover 使用技能库，通过模块化构建证明以及生成新技能，提高了大型语言模型在定理证明中的能力，并进一步推进了数学领域的研究。

Oct, 2023

DS-Prover 是一个用于定理证明的创新动态抽样方法，通过根据剩余时间和总分配时间来调整探索和开发之间的平衡，以提高证明搜索过程的效率，并通过拆分简化和重写策略为具有单个前提的策略来扩充训练数据集，从而在 MiniF2F 和 ProofNet 两个标准数据集上实现了显著的性能提升。

Dec, 2023

本文介绍了 LeanDojo：一个开源、可交互的证明环境，它从 Lean 中提取了证明中的数据及注释，提供了有价值的前提数据，以便于选取前提。 我们使用此数据，开发了 ReProver：第一个增加检索功能的基于 LLM 的证明程序。其成本低廉，只需要一台 GPU 进行一周的训练，并且可以有效地选择定理中的前提。我们构建了一个包含 96962 个定理和证明的新基准，并将其用于培训和评估。实验结果表明，相对于非检索基线和 GPT-4，ReProver 非常有效。我们发布了代码和数据集，以促进进一步的研究。

Jun, 2023

该论文表明，通过使用现有的证明助理，可以以与建立证明助理自身的信任和可审计性原则相一致的方式，构建对自然语言表达的规范的支持。我们在 Lean 证明助理内实现了一种方式，以可扩展的正式英语子集提供规范，并自动将其翻译成正式的命题。我们的方法是可扩展的（对语法结构没有永久限制），模块化的（允许在库中分发有关新词的信息），并且生成解释了每个词的解释方式以及如何使用句子结构来计算含义的证明证书。我们将原型应用于从一本流行教材中翻译各种正式规范的英文描述；在仅需进行小幅修改的情况下，借助一个适度的词汇表，所有规范都能被正确翻译。

Oct, 2023