提出一种基于大语言模型的AI代理与符号计算工具及人类策略指导协同的神经符号协作框架,用于组合设计理论中的数学发现,成功获得n≡1(mod 3)情形下拉丁方不平衡度的紧下界4n(n−1)/9,并通过近完美排列实现该界,结果经Lean 4形式化验证。
机构:康奈尔
来源:arXiv 2603.08322 | AI4Papers 论文推荐平台