用轻量级检查器验证LLM生成的数学推理草图，兼顾效率与可靠性。
ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning
- LLM生成紧凑的类型化证明草图，降低形式化门槛。
- 轻量级内核将草图展开为可验证的证明义务，确保逻辑正确。
- 适合需要高可靠推理但不愿全手工形式化的研究者。
大型语言模型（LLMs）虽能在数学和逻辑领域生成看似合理的论证，但常存在忽略前提条件、无效推导或引用无法在上下文中推导的引理等细微错误，这些错误仅凭文本难以察觉。相反，Lean、Coq等交互式定理证明器通过严格验证每一步语法和语义，保证了极高的可靠性，但代价是要求完全形式化证明，且需大量低层细节输入。本文提出一种混合管道：由LLM生成紧凑的类型化证明草图（使用专用领域语言DSL），再由轻量级可信内核将其扩展为明确的证明义务。该方法在保持可靠性的同时显著降低形式化负担。
原文摘要 · Abstract (English)
The large language models (LLMs) might produce a persuasive argument within mathematical and logical fields, although such argument often includes some minor missteps, including the entire omission of side conditions, invalid inference patterns, or appeals to a lemma that cannot be derived logically out of the context being discussed. These omissions are infamously hard to notice solely out of the text, as even the misconstrued construction still may seem mostly accurate. Conversely, interactive theorem provers like Lean and Coq have rigorous reliability by ensuring that syntactic and semantic statements only accept statements that can pass all the syntactic and semantic steps in the program which is a small trusted kernel of the language type-checks with. Despite the fact that this technique provides strong guarantees, it comes at quite a heavy price: the evidence must be completely formalized, and the evidence user or a auxiliary search program must provide an avalanche of low-level information. This paper presents a hybrid pipeline where an LLM generates a typed proof sketch in a compact DSL and a lightweight trusted kernel expands the sketch into explicit proof obligations.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。