arXiv cs.AI· Yuming Feng, Tadd Mao, Dhruva Arekar, Tianjun Zhong, Jiani Huang, Xujie Si, Ziyang Li·· 3 天前AI 评分29
FaithAlign：面向理论级自动形式化的忠实性对齐评测基准
Aligning Faithfulness for Theory-Scale Autoformalization
AI 导读
研究者提出 FaithAlign，首个理论级忠实性评测基准，包含 460 个条目和 4,982 条短语级标注链接，将忠实性评估建模为上下文感知的"先对齐再标注"问题。
正文 · AI 翻译
摘要：自动形式化（AF）不仅仅需要编译：形式化陈述必须保留其非形式化来源的含义，这一性质被称为忠实性。一个新兴的前沿方向是对该性质的自动化评估，然而现有方法大多在陈述层面运作并给出整体判定，无法揭示各个表达式如何对应，或哪些上下文解释支持该判断。这一缺失影响重大，因为 AF 本质上是理论规模的：目标陈述的意义源自周围的数学材料与未明说的约定。我们将忠实性评估表述为一个上下文感知的先对齐后标注问题：识别非形式化与形式化陈述之间的短语级对应关系，并在明确指定的上下文解释与假设下为每个对应关系赋予忠实性标签。我们还提出了 FaithAlign，这是首个理论规模的忠实性基准，包含 460 个条目和 4,982 条标注的短语级链接，以及配套的 FaithAlign-Gap，包含 146 个条目，其非形式化上下文与假设被隐去。每个 FaithAlign 条目包含目标陈述对、相关上下文、形式化依赖，以及在需要时指定某一给定解释的假设。在 8 个模型中，GPT-6 Astra 取得了最高的缺陷 F1，为 47.8%，并且仅在 4.5% 的含两个或更多缺陷的条目中识别出全部缺陷。在 FaithAlign-Gap 上，Astra 仅将 28.2% 的不可判定条目识别为不可判定。这些结果表明恢复上下文相关对应关系的难度，确立了 FaithAlign 作为细粒度、上下文感知忠实性评估测试平台的地位。
| 主题： | 计算与语言（cs.CL）；人工智能（cs.AI） |
| 引用为： | arXiv:2610.18498 [cs.CL] |
| （或 arXiv:2610.18498v1 [cs.CL] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.18498 arXiv 颁发的 DOI 经由 DataCite（待注册） |
提交历史
来自：Yuming Feng [查看电子邮件]
[v1]
2026年10月13日星期二 14:53:04 UTC（2,176 KB）
来源：arXiv cs.AI · arxiv.org