新上线今天0 投票
Sage 框架破解形式化验证「严谨性幻觉」：答案泄漏率从 70.9% 降至 2.7%
形式化数学的「最后一公里」难题
神经定理证明器在形式化数学领域屡有突破，但它们几乎都建立在一个未被言明的前提上：忠实的 Lean 4 形式化陈述已经被提供好了。真正把自然语言数学题翻译成形式语言，才是整个流程中最关键的瓶颈。
问题在于一种被称为「严谨性幻觉」（illusion of rigor）的现象：标准类型检查器只验证语句能否通过编译，却无法判断它是否丢掉了假设、引入了空洞的真命题、或悄悄改动了数学边界。一个「编译通过」的形式化陈述，未必忠实于原始题目。
Sage 的解法：分解生成 + 双信号纠错
针对这一痛点，研究者提出 Sage（Semantic Agent-Guided Formalization Engine，语义智能体引导的形式化引擎），用智能体框架取代传统的单体式翻译，核心设计包括两部分：
- 四阶段分解生成流水线：把翻译任务拆解为多个可控步骤，而非一次性端到端生成
- 双信号语义纠错循环：将 Lean 4 编译器诊断信息与多维语义反馈结合，在保证语法有效性的同时强制数学忠实性
论文特别指出，开放式查询与声明式形式化目标之间存在天然鸿沟。如果不对这一鸿沟显式建模，模型会通过猜测未经核实的答案来刷高形式化成功率——实验测得的答案泄漏率高达 70.9%。
关键数据
| 评测集 | Sage | 基线（微调 Goedel-Formalizer-V2） |
|---|---|---|
| Omni-MATH（无证明）联合编译与语义忠实 pass@4 | 73.3% | 42.0% |
| IMO-Unformalized（175 道未形式化 IMO 题）pass@4 验证忠实度 | 87.4% | 19.4% |
| 答案泄漏率 | 2.7% | 70.9% |
在盲测成对评估中，Sage 的胜率超过 79%。值得注意的是，IMO-Unformalized 是论文提出的一个全新前沿基准，包含 175 道尚未被形式化的国际数学奥林匹克竞赛题，Sage 在此展现出有效的零样本泛化能力。
为什么这件事重要
形式化数学长期被视为 AI 推理能力的「试金石」，但若训练数据本身就充满语义失真，模型学到的可能只是「编译技巧」而非数学理解。Sage 的价值不只在于指标提升，更在于它把语义忠实度变成了可优化、可度量的一等目标，并揭示了「高形式化率」背后可能隐藏的答案泄漏陷阱。
该论文共 27 页、4 张图，属预印本，涉及机器学习、人工智能、计算语言学和逻辑等多个方向。
