摘要
大语言模型在数学和逻辑领域生成的论证虽具说服力，但常包含细微错误，如遗漏前提条件、无效推理模式或引用无法推导的引理。这些错误难以仅凭文本发现。相比之下，交互式定理证明器虽能保证严谨性，却需完全形式化且代价高昂。本文提出一种混合流水线：利用大语言模型生成紧凑领域特定语言中的类型化证明草图，再由轻量级可信内核将其扩展为显式的证明义务，从而兼顾灵活性与可靠性。
AI 推荐理由
论文核心解决数学逻辑推理中的错误问题，提出混合架构以提升推理可靠性。
研究机构
Automatic Data Processing, Inc
Atlanta, USA
Amazon Web Services, Inc
Bangalore, India
论文信息