arXiv · cs.AI· Leyan Pan, Christian Szegedy, Frederick Rajasekaran, Robi Bhattacharjee, Gregory Constantine, Wenke Lee·· 5 小时前
研究提出面向理论级自动形式化的定义接地方法
Definition Grounding in Theory-Level Auto-formalization
arXiv:2610.19223v1阅读论文 PDF ↗
仅依据论文摘要整理；未读取全文，实验条件、证明与基准细节请核对原文。
作者：Leyan Pan, Christian Szegedy, Frederick Rajasekaran, Robi Bhattacharjee, Gregory Constantine, Wenke Lee
研究任务与主要进展
研究提出“定义接地”方法，通过持续评审和修订形式化定义，提高其被后续数学陈述复用的兼容性。基于论文摘要，Agent形式化教材定义时，定义集合与后续陈述的兼容率通常仅为25%–50%；澄清非形式化定义后，这一比例平均提升至77.5%。仅陈述少量未证明的基本性质，也可使模型更善于发现兼容性问题，额外成本约为定义形式化成本的11%。
阶段、条件与复现 · 深读核对
- 新能力对应什么具体任务与最小输入输出？
- 代码、模型、数据、许可与可用入口是否明确？
- 效果、总成本、失效条件与实际工作流如何验证？
这些是阅读核对问题；材料未说明的条件保留未知。请结合上方论文版本、资料范围与原文核验。
来源：arXiv · cs.AI · arxiv.org