自主人工智能代理在证明形式化方面系统地偏离人类偏好

摘要

arXiv:2611.06995v1 Announce Type: new Abstract: Artificial intelligence (AI) systems have ushered in a new age of proof abundance, but helping humans understand these proofs requires new attention to ...

proof and new humans the agents human attention how collaboration

2026-11-06 1 阅读约1分钟阅读 B\'alint Gyevn\'ar, Simon DeDeo

arXiv:2611.06995v1 公告类型：新摘要：人工智能 (AI) 系统迎来了证明丰富的新时代，但帮助人类理解这些证明需要重新关注人工智能代理和人类执行证明任务的差异。我们提出了“模拟协作”，这种方法允许我们研究两个关键问题：（1）人工智能代理对表面语法或更深层的底层语义的相对关注，以及（2）人工智能代理对下一步行动的偏好如何以及在何处与人类偏好不同。在精益中的九个主要人类合作中，有超过 6K 次提交的 470 万个定义，我们发现，在证明构建过程中，人工智能代理 (1) 比人类更容易被明确标记的差距所吸引； (2) 对密集连接的证明中心和复杂或令人惊讶的证明目标表现出相对厌恶； (3) 对令人惊讶的证明体相对有吸引力，他们倾向于将其规范化到基线。我们的结果强调了未来人类与人工智能在数学领域合作的重要盲点和潜在干预措施。

订阅66必读