面向数学发现的智能体神经符号协作：组合设计的案例研究

我们通过神经符号推理的视角研究数学发现：由大语言模型（LLM）驱动的AI智能体，与符号计算工具及人类战略指导相结合，共同产出了组合设计理论中的一个新结果。这一人类-AI协作的主要成果，是针对公认的困难情形 $n \equiv 1 \pmod{3}$ 给出了拉丁方不平衡度的紧下界。我们从跨越数天、多次会话的详细交互日志中重构了这一发现过程，并识别出各组成部分各自不同的认知贡献。AI智能体被证明在发掘隐藏结构与生成猜想方面颇为有效。符号部分由计算机代数、约束求解器与模拟退火组成，提供严格验证与穷举枚举。人类引导提供了关键的研究转向，将一条死路转化为富有成效的探究。我们的分析显示，前沿LLM之间的多模型商议在批评与错误检测方面可靠，但在建设性论断方面并不可靠。这一人类-AI数学贡献——$4n(n{-}1)/9$ 的紧下界——是通过一类新颖的近完美置换实现的。该下界已在Lean 4中获得形式化验证。我们的实验表明，神经符号系统确实能够在纯数学中产生真正的发现。