arXiv cs.AI· B\'alint Gyevn\'ar, Simon DeDeo·· 11 小时前AI 评分34
自主 AI 智能体在证明形式化中系统性偏离人类偏好
Autonomous AI Agents Systematically Diverge From Human Preferences in Proof Formalization
AI 导读
研究提出"模拟协作"方法，基于 Lean 中 9 项人类协作、超 6K 次提交和 4.7M 条定义，对比 AI 智能体与人类在证明构建中的偏好差异。结果显示 AI 智能体更倾向聚焦显式标记的缺口，相对回避高连接度的证明核心与复杂或意外的证明目标，却偏好意外的证明体并倾向将其规整至基线。
正文 · AI 翻译
摘要：人工智能（AI）系统开启了一个证明充裕的新时代，但帮助人类理解这些证明需要重新关注 AI 智能体与人类在开展证明构建任务时的差异。我们提出“模拟协作”方法，借此考察两个关键问题：（1）AI 智能体对表层语法、或反过来说对更深层语义的相对关注程度；（2）AI 智能体对下一步做什么的偏好与人类偏好如何以及在哪里出现分歧。基于 Lean 中九项重要的人类协作，涵盖超过 6K 次提交中的 4.7M 个定义，我们发现，在证明构建过程中，AI 智能体（1）比人类更强烈地被显式标记的缺口所吸引；（2）对连接密集的证明中心以及复杂或出人意料的证明目标表现出相对回避；（3）相对更被出人意料的证明主体所吸引，并倾向于将其规整至基线。我们的结果凸显了未来数学领域人机协作的重要盲点与潜在干预措施。
| 学科： | 人工智能（cs.AI）；人机交互（cs.HC） |
| 引用为： | arXiv:2611.06995 [cs.AI] |
| （或本版本的 arXiv:2611.06995v1 [cs.AI]） | |
| https://doi.org/10.48550/arXiv.2611.06995 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Bálint Gyevnár [查看邮箱]
[v1]
2026年11月4日星期三 18:34:25 UTC（388 KB）
来源：arXiv cs.AI · arxiv.org