Sage：基于语义校正的数学形式化引擎

研究团队推出智能体框架 Sage，通过四阶段分解流水线与双信号语义校正循环，将自然语言数学表述转为高保真的 Lean 4 形式化陈述。Sage 在 Omni-MATH 上取得 73.3% 的 pass@4 联合编译与语义保真度（基线 Goedel-Formalizer-V2 为 42.0%），并将答案泄露率降至 2.7%。