arXiv：cs.LG（机器学习，全量分类）· Thomas Hirtz, Farzad Jafarrahmani, Abdelmouksit Sagueni, Xiang Zhou, Wenping Deng, Liang Zhang·2026-09-30 12:00· 1 天前AI 评分48

Sage：带语义纠错的自然语言数学形式化框架

Sage: Formalization with Semantic Correction

AI 导读

针对神经定理证明器依赖人工形式化陈述、类型检查器存在"严谨性幻觉"的问题，研究者提出智能体框架 Sage，用四阶段分解生成流水线配合双信号语义纠错循环，将 Lean 4 编译器诊断与多维语义反馈结合。