标签
华为 Lagrange 数学计算研究中心提出 Sage，一个四阶段分解生成管线加双重信号语义校正循环的自动形式化框架，将答案泄漏率从 70.9% 降至 2.7%，在 Omni-MATH NP 上达到 73.3% pass@4，并在新提出的 IMO-Unformalized 基准上零样本达到 87.4% 验证保真度。
本文介绍了AutoGraphForge，这是一个用于自动化图论发现的计算管道，它生成猜想，针对大数据集进行测试，并使用神经证明器在Lean 4中进行形式化验证。