Agentic Neurosymbolic Collaboration for Mathematical Discovery: A Case Study in Combinatorial Design

我们从神经符号推理的视角研究了数学发现，其中由大型语言模型（LLM）驱动的AI代理与符号计算工具及人类战略导向共同完成了组合设计理论中的一个新结果。本次人机协作的主要结果是对Latin方块不平衡性给出一个紧下界，针对这个著称为难题的情形 $n \equiv 1 \pmod{3}$。我们从详细的交互日志（跨越数天数多个会话）重建了发现过程，并识别出每个组成部分的独特认知贡献。AI代理在揭示隐藏结构和生成假设方面效果良好。符号组件包括计算机代数、约束求解器和模拟退火，提供严谨的验证和穷举枚举。人类引导提供了将死胡转为富有成效的探究的关键研究转折点。我们的分析表明，前沿LLM之间的多模型 deliberation 在批评和错误检测方面可靠，但在建设性声明方面不可靠。所得的人机数学贡献——一个为 $4n(n{-}1)/9$ 的紧下界——通过一种新型的近完美置换实现。该下界在Lean 4中得到形式化验证。我们的实验表明，神经符号系统确实可以在纯数学中产生真正的发现。