Neural methods are transforming automated reasoning for proof assistants, yet integrating these advances into practical verification workflows remains challenging. A hammer is a tool that integrates premise selection, translation to external automatic theorem provers, and proof reconstruction into one overarching tool to automate tedious reasoning steps. We present LeanPremise, a novel neural premise selection system, and we combine it with existing translation and proof reconstruction components to create LeanHammer, the first end-to-end domain general hammer for the Lean proof assistant. Unlike existing Lean premise selectors, LeanPremise is specifically trained for use with a hammer in dependent type theory. It also dynamically adapts to user-specific contexts, enabling it to effectively recommend premises from libraries outside LeanPremise's training data as well as lemmas defined by the user locally. With comprehensive evaluations, we show that LeanPremise enables LeanHammer to solve 21% more goals than existing premise selectors and generalizes well to diverse domains. Our work helps bridge the gap between neural retrieval and symbolic reasoning, making formal verification more accessible to researchers and practitioners.

翻译：神经网络方法正在变革证明助手的自动推理技术，然而将这些进展整合到实际验证工作流中仍面临挑战。Hammer是一种集成工具，它将前提选择、外部自动定理证明器的转换以及证明重构整合为一个整体工具，以自动化繁琐的推理步骤。本文提出了LeanPremise——一种新颖的神经网络前提选择系统，并将其与现有的转换及证明重构组件相结合，构建出首个面向Lean证明助手的端到端通用领域工具LeanHammer。与现有的Lean前提选择器不同，LeanPremise专门针对依赖类型理论中的hammer应用进行训练。该系统还能动态适应用户特定语境，使其能够有效推荐训练数据之外的库中的前提以及用户本地定义的引理。通过全面评估，我们证明LeanPremise使LeanHammer相比现有前提选择器多解决21%的证明目标，并能良好泛化至不同领域。本研究有助于弥合神经检索与符号推理之间的鸿沟，使形式化验证对研究人员和实践者更具可及性。