ProofSketcher：面向可靠数学/逻辑推理的混合LLM与轻量级证明检查器

大语言模型（LLM）在数学与逻辑领域能产出颇具说服力的论证，但这类论证常包含一些小疏漏，例如完全遗漏侧条件、无效的推理模式，或诉诸无法从所讨论上下文逻辑推出的引理。这些疏漏仅凭文本本身极难察觉，因为即便是被误解的构造，看起来也大多是对的。相比之下，Lean、Coq等交互式定理证明器具有严格的可靠性，其确保只接受能通过语言小型可信内核中全部语法与语义检查步骤的陈述。尽管该技术提供了强保证，其代价也相当高昂：证明必须完全形式化，且证明使用者或辅助搜索程序必须提供海量的低层信息。本文提出一种混合流水线：由LLM以紧凑DSL生成带类型的证明草图，再由轻量级可信内核将草图展开为显式的证明义务。