我们提出了一种自动为入门编程问题提供反馈的新方法，该方法利用参考实现的任务和由可能制造的错误组成的错误模型。
Apr, 2012
通过GamePad系统，探索机器学习方法在Coq证明助手中的应用，通过基线模型训练解决“定位评估”和“策略预测”任务，从而探索定理证明与人类监督交替的可能性。
Jun, 2018
本文研究在形式数学中使用专家迭代进行语言建模，使用证明搜索交错学习的方法，以与仅使用证明搜索相比，达到显著优异的性能，成功地解决了高中奥林匹克竞赛等多个具有挑战性的问题，实现了基于miniF2F基准的最新技术水平。
Feb, 2022
本文介绍了一种名为DSP的方法，可以将非正式证明映射到正式证明草图并指导自动证明器，使其搜索更容易的子问题。实验证明语言模型能够产生结构良好的正式草图，并将其指导自动证明器，从而提高性能达到39.3%。
Oct, 2022
ProofNet是一个面向本科级数学自动形式化和形式证明的基准，包括371个例子，目的在于推动自动形式化和自动定理证明的进步。 通过上下文学习实现了对陈述自动形式化的基线结果。同时，引入了两种新的陈述自动形式化方法：提示检索和精炼反向翻译。该基准主要涵盖了实数和复数分析，线性代数，抽象代数和拓扑等主题。
Feb, 2023
介绍了在中学引入自动推理系统面临的几个瓶颈，讨论了一个基于推理规则和自动方法的实现并使用其进行几何猜想的证明，旨在介绍几何定理的形式证明，以激发学生的兴趣。
Mar, 2023
提出了一种基于流行测验的脚手架框架，使用符号推理和基于图的代码表示技术自动生成数百个流行测试，个性化指导初学者完成编程任务。
该研究论文通过探索定理证明技术在STEM教育中的软件支持，以实现从中学的直观数学方式到更正式学科的平滑过渡，并促进计算机科学家、数学家和教育者之间的相互理解。
Apr, 2024
数学证明教育的关键词包括准时反馈、自然语言处理、自动分级自由形式数学证明、用户研究。
Jun, 2024
利用神经网络的数学定理证明、代码验证和自动化定理证明等领域的研究，提出了一个测试用例，旨在进一步发展形式验证代码的自动定理证明。