热点事件持续更新

论文提出定义接地方法与ReuseBench，提升自动形式化定义兼容率

1 篇报道1 个报道来源4 小时前更新

先了解这件事

AI 综述

Leyan Pan 等在 arXiv 论文《Definition Grounding in Theory-Level Auto-formalization》中提出“定义接地”方法：对形式化定义持续评审和修订，以保证其被后续数学陈述复用的兼容性，并公开了用于形式化新数学领域与理论的基准 ReuseBench。基于论文摘要：Agent 形式化教材定义时，定义集合与后续陈述的兼容率通常仅 25%–50%；澄清非形式化定义后平均提升至 77.5%。仅陈述少量未证明的基本性质，也可使模型更善于发现兼容性问题，额外成本约为定义形式化成本的 11%。

AI 根据报道生成 · 3 小时前更新

最新进展10月15日 12:00

研究提出面向理论级自动形式化的定义接地方法

报道时间线

沿着报道，了解事件的不同侧面。

10月15日

12:00
arXiv · cs.AI
研究提出面向理论级自动形式化的定义接地方法
研究提出“定义接地”方法，通过持续评审和修订形式化定义，提高其被后续数学陈述复用的兼容性。基于论文摘要，Agent形式化教材定义时，定义集合与后续陈述的兼容率通常仅为25%–50%；澄清非形式化定义后，这一比例平均提升至77.5%。仅陈述少量未证明的基本性质，也可使模型更善于发现兼容性问题，额外成本约为定义形式化成本的11%。

本事件热度走势

可比范围当前: 9
可比范围峰值: 1010月15日 13:00
近 24 小时变化: –

趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。