2024年7月12日，陈长波研究员邀请华东师范大学软件工程学院杨争峰教授来访生物计算安全重庆市重点实验室，并在综合科研楼412会议室举办一场题为“基于深度学习的自动定理证明”的学术报告。

       自动定理证明（ATP）是计算机科学中的一个重要分支，传统上依赖于证明搜索技术。近年来，随着机器学习技术的快速发展，它为自动定理证明提供了新的解决方案。然而，将机器学习技术应用于自动定理证明仍面临许多挑战，尤其是现有证明数据的限制。

        在本次报告中，杨争峰教授将介绍一种新的自动定理证明方法，该方法结合了大型语言模型（LLMs）和深度强化学习（DRL）。此外，其团队还开发了一个名为LeanComb的正式基准测试，用于使用Lean证明组合恒等式。该基准测试背后支持的是一个利用蒙特卡洛模拟和深度强化学习生成新定理的定理生成器。实验结果表明，该证明器不仅在性能上超越了一些现有的机器学习方法，而且在MetaMath基准测试中与最先进的启发式定理证明器竞争效果显著。

        此次报告不仅为学术界提供了一个了解和讨论自动定理证明最新进展的平台，也展示了深度学习如何推动传统科学研究的边界。

                                杨争锋教授作学术报告 

                                                            研讨会现场