arXiv：cs.AI· Yuming Feng, Tadd Mao, Dhruva Arekar, Tianjun Zhong, Jiani Huang, Xujie Si, Ziyang Li·· 5 小时前
FaithAlign：面向理论级自动形式化的忠实性对齐基准
Aligning Faithfulness for Theory-Scale Autoformalization
AI 导读
研究提出 FaithAlign，首个理论级自动形式化忠实性基准，含 460 个条目和 4,982 条短语级标注链接，另有 FaithAlign-Gap 的 146 个条目隐藏非形式化上下文与假设。
正文
Abstract:Autoformalization (AF) requires more than compilation: formal statements must preserve the meaning of their informal sources, a property known as faithfulness. An emerging frontier is the automated evaluation of this property, yet most existing methods operate at the statement level and produce whole-item verdicts, failing to reveal how individual expressions correspond or which contextual interpretations support the judgment. This omission is consequential because AF is inherently theory-scale: target statements derive their meaning from surrounding mathematical material and unstated conventions. We formulate faithfulness evaluation as a context-aware align-then-label problem: identifying phrase-level correspondences between informal and formal statements and assigning a faithfulness label to each under explicitly specified contextual interpretations and assumptions. We also introduce FaithAlign, the first theory-scale faithfulness benchmark comprising 460 items and 4,982 annotated phrase-level links, alongside FaithAlign-Gap, a companion set of 146 items with informal context and assumptions withheld. Each FaithAlign item includes the target statement pair, relevant context, formal dependencies, and, where needed, assumptions specifying one given interpretation. Across 8 models, GPT-6 Astra achieves the highest defect F1 at 47.8% and identifies all defects in only 4.5% of items with two or more defects. On FaithAlign-Gap, Astra identifies only 28.2% of undecidable items as such. These results show the difficulty of recovering context-dependent correspondences, establishing FaithAlign as a testbed for fine-grained, context-aware faithfulness evaluation.
| Subjects: | Computation and Language (cs.CL); Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2610.18498 [cs.CL] |
| (or arXiv:2610.18498v1 [cs.CL] for this version) | |
| https://doi.org/10.48550/arXiv.2610.18498 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Yuming Feng [view email]
[v1]
Tue, 13 Oct 2026 14:53:04 UTC (2,176 KB)
来源：arXiv：cs.AI · arxiv.org