BMOA：编译器诱导数值偏差的基线-机制-结果归因
BMOA: Baseline-Mechanism-Outcome Attribution for Compiler-Induced Numerical Deviations
中文总结 AI 辅助
本研究针对编译器诱导的数值偏差问题，提出BMOA诊断框架，结合多维度比较方法，通过实证评估验证其可转化原始不匹配为可审计记录，为相关形式规范提供基础。
中文摘要 AI 辅助
形式化感知编译器的数值正确性，需要区分观测到的浮点差值的含义、证据支持的编译器行为以及随之产生的数值后果。现有测试工作流常将这些问题简化为通过/不通过的不匹配。我们引入基线-机制-结果归因（Baseline--Mechanism--Outcome Attribution，BMOA），这一诊断框架将比较关系与系统边界、证据支持的编译器机制、经参考校准的精度结果分离开来。BMOA结合了严格操作浮点、转换局部性、可复现性、跨编译器及更高精度的比较，同时在证据不足时保留混合、模糊和未知的归因。每条记录保留输入、配置、数值指标及支持构件以供审计。我们在6个科学计算核函数、确定性压力输入族以及ARM64上的受控Clang配置上评估BMOA。包含1276条记录的归因语料库和162个实例的受控机制矩阵显示，基线选择会改变诊断结果，编译器诱导的偏差并不意味着精度损失，且抵消和大动态范围在目标矩阵中表现出最强的效应。BMOA将原始不匹配转化为明确、可审计、受证据约束的记录。尽管它本身并非证明系统，但这些记录为未来感知编译器的数值正确性的形式规范和证明义务提供了实证基础。
英文摘要
Formalizing compiler-aware numerical correctness requires distinguishing what an observed floating-point difference means, what compiler behavior the evidence supports, and what numerical consequence follows. Existing testing workflows often collapse these questions into a pass/fail mismatch. We introduce Baseline--Mechanism--Outcome Attribution (BMOA), a diagnostic framework that separates the comparison relation and system boundary, the evidence-supported compiler mechanism, and the reference-qualified accuracy outcome. BMOA combines operational strict floating-point, transformation-local, reproducibility, cross-compiler, and higher-precision comparisons, while preserving mixed, ambiguous, and unknown attributions when evidence is insufficient. Each record retains inputs, configurations, numerical metrics, and supporting artifacts for audit. We evaluate BMOA on six scientific-computing kernels, deterministic stress-input families, and controlled Clang configurations on ARM64. A 1,276-record attribution corpus and a 162-instance controlled mechanism matrix show that baseline choice changes diagnoses, compiler-induced deviation does not imply accuracy loss, and cancellation and large dynamic range expose the strongest effects within the targeted matrix. BMOA converts raw mismatches into explicit, auditable, evidence-bounded records. Although it is not itself a proof system, these records provide an empirical foundation for future formal specifications and proof obligations for compiler-aware numerical correctness.
