3D-Prover：基于行列式点过程的多样性驱动定理证明
原文中文，约300字，阅读约需1分钟。发表于：。本研究解决了自动化形式推理中的搜索空间问题，该问题随着证明深度的增长而呈指数级增加。通过使用历史证明尝试生成的合成数据，提出了一种新的过滤机制，从中选择语义多样性高且质量优良的策略，从而显著提高了证明成功率和执行效率。
LeanDojo是一个开源的交互式证明环境，用于从Lean中提取数据和注释，帮助选择前提。基于这些数据，我们开发了ReProver，这是首个增加检索功能的LLM证明程序，只需一台GPU训练一周。我们还创建了一个包含96962个定理的新基准进行评估。实验表明，ReProver比非检索基线和GPT-4更有效。代码和数据集已发布以支持研究。
