Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees
🔍 耿同学打假报告
论文信息
- 标题：Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees
- 作者：Xiaoyang Liu, Zineng Dong, Yifan Bai, Yantao Li, Yuntian Liu, Tao Luo
- 期刊：Proceedings of the 43rd International Conference on Machine Learning (PMLR 306, 2026)
- DOI：arXiv:2604.19000v2
- 发表年份：2026 (arXiv 22 May 2026)
- 论文来源：2604.19000v2.pdf
综合评定：🟡 存疑
本论文为 NLP/自动形式化领域的方法论论文。复核后，原报告的统计取证结论（末位数字分布、Benford 检验）因引用的统计量数值无法在原文中找到对应数据点而被判为"结论不成立"并删除；图像 PRNU/copy-move/噪声方差信号因无法在论文原文中找到对应数据点，且原报告未提供可在原文中验证的具体证据（仅引用机器取证编号与像素参数），按规则无法保留为有效结论；Table 2 中 Goedel-V2-Formalizer-32B (Global Repair) 行的列宽错位为可观察的文本异常，原文确实呈现该行仅有 5 个数值，保留为依据不足的疑点；Figure 4 修复示例中的代码引用经核验未在原文中完全命中对应字符串，因依据不足删除。综合复核后剩余的可疑线索为单一的 Table 2 列错位疑点，定级为 🟡 存疑。
详细发现
⚠️ 发现 1：Table 2 中 Goedel-V2-Formalizer-32B (Global Repair) 行数据列数异常
- 位置：Table 2, "Baselines (Global Repair)" 组，Goedel-V2-Formalizer-32B 一行
- 描述：该行在论文原文中实际呈现为
Goedel-V2-Formalizer-32B 96.31 72.51 63.07 77.56 62.82，仅含 5 个数值。同一组其他基线行（如 Qwen3-Max、Kimina-Autoformalizer-7B、ATF-32B 等）均报告了 12 个数值（ProverBench/ProofNet/PRIME × SC/CC）。该行只显示了 5 个数值，明显存在列缺失或排版错位。 - 证据：原文 Table 2 "Baselines (Global Repair)" 中除 Goedel-V2-Formalizer-32B 行外的其他 7 行均报告 12 个数值。Goedel-V2-Formalizer-32B 的 Pass@k 行报告了完整的 12 个数值（95.38 / 83.38 / 77.63 / 70.89 / 77.56 / 66.67），与其下方的 Global Repair 行数值无法对应拼接，可推断存在排版错位或数据缺失。
- 良性解释评估：可能是 LaTeX 表格在排版时因 96.31 与下一列重叠或换行丢失。论文未提供原始数值，无法判断是 OCR 提取错误还是源文件本身的缺陷。
- 严重程度：🟡
- 复核状态：⚠️ 依据不足（仅观察到列数不一致，原文未给出导致该现象的具体说明，无法判定为排版缺陷还是数据缺失）
耿同学辣评
这篇论文把"自动形式化"包装成"分解+结构+修复"三板斧，方法描述读起来头头是道。不过耿同学要把原报告里的"统计奇偶失衡 0.33"和"Benford χ² 四百"先撤掉——那些统计量本身没有出现在原文里，是机器取证跑出来的间接证据，不能当原文数据用。但有一个小细节让我想多看两眼：Table 2 里 Goedel-V2-Formalizer-32B (Global Repair) 那一行，只给了 5 个数，比同组的其他基线少了一半多，要么是排版时某列被吃掉了，要么——你懂的。论文已经开源 GitHub，耿同学建议先去仓库里把 Table 2 的 evaluation log 翻出来对一对，别让一行少列的数据挡住 ICML 2026 的 spotlight。
建议后续行动
- 访问 https://github.com/XiaoyangLiu-sjtu/DSR 核对 Table 2 的完整 evaluation logs，确认 Goedel-V2-Formalizer-32B (Global Repair) 一行缺失的 7 个数值
- 联系作者要求提供 Table 2 的源 CSV/JSON 数据，重点核查 Goedel-V2-Formalizer-32B 在 Global Repair 设定下 ProverBench SC 的实际数值
- 在 PubPeer 上提出对 Table 2 列缺失的具体技术性质疑（请求补全数据，而非定性指控）
- 复核 GitHub 仓库中 evaluation scripts 是否能复现 Table 2 的报告数值
⚠️ 免责声明
本报告由 AI 辅助生成，仅供学术讨论参考。
学术不端的最终认定需要专业机构调查。
我们支持学术诚信，但也尊重每一位研究者的名誉权。
如有异议，请以官方调查结论为准。
本工具不保证检测结果的准确性，误报和漏报均有可能。