OpenAI用生成式语言模型自动证明定理

OpenAI 发布了一项研究，探索使用生成式语言模型进行自动定理证明。该工作将定理证明视为一个序列生成问题，利用大规模语言模型生成证明步骤，并在多个数学领域进行了测试。结果表明，该方法在形式化定理证明任务上取得了显著进展，能够生成比传统方法更长的证明链，并发现了一些新的证明路径。研究还讨论了模型在数学推理中的局限性，如对复杂逻辑结构的处理能力。该工作为 AI 辅助数学研究提供了新思路，但距离完全自动化证明仍有距离。