Lean Hammer 的前提选择

神经方法正在改变证明助手的自动推理，但将这些进展集成到实际验证工作流程中仍具有挑战性。锤子是一种工具，将前提选择、翻译到外部自动定理证明器以及证明重构集成为一个整体工具，以自动化繁琐的推理步骤。我们提出了 LeanPremise，一种新型神经前提选择系统，并将其与现有的翻译和证明重构组件结合，创建了 LeanHammer——第一个面向 Lean 证明助手的端到端领域通用锤子。与现有的 Lean 前提选择器不同，LeanPremise 专为依赖类型论中的锤子而设计。它还能动态适应用户特定的上下文，有效地从训练数据之外的库中推荐前提，以及来自用户本地定义的引理。通过全面的评估，我们展示，LeanPremise 使 LeanHammer 解决的目标数量比现有的前提选择器多出 21%，并能良好地针对 diverse domains 进行泛化。我们的工作有助于搭建神经检索与符号推理之间的鸿沟，使研究人员和实践者更易于进行形式化验证。