arXiv Artificial Intelligence· B\'alint Gyevn\'ar, Simon DeDeo·· 2 天前AI 评分31
AI 智能体在证明形式化中系统性偏离人类偏好
Autonomous AI Agents Systematically Diverge From Human Preferences in Proof Formalization
AI 导读
研究提出"模拟协作"方法，在 Lean 中 9 组人类协作、超 6K 次提交和 4.7M 条定义上对比 AI 智能体与人类的证明偏好。结果显示 AI 智能体更倾向明确标记的缺口，相对回避密集连接的证明核心与复杂或意外的证明目标，却偏好意外的证明体并倾向将其规整到基线。
来源：arXiv Artificial Intelligence · arxiv.org