📖 AI 总结

本文提出Sage（语义智能体引导的形式化引擎），旨在解决自然语言数学命题转化为Lean 4形式化语句时的"严谨性幻觉"问题——传统类型检查器会接受那些虽能编译但丢失假设、引入空洞真值或篡改数学边界的语句。Sage以四阶段分解生成流水线替代单体式翻译，并配合双信号语义校正循环，将Lean 4编译器诊断与多维语义反馈相结合，在保证语法有效的同时强制数学保真度。该框架明确区分开放式查询与声明式形式化目标之间的差距，从而抑制模型通过猜测未验证答案来虚高形式化率的行为：单体基线答案泄漏率高达70.9%，Sage将其压低至2.7%，并在无证明的Omni-MATH上实现73.3%的pass@4联合编译与语义保真度，显著优于微调后的Goedel-Formalizer-V2基线（42.0%）。在包含175道未形式化IMO题目的IMO-Unformalized基准上，Sage展现出有效的零样本泛化能力，pass@4验证保真度达87.4%，而基线仅为19.4%，并在超过79%的盲评成对比较中胜出。

🔑 关键词速览