在现代计算体系中，浮点数学函数的精度直接影响科学计算、金融建模和工程仿真的可靠性。GNU C Library（glibc）作为 Linux 系统的核心数学库，其实现的每一个超越函数都面临着正确舍入（correct rounding）的严格考验。atanh（反双曲正切函数）作为基础超越函数之一，其正确舍入实现的进展折射出整个浮点数学库领域的精度工程演进。
正确舍入的概念与 IEEE 754 标准框架
正确舍入是 IEEE 754 浮点标准体系中的核心要求之一。简言之，对于任意给定输入 x 和指定的舍入模式（如最近偶数舍入、向零舍入、向上舍入、向下舍入），数学函数的实现必须返回与数学精确结果最接近的可表示浮点数。当精确结果恰好位于两个相邻可表示值的中点时，实现必须根据当前舍入模式的规则选择上方或下方的值。这一要求看似简单，但实现起来却面临严峻挑战。
IEEE 754 定义了四种舍入模式：round-to-nearest（最近偶数）、round-toward-positive-infinity（向上）、round-toward-negative-infinity（向下）和 round-toward-zero（向零）。对于 atanh 这类超越函数，其数学定义涉及对数和除法运算，在边界区域（如输入接近 1 或 -1 时）会产生极大的导数值，微小的输入变化可能导致输出发生显著变化。传统实现往往仅保证 round-to-nearest 模式下的精度，而忽视了其他三种模式的严格正确性要求。
glibc 的数学库（libm）在历史上长期采用混合策略：针对常见输入范围优化性能，对极端输入和特定舍入模式则仅保证 “足够好” 的精度。这种务实选择在大多数应用场景中运行良好，但无法满足严格合规性要求和高精度计算场景的需求。近年来，随着 CORE-MATH 项目的崛起，这一状况正在发生根本性转变。
CORE-MATH 项目的正确舍入方法论
CORE-MATH（Correctly Rounded Mathematical Functions）是由法国国家信息与自动化研究所（INRIA）发起的开源项目，旨在为一系列基础数学函数提供经过严格验证的正确舍入实现。该项目的核心方法论融合了区间算法、多项式逼近和形式化验证技术，确保实现能够在整个输入域内满足 IEEE 754 的正确舍入要求。
与传统的基于表格查找（table-driven）方法不同，CORE-MATH 采用了一种被称为 “区域分解” 的策略。开发者将函数的定义域划分为多个互不重叠的区域，在每个区域内使用精心设计的多项式近似。在边界区域（正确舍入的最困难区域），实现会使用更高的精度进行中间计算，以确保最终结果的正确性。这种方法在保证正确性的同时，也兼顾了实际性能。
根据 2024 年的项目进展报告，CORE-MATH 已经完成了包括 atanh、asinh、acosh 在内的多个反双曲函数的正确舍入实现。这些实现的源代码托管于 GitLab 仓库，并获得了广泛的测试覆盖。项目团队还发表了详细的基准测试数据，表明在现代 x86_64 架构上，CORE-MATH 实现的性能与现有的非正确舍入实现相当，这意味着正确舍入不再是性能的对价。
glibc 对 CORE-MATH 的集成与工程实践
glibc 维护团队近年来积极将 CORE-MATH 的实现成果集成到官方版本中。这一集成过程并非简单的代码复制，而是涉及大量的适配工作。glibc 使用了一套名为 math_config.h 的框架来处理错误域（errno）、溢出和下溢等边界条件，实现必须与这一框架无缝对接。
2024 年 12 月发布的补丁系列展示了这一集成的具体进展。glibc 开始逐步将 CORE-MATH 的实现方式纳入其数学库代码树，使用与 CORE-MATH 相似的算法框架，但对代码风格和构建系统进行了调整以符合 glibc 的整体架构。值得注意的是，集成工作首先从 binary32（单精度）函数开始，因为单精度实现的验证相对简单；随后逐步扩展到 binary64（双精度）函数。
对于 atanh 函数而言，集成工作尤其具有挑战性。atanh 的数学定义为 0.5 × ln ((1+x)/(1-x))，当 |x| 接近 1 时，分子和分母都非常接近零，直接计算会导致严重的有效数字损失。传统的实现会使用特殊处理的分支来避免这一问题，CORE-MATH 的实现则采用了更精细的区间划分策略，在不同输入区间使用不同的计算路径，以确保在所有情况下都能返回正确舍入的结果。
精度验证与测试框架
正确舍入的实现必须经过严格的验证才能投入使用。glibc 项目维护了一套完整的测试框架，包括穷举测试和随机测试两种方式。穷举测试遍历目标浮点格式的全部可表示输入，对于 binary64 而言这意味着约 2^64 个测试点，显然不切实际；因此实践中通常只对特定 “困难” 区域进行穷举测试，而对其他区域采用统计抽样。
一种广泛采用的验证方法是使用参考实现（reference implementation）进行比对。参考实现通常使用更高精度（如 128 位浮点或任意精度算术）计算数学精确结果，然后与被测实现的结果进行比较。如果被测实现在所有测试用例上都返回了正确舍入的值，就可以认为其正确性得到了高度置信度的验证。CORE-MATH 项目提供了这样的参考实现，并与测试框架紧密集成。
此外，形式化验证方法也在逐步进入这一领域。通过使用证明助手（如 Coq 或 ACL2）证明实现代码与数学定义的等价性，可以获得更强的正确性保证。虽然这种方法目前还不常见于生产级数学库，但它代表了未来的发展方向。
工程实践中的关键参数与配置
对于需要在生产环境中部署正确舍入数学函数的开发者，以下几个工程实践要点值得关注。首先是舍入模式的配置，现代 x86_64 处理器默认使用 round-to-nearest 模式，但可以通过控制寄存器（FCW / MXCSR）切换到其他模式；正确舍入实现应该在所有四种模式下都能正常工作。
其次是精度配置，某些应用程序可能使用扩展精度（如 x87 80 位浮点）进行中间计算，这可能导致与 IEEE 754 binary64 预期的结果不一致。开发者应确保应用程序的浮点环境配置与预期一致。
第三是性能与精度的权衡。对于性能敏感的场景，可以考虑使用手动内联的近似实现，但必须清楚这种近似带来的精度损失；对于精度敏感的场景（如金融计算），应坚持使用经过验证的正确舍入实现。
glibc 2.40 及更高版本已经开始包含部分 CORE-MATH 集成的实现。开发者可以通过检查 glibc 的版本信息和 math 目录下的源代码确认具体函数的支持状态。对于需要完全正确舍入保证的场景，也可以考虑单独链接 CR-LIBM 等专门提供正确舍入保证的数学库。
资料来源：The CORE-MATH project (https://core-math.gitlabpages.inria.fr)；glibc 数学库补丁系列（sourceware.org/pipermail/libc-alpha）。