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 智能体更倾向聚焦显式标记的缺口，相对回避高连接度的证明核心与复杂或意外的证明目标，却偏好意外的证明体并倾向将其规整至基线。
正文 · 原文
Abstract:Artificial intelligence (AI) systems have ushered in a new age of proof abundance, but helping humans understand these proofs requires new attention to the differences in how AI agents and humans pursue a proof-making task. We present "simulated collaboration", a methodology that allows us to examine two key questions: (1) the relative attention AI agents pay to surface syntax or, conversely, deeper underlying semantics, and (2) how and where AI agent preferences for what to do next diverge from human preferences. On a set of nine major human collaborations in Lean with 4.7M definitions across more than 6K commits, we find that, over the course of proof construction, AI agents (1) are far more strongly drawn than humans to explicitly marked gaps; (2) show a relative aversion to densely connected proof centers and to complex or surprising proof goals; and (3) are relatively attracted to surprising proof bodies, which they tend to regularize toward baseline. Our results highlight important blind spots and potential interventions for future human-AI collaboration in mathematics.
| Subjects: | Artificial Intelligence (cs.AI); Human-Computer Interaction (cs.HC) |
| Cite as: | arXiv:2611.06995 [cs.AI] |
| (or arXiv:2611.06995v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2611.06995 arXiv-issued DOI via DataCite |
Submission history
From: Bálint Gyevnár [view email]
[v1]
Wed, 4 Nov 2026 18:34:25 UTC (388 KB)
来源：arXiv cs.AI · arxiv.org