摘要
针对大模型在研究级数学问题中因自然语言歧义导致的验证难题，本文提出一种自动化框架。该框架包含非形式推理代理 Rethlas 与形式验证代理 Archon，前者模拟数学家工作流探索策略，后者通过任务分解将论证转化为 Lean 4 形式证明。实验成功自动解决并验证了一个交换代数开放问题，展示了非形式与形式推理系统协同工作的新范式，显著减少人工干预并确保证明正确性。
AI 推荐理由
论文核心聚焦于结合自然语言推理与形式化验证解决数学问题，显著提升推理可靠性。
研究机构
北京大学数学科学学院
北京大学前沿交叉学科研究院
日本京都大学数理研究所
清华大学数学科学系
论文信息