一、研究背景与问题1.1 核心问题在算法博弈论中近似纳什均衡ANE的多项式时间算法设计是一个长期悬而未决的开放问题。核心挑战在于所有已知的精确纳什均衡算法如 Lemke-Howson需要指数时间PPAD-完全性结果证实了精确计算的固有困难确定在多项式时间内能达到的最佳近似保证是领域的基本问题之一1.2 研究进展与瓶颈时间双人博弈最佳保证突破20060.75KPS算法20060.5DMP算法20070.3393δTsaknakis-Spirakis算法停滞15年——20221/3δDeligkas-Fasoulakis-Markakis多玩家博弈进展更为有限唯一已知方法是扩展技术将r人算法递归提升到r1人但保证值迅速恶化——三人为0.6δ四人约0.71δ随玩家数增长趋近于1。1.3 研究契机大型语言模型能够大规模生成候选算法但需要一个自动化的验证系统来证明算法对所有博弈实例的最坏情况保证——此前该领域不存在这样的系统。二、LegoNE框架核心贡献2.1 框架定位LegoNE是一个领域特定的形式化系统能够用符号语言编写ANE算法自动证明算法的最坏情况近似保证与LLM集成形成提出→验证→改进的自动化发现循环2.2 两大核心原则1实例化Instantiation将全称量词∀策略仅实例化为算法实际构造的有限策略集将无限问题转化为有限约束。示例对于k BestResponse1(j)其逻辑属性为 ∀s₁, u₁(s₁,j)≤u₁(k,j)。分析器只将其实例化为算法中出现的具体策略如i、k、r₁得到有限不等式集。2遗忘Forgetting将每个支付项如u₁(i,j)抽象为独立的实变量如a₁遗忘其函数结构将问题转化为纯代数系统。2.3 技术流程算法代码 → Floyd-Hoare逻辑编码 → 实例化(有限约束) → 遗忘(实变量) → 约束优化问题 → 求解器(Mathematica) → 最优ε保证最终形成一个固定规模的优化问题变量数量不随博弈规模增长。2.4 框架验证用LegoNE实现了文献中所有主要ANE算法计算结果与原始论文精确匹配精度10⁻⁵而每个算法仅需约50行代码、80秒内完成分析——此前需要人类研究者数年的累积工作。三、LLM驱动的算法发现3.1 人机协作范式角色职责人类专家提供高层构建模块BestResponse、StationaryPoint等编码领域知识LLM探索构建模块的组合空间生成候选算法LegoNE分析器自动计算近似保证作为定量反馈指导LLM迭代改进3.2 关键技术细节构建模块BestResponse、Random、StationaryPoint、ZeroSumNE、EqMix、OptimalMixing等LLM模型DeepSeek-R1推理模型温度0.8工程优化编译器自动应用最优混合作为最后一步降低LLM负担搜索约束必须包含StationaryPoint所有竞争性算法共同点每个玩家最多3个策略3.3 重要说明专家知识未偏导结果专家提供的构建模块不包含任何算法结构或组合顺序的建议使用或避免扩展技术的提示任何混合系数或目标ε值算法设计的示例仅格式示例实证证据12轮产生的7个不同三人算法中仅第1个使用扩展技术其余6个独立探索了非扩展结构。四、主要发现与成果4.1 成果一复现双人博弈最佳保证设置仅提供2007年以前可用的构建模块结果2轮交互后LLM构造出与DFM算法2022年相同的1/3δ保证意义这一结果人类专家耗时15年才实现4.2 成果二三人博弈突破核心贡献指标之前最佳LegoNE发现近似保证0.6δ0.5δ设计范式扩展技术非扩展结构发现轮数—11轮4.3 三人成果的深远意义数学证明扩展技术满足 ε₃ 1/(2−ε₂)。要达到 ε₃≤0.5需要 ε₂0——即精确纳什均衡这是PPAD-难的。因此所发现的算法✅ 在可证明上超越了扩展技术的能力范围✅ 首次证明有效的多玩家ANE算法存在于扩展范式之外✅ 开辟了全新的算法设计空间结构差异扩展技术BestResponse → Mix简单两步发现算法BestResponse、EqMix、OptimalMixing的复杂交织组合五、框架通用性验证LegoNE的核心原则不仅限于ANE已成功扩展到5.1 Polymatrix博弈处理任意数量玩家的图博弈通过遗忘抽象掉玩家索引统一分析证明了已知算法(1/2δ)保证5.2 顶点覆盖问题的LP舍入算法将LP松弛舍入过程编码到框架自动证明2-近似比与已知最优一致这表明框架可推广到其他通用保证可化为有限代数系统的问题。六、与现有工作的对比维度AlphaGeometryFunSearchLegoNE评估器预先存在(DDAR)简单可构造本工作构建反馈类型二元(证明/未证明)经验指标定量最坏情况保证ε验证对象静态几何命题特定实例运行无限博弈族上的程序保证推理方法演绎引擎执行Floyd-Hoare 实例化遗忘七、局限性与未来方向当前局限依赖人工策划的构建模块编码了现有文献的证明策略无法发现根本不同的证明技术适用边界未明确仅适用于通用保证可化为有限代数系统的问题不支持分支操作编译器当前限制但可通过对称性绕开未来方向开发更富表达力的语言允许从第一原理分析算法减少对人工策划模块的依赖拓宽自动化分析的问题范围八、总结性评价这项工作的核心贡献是为ANE算法分析构建了一个此前不存在的自动化形式化系统其意义在于理论层面首次证明非扩展范式的多玩家ANE算法存在开辟新研究路径方法层面实例化遗忘的编译原则可推广到更广的算法分析问题实践层面LLMLegoNE的发现循环显著加速了理论探索——将15年人类工作压缩到2轮迭代这项工作展示了将领域证明策略编码为机器可处理语言如何支持超越已知人类设计范式的算法发现。这里是自己的论文阅读记录感兴趣的话可以参考一下如果需要阅读原文的话可以看这里如下所示摘要设计具有可证明的最坏情况保证的近似纳什均衡ANE的多项式时间算法是算法博弈论中的一个基本开放问题。虽然大型语言模型LLM能够大规模生成候选算法但验证其最坏情况保证需要对所有博弈实例进行形式化分析——而此前并不存在能够自动完成这项任务的系统。在此我们提出了 LegoNE一个将专家证明策略编码为符号语言的框架该框架能够自动将任何候选算法编译成一个有限优化问题以验证其最坏情况保证。将 LegoNE 与推理型 LLM 集成后我们重新发现了一种与双人博弈最佳多项式时间保证相匹配的算法并发现了一种三人博弈算法将其最佳保证从 0.6δ 提升至 0.5δ——这在可证明上超出了扩展技术此前唯一已知的多玩家 ANE 设计范式的能力范围。这些结果表明将特定领域的证明策略编码为机器可处理的语言能够支持 LLM 驱动的、超越已知人类设计范式的算法发现。引言纳什均衡NE由 Nash 于 1951 年提出 [1]是博弈论中基础性的解概念。然而计算 NE 已被证明是一个持续的挑战所有已知算法如经典的 Lemke-Howson 方法 [2]都需要指数时间而著名的 PPAD-完全性结果 [3, 4] 证实了这种困难是固有的。近似纳什均衡ANE的研究应运而生Lipton、Markakis 和 Mehta [5] 表明对于任何常数 ϵϵ-ANE 可以在拟多项式时间内计算这是首个次指数算法Babichenko、Barman 和 Peretz [6] 进一步将算法对玩家数量的依赖从多项式降低为对数。大型语言模型LLM为加速算法探索提供了一条途径它们能够以超越人类研究者的速度生成大量候选算法。近年来将 LLM 与自动评估器相结合已在多个科学领域取得进展从几何定理证明 [17, 18] 到矩阵乘法 [19] 和组合优化 [20] 的算法发现。然而将这一范式应用于 ANE 算法设计需要一个能够验证最坏情况性能保证的自动评估器——即证明候选算法对于每一个可能的博弈实例都能产生有效的近似均衡。这种自动评估需要特定领域的形式化工具对于欧几里得几何机械化演绎系统已存在数十年 [21, 22]而对于 ANE 算法分析此前不存在可比较的自动化系统证明依赖于逐个论文的临时性数学论证。在此我们提出了 LegoNE一个特定领域的框架使得 ANE 算法的这种验证成为可能。LegoNE 提供了一种符号语言将二十年 ANE 研究中的专家证明策略转化为可组合的构建模块并提供了一个自动分析器可将用该语言编写的任何候选算法编译成一个有限优化问题其最优值验证了算法的最坏情况保证。该编译基于两个原则——实例化将全称量词简化为有限的具体约束集和遗忘将支付函数抽象为符号实变量——共同将无限维的证明义务简化为可由现成求解器解决的固定规模数学规划问题。与推理型 LLM 结合LegoNE 实现了一个自动化发现循环LLM 通过组合构建模块提出候选算法分析器计算出一个可证明正确的近似保证并将其作为定量反馈返回LLM 则迭代改进设计。这两个组件是互补的LLM 提供大规模探索LegoNE 提供严格、定量的评估。利用这一框架我们展示了两个主要结果。首先LLM-LegoNE 系统在两次迭代内重新发现了一个与双人博弈已知最佳保证 1/3δ 相匹配的多项式时间算法——这一结果此前人类专家从之前的最佳结果起花费了 15 年才实现。其次该系统发现了一个三人博弈算法实现了 0.5δ优于此前最佳的 0.6δ。三人博弈结果的意义超越了数值上的改进。扩展技术——此前唯一已知的多玩家 ANE 设计范式——满足 ϵ31/(2−ϵ2) [15, 16]其中 ϵ2 是双人保证。要通过扩展实现 ϵ3≤0.5则需要 ϵ20——即精确纳什均衡这是 PPAD-难的。因此所发现的算法实现了一个可证明超出扩展技术在多项式时间内所能达到的保证据我们所知这确立了有效的多玩家 ANE 算法存在于扩展范式之外。这些结果说明了将领域的证明策略编码为机器可处理的形式语言如何支持 LLM 驱动的算法发现。高层方法——LLM 提出候选自动评估器提供反馈——与先前的 AI 科学发现系统 [17, 20, 19] 相同我们的贡献在于评估器本身这是一个此前在该领域不存在的、用于自动最坏情况分析的形式化系统。虽然 LegoNE 目前特定于 ANE但对顶点覆盖近似和 polymatrix 博弈的初步扩展见附录表明底层的编译技术可能适用于其他算法分析问题在这些问题中通用保证可以简化为有限的代数不等式系统。LegoNE 框架LegoNE 是一个用于规范并自动验证 ϵ-近似纳什均衡ANE[23] 算法的框架。ϵ-ANE 是一种接近稳定的策略组合其中任何玩家的后悔值不超过 ϵ即没有玩家能通过单方面偏离使收益提高超过 ϵ。算法保证的最坏情况 ϵ 越小其性能保证越好。LegoNE 提供 (i) 一种专门的符号语言用于从高层构建模块组合 ANE 算法以及 (ii) 一个自动分析器可将任何此类程序编译成一个有限优化问题其解可验证算法的性能保证。算法设计语言。LegoNE 语言是一种专门设计的、类似 Python 的语言用于为固定玩家数量的博弈指定 ANE 算法。它基于一套紧凑的、源自过去二十年已建立的博弈论研究的预定义构建模块。这些模块代表了高层策略概念例如计算最优反制策略BestResponse或混合现有策略UniformMixing。这种模块化方法简化了算法设计。例如Daskalakis-Mehta-PapadimitriouDMP算法 [13] 可以通过组合这些模块图1仅用几行代码表示。LegoNE 语言在其领域内具有很强的表达能力能够描述文献中各种各样的构建模块从解决线性规划到梯度下降。此外它支持通过任意组合这些模块来表达复杂算法从而允许创建新的算法。这种抽象通过编程语言创建了一个结构化的设计空间。在此背景下LLM 可以学习通过组合这些已建立的概念来探索算法而不是从头推理。num_players 2 def Random1() - p1: description 针对玩家1的随机策略 x1 constraints [] return x1 def BestResponse1(s2: p2) - p1: description 针对玩家2的策略 s2玩家1的最佳反应 x1 constraints [ forall(s1).(U1(s1,s2)U1(x1,s2)) ] return x1 def BestResponse2(s1: p1) - p2: ... def UniformMix1(s1: p1, s2: p1) - p1: ... def algo(): i: p1 Random1() j: p2 BestResponse2(i) k: p1 BestResponse1(j) r1: p1 UniformMix1(i, k) return r1, j图1: DMP算法的LegoNE代码。该语言使用简单、高层的构建模块封装了核心博弈论概念。这里我们定义了构建模块 BestResponse1用于计算玩家1p1针对玩家2p2的策略 s2 的最佳反应 x1Random1用于为玩家1p1随机生成一个策略等等。然后我们定义 DMP 算法它组合了这些模块并最终返回两个玩家的策略组合 r1, r2。自动分析器从代码到证明。LegoNE 的一个关键组件是其自动分析器它将算法分析转化为系统化的机器驱动过程。对于用 LegoNE 语言表达的任何算法分析器计算其最佳可能的近似保证 ϵϵ并同时生成该保证的计算机证明。这通过一个两步抽象实现将原始的无限维问题即为所有可能的博弈陈述一个保证简化为一个有限的、可求解的数学规划问题。此过程的概述如图2所示。该过程首先基于 Floyd-Hoare 语义 [24, 25] 将算法的过程代码翻译为一组声明性的逻辑属性。在此过程中代码的每一行都被编码为一个数学语句。例如指令图2: LegoNE 分析器过程。** a 分析器读取所有构建模块这些模块描述了它们的数学属性。 b 分析器然后读取由这些构建模块组成的算法代码。 c 分析器将算法代码翻译成算法属性和近似分析证明目标的逻辑编码。 d 分析器为算法构造的有限策略集实例化逻辑属性。 e 分析器然后“遗忘”支付函数的底层结构并将属性编码为关于实变量 \(a_1, a_2, a_3, \ldots\) 的有限代数不等式集。 f 最后分析器公式化一个约束优化问题以在满足这些不等式的前提下找到最紧的 \(\epsilon\)并使用外部求解器如 Mathematica求解。通过这两步过程最初关于无限维函数的断言被转换成一个关于一组实变量的有限代数不等式系统。该系统随后被公式化为一个约束优化问题在导出不等式系统的约束下寻找最小可能的 ϵϵ——ϵϵ 也使用这些新变量表示。由外部求解器找到的最优值即是最紧的可能最坏情况近似保证 ϵϵ。该优化问题的解构成了算法性能保证的构造性证明。在 LegoNE 框架内计算保证等同于证明它。实证验证。为了验证 LegoNE 分析器的正确性我们用 LegoNE 语言实现了文献中所有已知的、针对固定玩家数量博弈的多项式时间 ANE 算法。这包括了二十多年来发表的一系列工作。ANE 算法的文献几乎完全集中在双人博弈上。对于多于两名玩家的博弈唯一已建立的设计范式是扩展双人算法。我们也实现了从该范式导出的三人算法。结果如表1所示。对于每个算法LegoNE 分析器计算出的近似保证与原始论文中的结果匹配精度达到 10−5。这些算法的原始证明需要几页到十几页的数学论证。在 LegoNE 中每个算法的代码表达都在 60 行以内。所有算法的近似保证自动计算都在 80 秒内完成而此前这需要人类研究者数年的累积研究。这些结果证实了框架的正确性并展示了其通过高效识别正确的近似保证来加速理论研究的潜力。详细实验结果见表2。扩展框架。框架的核心原则实例化和遗忘超出了固定玩家数量博弈的分析范围。我们已将框架应用于分析两类更广泛问题的算法展示了其通用性。详见附录。首先我们分析了 polymatrix 博弈 [28] 中的近似纳什均衡算法。与固定玩家数量的标准博弈不同polymatrix 博弈模拟大型网络中的交互其中每个玩家的收益仅由给定图中其邻居决定。挑战在于推理任意数量的玩家。我们将框架应用于文献中唯一的 polymatrix 博弈多项式时间 ANE 算法。我们的框架通过使用遗忘原则抽象掉玩家特定的索引来处理分析从而允许进行统一分析自动证明算法的近似保证。其次我们将框架扩展以分析基于线性规划LP松弛和舍入 [8] 的一大类近似算法。作为这种方法的经典示例我们分析了顶点覆盖问题的算法这是计算机科学中的一个基本挑战。分析涉及将算法——即求解松弛问题并对解进行舍入——翻译到我们的框架中。然后分析器自动证明了算法具有 2 的近似比与文献中已知结果匹配。这些应用表明该框架有潜力成为跨更广泛计算问题的通用自动算法分析工具。表1: LegoNE 对现有算法的基准测试。该表总结了 LegoNE 为每个算法证明的近似保证并与原始论文中证明的保证进行了比较。结果精确匹配展示了框架在自动化算法分析方面的正确性和有效性。本文中δ0 表示近似保证中使用的任意小常数保证对任何固定的 δ 成立运行时间关于 1/δ 为多项式。作者首字母年份原始论文证明的保证LegoNE 证明的保证KPS [12], 20060.750.75000DMP [13], 20060.50.50000DMP [26], 20060.38197 δ0.38197 δBBM-1 [15], 20070.381970.38197CDFFS [27], 20160.381970.38197BBM-2 [15], 20070.363920.36392TS [14], 20070.33933 δ0.33933 δDFM [9], 20221/3 δ0.33333 δDFM扩展 (3人) [9, 15, 16], 20220.6 δ0.60000 δ表2: LegoNE 对现有算法的详细基准测试。该表显示了每个算法的代码行数和运行时间。代码行数包括定义所有使用的构建模块、固有约束和算法定义。LegoNE 计算的保证也列出以供参考。作者首字母年份LegoNE 证明的保证代码行数运行时间 (秒)KPS [12], 20060.750002722.55DMP [13], 20060.50000424.31DMP [26], 20060.38197 δ3831.13BBM-1 [15], 20070.381974611.81CDFFS [27], 20160.381974865.87BBM-2 [15], 20070.36392—1.38TS [14], 20070.33933 δ3113.90DFM [9], 20220.33333 δ5279.63DFM扩展 (3人) [9, 15, 16], 20220.60000 δ508.34图3: 算法发现的人机协作循环。人类专家提供高层构建模块和设计指导。然后 LLM 通过组合这些模块提出候选算法。LegoNE 分析器自动计算一个已证明的近似保证并将其作为反馈返回如果算法存在语法错误分析器将向 LLM 输出具体的错误信息。该循环迭代进行允许 LLM 基于严格的理论反馈改进其设计。方法的经典示例我们分析了顶点覆盖问题的算法这是计算机科学中的一个基本挑战。分析涉及将算法——即求解松弛问题并对解进行舍入——翻译到我们的框架中。然后分析器自动证明了算法具有 2 的近似比与文献中已知结果匹配。这些应用表明该框架有潜力成为跨更广泛计算问题的通用自动算法分析工具。LLM 驱动的算法发现我们进一步将 LegoNE 与 LLM 集成以实现算法发现的自动化图3。在这一范式中人类专家和 LLM 基于各自互补的优势扮演不同角色。人类专家提供算法设计的基本组件将领域特定知识和高层证明策略翻译成 LegoNE 语言的构建模块。这项任务需要 LLM 目前尚无法达到的概念理解水平。而 LLM 则负责导航如何组合这些模块的庞大组合空间以人类研究者难以企及的规模和速度探索潜在算法。此框架中的学习过程之所以有效有两个原因。首先构建模块提供了设计空间的高层规范使其对 LLM 来说是可处理的。其次LegoNE 分析器通过为任何提议的算法计算一个可证明正确的近似保证来提供快速、严格的反馈。这种提出、验证和改进的迭代过程使得算法设计空间的高效探索成为可能。一个交互控制器管理此过程使用由人类专家设计经验和洞见精心设计的提示引导 LLM 走向设计空间中有前景的区域同时仍鼓励生成多样化的解决方案。重要的是此反馈并非基于特定博弈实例进行评估分析器返回的近似保证对所有博弈实例均成立。复现最佳多项式时间最坏情况保证。为了验证该框架我们首先让其重新发现 ANE 研究中的一个已知结果。在一个为双人博弈配置的实验中一个推理型 LLM [29] 仅被提供了 2007 年之前文献中可用的构建模块当时 [14] 获得了当时最佳的多项式时间最坏情况保证。在与 LegoNE 分析器交互 2 轮后LLM 构建了一个算法。尽管其结构与 2022 年实现当前最佳多项式时间最坏情况保证 [9] 的改进算法不同但 LegoNE 证明它达到了相同的近似保证。这一结果人类专家需要 15 年累积研究才实现表明该框架有潜力加速理论思想的生成和验证过程。发现多玩家算法。我们将该框架应用于三人博弈这是一个人类设计方法进展有限的领域。先前的工作通常依赖于一种扩展技术来改编双人算法 [15, 16]这种方法具有局限性且通常产生较弱的保证。图4 说明了三人博弈多项式时间基线即在我们工作之前通过将扩展技术应用于 DFM 算法 [9] 构建的、实现了最佳多项式时间最坏情况保证的算法。在 12 轮中LLM 生成了 7 个不同的算法只有第一个依赖于扩展技术其余 6 个探索了替代的非扩展结构尽管如此它们仍获得了非平凡的保证。提供给 LLM 的专家知识包括构建模块本身来自 ANE 文献的标准博弈论操作如 BestResponse、StationaryPoint 和 OptimalMixing以及定义搜索空间的提示级约束——但不包括算法结构、组合顺序或混合系数。在这些运行中扩展技术作为一个可能的组件是可用的然而 LLM 生成了非扩展方法。最终 0.5δ 算法的结构并未被设计这些构建模块的人类专家所预见。专家输入的详细清单见方法B.1节。def algo(): z: p3 Random3() x: p1, y: p2 DFM(z) z_br: p3 BestResponse3(x, y) z_mix: p3 0.6 * z 0.4 * z_br return x, y, z_mix图5: 由LLM发现的三人ANE算法。讨论这项工作提出了 LegoNE一个特定领域的形式化系统用于自动化近似纳什均衡算法的分析并展示了其与 LLM 的集成以形成一个自动发现循环。LegoNE 分析器——建立在实例化和遗忘原则之上——将用 LegoNE 语言表达的任何候选算法编译成一个有限优化问题其解可验证算法的最坏情况保证。与推理型 LLM 结合该循环在两次迭代内复现了双人博弈的最佳多项式时间最坏情况保证并发现了一个三人算法将其最佳保证从 0.6δ 提升至 0.5δ。三人博弈结果的意义超越了特定的近似常数。扩展技术 [15, 16]——此前唯一已知的设计多玩家 ANE 算法的范式——满足 ϵ31/(2−ϵ2)要通过扩展实现 ϵ3≤0.5则需要一个精确纳什均衡算法这是一项 PPAD-难的任务。因此据我们所知所发现的算法确立了有效的多项式时间多玩家 ANE 算法存在于扩展范式之外。这为多玩家算法开辟了一个设计空间并有助于缩小已知最佳多项式时间保证与硬度下界之间的差距——对于双人及多玩家设置这个差距仍然很大且在很大程度上未被刻画。我们的进展应被理解为既是一个积极的结果也是一个边界标记。LegoNE 目前依赖于人工策划的构建模块这些模块编码了现有文献中的证明策略它无法发现根本不同的证明技术。该框架的范围限于实例化和遗忘原则适用的算法分析问题——即通用保证可以简化为有限代数不等式系统的设置。我们对顶点覆盖近似和 polymatrix 博弈的初步扩展见附录表明这一类别是非平凡的但其确切边界仍有待刻画。展望未来我们希望开发更具表达力的语言允许方法LegoNE 框架详解背景近似纳什均衡 (ANE)LegoNE 语言LegoNE 框架引入了一种领域特定编程语言它将描述算法的执行步骤其操作语义 [31]转变为指定其数学属性其公理语义 [24, 25]的范式。这种方法受 Floyd-Hoare 逻辑 [24, 25] 启发促进了一种人机协作其中人类设计者将其关于算法组件的洞见编码为逻辑公式机器随后将其用作进一步分析的公理。一个算法首先通过定义基本的构建模块然后顺序组合它们来构建。考虑双人博弈的 Daskalakis-Mehta-PapadimitriouDMP算法 [13]。其构建模块包括如 BestResponse找到对抗对手的最优策略例如 jBestResponse(i) 和 UniformMixing创建两个策略的等概率混合例如 r1UniformMixing(i,k) 等操作。尽管这些示例很简单但 LegoNE 语言在其领域内具有很强的表达能力能够描述文献中各种各样的构建模块从求解线性规划到梯度下降。LegoNE 分析器形式化分析 ANE 算法的核心挑战在于处理无界维度的对象。算法的近似保证必须对任何博弈都成立。这意味着它必须对任意大小的支付矩阵以及单纯形内相应混合策略的无限连续统都有效。证明目标的这种全称量化性质使得直接计算验证不可行。为了克服这一基本障碍LegoNE 分析器引入了一个两步过程系统地将抽象的、无限维的证明任务转化为一个具体的、固定大小的约束优化问题。此过程的灵感来自人类专家构建证明的方式将算法的属性与实算术的通用属性分离开来。我们自动分析的核心依赖于两个原则实例化和遗忘。这个固定大小优化问题的最优值正是可通过此证明策略为给定算法推导出的最佳近似保证。至关重要的是一旦策略固定该优化问题的变量和约束数量也是固定的不会随博弈实例的大小而扩展。这最终是一个固定规模的程序可以通过现成的数值求解器如 Gurobi [32] 或 Mathematica [33]求解。在现有类人设计算法上基准测试 LegoNE为了验证 LegoNE 框架的正确性和分析能力我们将其与文献中现有的类人设计 ANE 算法进行了基准测试。该框架的编译器使用 C 实现并采用词法分析器 Flex [34] 和语法分析器 Bison [35]Mathematica 作为外部优化求解器。Mathematica 内部使用的是 Wolfram Engine版本 14.2。我们将 Mathematica 参数设置如下AccuracyGoal 设为 10WorkingPrecision 设为 20MaxIterations 设为 2000。我们使用默认方法自动作为优化方法。为了确保结果可重现我们在 MacBook 和 Windows PC 上重新运行了相同的优化。为了测试运行时间我们使用了 MacBook Pro 14M4 芯片10核CPU/10核GPU16GB RAM。每个优化在相同条件下执行 5 次。大多数现有的多项式时间 ANE 算法是为双人博弈设计的。我们用 LegoNE 语言编码了文献中的所有主要算法包括像 Tsaknakis-Spirakis 算法这样的复杂算法。这一过程展示了 LegoNE 表达复杂算法组件的能力例如分支操作、具有支付依赖系数的混合策略以及复杂的 StationaryPoint 构建块。出于计算效率考虑并由于当前 LegoNE 编译器的限制我们对某些算法设置了特殊参数。LegoNE 编译器目前不支持分支操作然而由于算法的对称性编码一个分支就足够了。对于具有 0.36 近似保证的 BBM-1 [15]LegoNE 编译器目前不支持平方根操作因此我们手动计算了编译器输出。对于具有 0.75 近似保证的 KPS [12] 和具有 0.38 近似保证的 DMP [26]我们手动提供了最优混合操作的对角线逻辑编码见关于双人博弈最优混合的附录说明以遵循原始证明。自动化算法发现的实验细节人机交互循环与工程考量我们的自动化发现过程围绕大型语言模型LLM与 LegoNE 框架之间的迭代交互循环展开。这种方法建立在人机协作范式之上即人类建立高层理论框架机器在其中探索广阔的算法设计空间。该过程将基础构建模块的定义与将它们组合成完整算法的任务分离开来。定义额外的构建模块需要深厚的领域专业知识和复杂的数学推导这是为人类专家保留的角色。相比之下组合这些预定义模块的任务则更具结构性更适合由 LLM 自动化。这种自动化之所以可行有两个关键因素通过使用封装了人类洞见的复杂预定义模块设计空间被显著压缩并且 LegoNE 编译器通过自动计算任何有效组合的近似保证来提供即时反馈。为了使这一探索过程高效且鲁棒我们实施了若干工程选择带最优混合的自动返回在 ANE 算法的文献中一个特别复杂的步骤是确定适当的系数来混合构造的策略以实现较小的近似保证。这对 LLM 来说是一项具有挑战性的任务。为简化任务我们修改了 LegoNE 编译器使其自动将最优混合操作作为任何给定算法片段的最后一步应用。这一增强使得 LLM 能够专注于构建有效策略而编译器负责处理混合。提示工程我们设计了一个多阶段提示策略来引导 LLM。初始提示第一个提示为 LLM 提供了清晰且受约束的起点。它包括(1) 任务的清晰描述主要目标是最小化近似保证 ϵ(2) 严格的设计约束例如强制使用静态单赋值SSA、类型注解、禁止 return 语句以及根据人类专家经验证明其有效性必须至少包含一个 StationaryPoint 构建块(3) 有效和无效代码片段的具体示例以帮助 LLM 理解预期格式和约束。迭代反馈提示后续提示根据 LLM 之前的输出动态调整。如果之前的算法无效新提示将包含详细的编译器错误信息突出显示诸如类型不匹配、构建块使用不正确或违反 SSA 规则等具体问题。然后指示 LLM 仔细审查并纠正这些错误。如果算法有效提示则侧重于优化。它提供当前最佳的近似保证 ϵϵ并鼓励 LLM 实现更小的值。具体来说提示引导 LLM利用更复杂的构建块通过对不同玩家应用不同的模块来打破对称性探索替代组合以避免局部最优并遵循奥卡姆剃刀原则倾向于选择能实现相当或更好结果的更简单策略。专家知识清单为了能够评估专家提供的知识是否可能使 LLM 偏向于所发现的解决方案我们提供了所有专家输入的详细说明。提供给 LLM 的构建块编码了来自 ANE 文献的标准博弈论操作BestResponse计算对手策略的最优反应基本博弈论概念- Random生成任意策略平凡- StationaryPoint计算最大后悔函数及其对偶的近似驻点返回四个策略 [14]ZeroSumNE通过线性规划计算零和博弈的精确纳什均衡教科书内容 2. EqMix两个策略的等概率混合平凡 3. MaxPayoff最大化给定支付函数平凡。这些构建块定义了哪些操作可用但并未规定如何组合它们——组合完全由 LLM 决定。提示级约束分为三类结构约束限制搜索空间每个玩家最多 3 个策略运行时强制执行、静态单赋值SSA、需要类型注解。启发式指导非限制性奥卡姆剃刀偏好更少策略、鼓励打破玩家间的对称性、惩罚重复算法。领域特定约束LLM 必须至少包含一个 StationaryPoint 构建块。此约束反映了领域知识即自 Tsaknakis 和 Spirakis [14] 以来所有有竞争力的多项式时间 ANE 算法都依赖于驻点计算没有它的算法例如 KPS [12] DMP [13]最多只能达到 ϵ0.5。此约束排除了已知的次优方向但并未指定如何组合 StationaryPoint 返回的策略——后者是 LLM 必须确定的创造性部分。至关重要的是专家输入不包括任何关于整体算法结构或组合顺序的建议- 任何使用或避免扩展技术的提示- 任何混合系数或支付依赖权重的指定- 任何目标 ϵϵ 值- 任何算法设计的少样本示例提供的代码示例仅说明预期格式而非算法策略。结果提供了实证证据表明专家输入并未使 LLM 偏向于所发现的解决方案在 12 轮中产生的 7 个不同的三人算法中只有第一个使用了扩展技术其余 6 个独立探索了非扩展结构。最终的 0.5δ 算法以人类专家设计构建块时未曾预料到的模式组合了 BestResponse、EqMix 和 OptimalMixing。用于鲁棒探索的流程管理为了防止冗余探索我们维护了所有先前生成算法的记录。如果 LLM 提出重复算法它会被告知并显示过去尝试的记录。如果重复持续超过一定阈值则重新开始交互以鼓励新的探索方向。同样为防止 LLM 在长对话历史中遗忘指令当聊天历史超过一定长度时我们会重新开始交互。最后为了确保 LegoNE 的及时分析我们设置了代码行数和构造策略数的限制提示 LLM 简化其生成的任何过于复杂的算法。在我们的实验中我们使用了 DeepSeek-R1-250120缩写为 R1[29]一个推理型 LLM。我们将温度设置为 0.8以允许 LLM 响应有一定变化。我们为 LLM 提供了一组源自现有类人设计算法的构建模块。对于 LegoNE 分析器我们使用与上述基准测试小节相同的环境。对于双人情况我们将 Mathematica 参数设置如下AccuracyGoal 设为 6MaxIterations 设为 5000。对于三人情况由于计算更困难我们将 AccuracyGoal 设为 40WorkingPrecision 设为 60MaxIterations 设为 2000。对于这两种情况我们都使用默认方法自动作为优化方法。作为可重现性检查我们在 Windows 个人电脑PC上运行完整流程然后在 MacBook 上手动验证 LegoNE 分析器的输出。双人博弈实验在双人博弈设置中R1 在 2 轮内复现了最佳多项式时间最坏情况保证但算法与文献不同。这为人类设计文献中先前保证与当前保证之间 15 年的差距提供了一个具体对比。我们也使用 DeepSeek-V3-241226缩写为 V3模型 [36] 进行了测试。同样我们将温度设置为 0.8并使用相同的构建块要求。在更广泛的 100 轮测试中V3 没有超越最佳多项式时间最坏情况保证但确实发现了几种文献中未出现的组合。三人博弈实验在更具挑战性的三人博弈领域R1 在 11 轮中发现了一个具有可证明近似保证为 (0.5δ) 的算法。这改进了此前人类设计的最佳多项式时间最坏情况保证 0.6δ。此外R1 在 12 轮内发现了另外六个保证范围在 0.5δ 到 0.8δ 之间的算法。除了第一个之外所有这些被发现的算法都没有使用图4所示的扩展技术而该技术此前是人类专家设计具有非平凡优于1保证的三人 ANE 算法的唯一已知方法。这些结构上不同的算法表明自动化过程可以探索扩展范式之外的设计空间部分。表现最佳的发现算法如图5所示。扩展技术构造以最佳响应后混合步骤结束相比之下发现的算法依赖于构建块更复杂的组合以非平凡的方式交织了 BestResponse、EqMix 和 OptimalMixing。相关工作纳什均衡的计算复杂性。纳什均衡 [1, 30] 是非合作博弈论中的核心解概念。纳什的存在性定理纯粹是存在性的第一个算法方法Lemke-Howson 算法 [2]在最坏情况下需要指数时间并且几十年来没有找到多项式时间算法尽管当时也没有已知的难度证明。在此背景下Lipton、Markakis 和 Mehta [5] 开创了近似纳什均衡的研究证明对于任何常数 ϵϵ-ANE 可以在拟多项式时间内计算通过一个结构结果表明纳什均衡可以用对数支撑的策略很好地近似——这是该问题的首个次指数算法。随后 Daskalakis、Goldberg 和 Papadimitriou [3]针对三人或更多玩家以及 Chen 和 Deng [4]针对双人的 PPAD-完全性结果证实了计算精确纳什均衡是难以处理的为追求近似提供了理论依据。在 PPAD-完全性之后多项式时间近似算法迅速进展Kontogiannis、Panagopoulou 和 Spirakis [12] 实现了 ϵ0.75ϵ0.75Daskalakis、Mehta 和 Papadimitriou [13, 26] 将其改进到 0.5 和 0.382Bosse、Byrka 和 Markakis [15] 达到了 0.364Tsaknakis 和 Spirakis [14] 达到了 0.3393δ。然后进展停滞了 15 年。在拟多项式机制中Babichenko、Barman 和 Peretz [6] 大幅改进了多玩家博弈的支撑大小界限将对玩家数量的依赖从多项式降低为对数。Rubinstein [10] 证明了不存在 PTAS假设 PPAD 的指数时间假说排除了任意小 ϵϵ 的多项式时间算法然而相应的硬度常数不是显式的并且被认为非常小 [11]。Deligkas、Fasoulakis 和 Markakis [9] 最终以 1/3δ 的保证打破了 15 年的僵局。对于多玩家博弈扩展技术 [15, 16] 将 r 人算法提升至 (r1) 人其保证从 ϵr 降低至 1/(2−ϵr)。应用于最佳双人结果这为三人博弈产生 0.6δ随着玩家数量增长保证值趋近于 1。在此工作之前没有已知的用于多项式时间多玩家 ANE 算法的替代设计范式。用于算法发现的探索-评估管道。一条广泛的研究路线通过探索假设空间并使用机器可计算的目标评估候选方案来自动化算法开发包括程序合成 [37] 和自动化算法配置 [38]。近期的系统使用学习到的启发式方法来导航大规模的低级算法空间例如发现更快排序例程 [39] 和新矩阵乘法分解 [19] 的强化学习代理以及用于诸如整数序列程序 [40] 等结构化领域的自学习合成。这些努力通常通过经验指标运行时、操作计数、基准准确性或针对固定输入大小的正确性来评估候选方案而 LegoNE 则针对无限博弈族上的定理式最坏情况近似保证。与 AI 科学发现系统的关系。LegoNE 与 LLM 的结合共享了与近期 AI 科学发现系统如 AlphaGeometry [17, 18]、FunSearch [20] 和 AlphaEvolve [41]相同的高层探索-评估架构。在此共享范式中有三个技术差异值得注意。首先先前系统中的评估器要么是预先存在的AlphaGeometry 的演绎引擎 DDAR 可追溯到 Chou、Gao 和 Zhang 在 1990 年代的工作 [42]要么是易于构建的FunSearch 通过在特定实例上执行程序来评估程序而 LegoNE 分析器——基于实例化和遗忘编译原则——是在本工作中构建的一个形式化系统。其次虽然 AlphaGeometry 的评估器提供二元反馈找到证明或未找到但 LegoNE 分析器返回一个定量的最坏情况保证 ϵ从而在 LLM 搜索循环中实现类似梯度的优化。第三AlphaGeometry 验证静态几何命题而 LegoNE 验证过程算法的通用性能保证需要将 Floyd-Hoare 式程序推理与实例化和遗忘编译相结合。战略属性的基于样本的保证。存在一个不断增长的文献它从样本中评估算法或战略属性提供的是依赖于分布的保证而非最坏情况保证。例如泛化结果量化了在未知实例分布下学习或调整高性能算法所需的数据量 [43]以及相关技术从抽样类型或博弈轨迹估计拍卖中的近似激励兼容性或离均衡距离 [44, 45]。这些工具非常适合参考分布有意义且数据可用的场景它们补充了寻求与实例无关的近似保证的经典最坏情况分析。用于博弈求解和策略/策略生成的 LLM。近期工作研究 LLM 作为策略和策略的生成器包括使用代码生成模型进行自我对弈以改进博弈策略 [46]使用博弈论均衡求解器引导语言生成 [47]将自然语言博弈描述翻译为扩展形式表示 [48]以及用于可解释多智能体策略的代码空间响应预言机 [49]。这些路线主要针对特定博弈或交互领域中的经验行为而我们的重点是为正则形式博弈合成多项式时间算法并提供机器可检查的最坏情况保证。数据可用性本研究生成的所有数据——包括以 LegoNE 语言表达的已发现 ANE 算法、分析器计算的基准近似保证表1、2、LLM 提示src/auto_design/prompts.py以及运行时间测量——均可在 Zenodo 仓库 [50] 公开获取这些材料的重用受下文代码可用性声明中所述许可证的约束。代码可用性本研究中使用的 LegoNE 编译器和分析器、构建模块库以及 LLM 驱动发现流程的源代码已存放在 Zenodo 仓库 [50] 中。代码包含足以重现本文报告的所有实验的实现。由于正在进行的专利相关计划该仓库由作者以版权“保留所有权利”的形式发布。非商业学术用途——包括本文报告结果的重现、验证和扩展——在向通讯作者 Hanyu Lilhydavepku.edu.cn提出书面请求后可免费获得许可请求通常在两週内得到回复。该仓库将无限期保持可用。其他用途需要与作者签订单独的许可协议。
