计算机科学
Computer Science
人工智能
Artificial Intelligence
计算与语言
Computation and Language
计算复杂性
Computational Complexity
我们研究PDDL片段中的规划,具有定性状态轨迹约束,捕获安全要求,任务排序条件以及现实世界中常见的中间子目标。 解决这些问题的一个突出方法是将其约束性地编译掉,导致一个得到最先进的规划者支持的问题。 不幸的是,现有的编译器不会扩展大量对象和高属性操作的问题,因为它们需要在编译之前解决问题。 为了解决这个问题,我们提出了两种在不接地的情况下编纂约束的方法,使它们适合大规模的规划问题。 我们证明了编译器的正确性,并概述了它们最坏情况的时间复杂性。 此外,我们还对最新的国际规划竞赛中使用的领域进行了可重复的经验评估。 我们的结果表明,我们的方法是高效的,并且产生的规划规范比基于域的编译器产生的规划规范要简洁得多,同时在与最先进的规划师一起用于规划时保持竞争力。
SeQuant是一个开源库,用于在交换(标量)和非交换(操作器)环上符号代数的张量。 支持其大部分功能的关键创新是图形理论张量网络(TN)规范化器,可以比标准组理论对应器更快地处理对称的张量网络。 TN 规范化器用于常规的张量表达式的常规简化,用于优化 Wick's 定理的应用(用于将张量产品用于操作域的正法)以及用于操作导致数值评估的中间表示的操纵。 SeQuant的显着特征包括支持非协变张量网络(通常来自张量分解)和具有参数化模式模式的张量(自由度之间的依赖性自然被视为张量嵌套,“张量”在数据科学和现代量子模拟中产生的块状数据压缩)。 SeQuant通过包括编译器类组件来优化和直接解释外部数值张量代数框架,从而模糊了纯符号操作/代码生成和数值评估之间的界限。 SeQuant源代码可在https://github.com/ValeevGroup/SeQuant上找到。
符号回归试图通过搜索闭态表达式来从实验数据中揭示物理定律,这是AI驱动的科学发现中的一项重要任务。 然而,表达搜索空间的指数级增长使任务在计算上具有挑战性。 减少有效搜索空间和加速训练的一个有希望的但探索不足的方向在于符号等价物:许多表达式虽然在语法上不同,但定义了相同的函数 - 例如log(x_1^2x_2^3),log(x_1^2)+log(x_2^3)和2log(x_1)+3log(x_2)。 现有的算法将这些变体视为不同的输出,导致冗余的探索和缓慢的学习。 我们引入了EGG-SR,这是一个统一的框架,将平等图(e-graphs)集成到不同的符号回归算法中,包括蒙特卡洛树搜索(MCTS),深度强化学习(DRL)和大型语言模型(LLM)。 EGG-SR通过拟议的EGG模块紧凑地代表等效表达式,通过以下方式实现更高效的学习:(1)在EGG-MCTS中修剪冗余子树探索,(2)在EGG-DRL中跨等效类聚合奖励,(3)丰富EGG-LLM中的反馈提示。 在温和的假设下,我们表明嵌入电子图会收紧MCTS的遗憾约束,并减少DRL梯度估计器的方差。 经验上,EGG-SR在具有挑战性的基准测试中持续增强多个基线,发现比最先进的方法具有低标准化平均平方误差的方程。 代码实施可查阅:https://www.github.com/jiangnanhugo/egg-sr。
模合成是指给定底层域𝔽上单变量多项式f、g和h的系数向量，计算多项式f(g(x)) h(x)的系数向量的问题。虽然由于Kedlaya和Umans的工作，已知该问题在有限域上可在近线性时间内求解，但在无限域上尚未发现这样的近线性时间算法，目前最快的算法来自Neiger、Salvy、Schost和Villard最近的工作，在n次输入上需要O(n^1.43)次域操作。在这项工作中，我们证明对于任何无限域𝔽，模合成属于具有近线性规模和多对数深度的带除法门的代数电路的边界。此外，这个电路族本身可以在近线性时间内构造。我们的技术也扩展到其他代数问题，最显著的是计算单变量多项式的最大公因式问题。我们证明在任何无限域𝔽上，两个单变量多项式的GCD可以通过具有近线性规模和多对数深度的带除法门的代数电路在边界意义上（分段）计算，其中电路本身可以在近线性时间内构造。虽然已知单变量多项式GCD可以通过Knuth–Schönhage算法在近线性时间内计算，或者通过Andrews和Wigderson最近结果中的常数深度代数电路计算，但获得同时实现多对数深度和近线性工作的并行算法仍然是一个备受关注且尚未解决的问题。我们的结果表明在边界复杂性设置中存在这样的上界。
本文同时处理公式的快速和就地算法,其中结果必须线性累积:一些输出变量也是输入变量,由线性依赖关系链接。 基本示例包括多项式或矩阵的就地累积乘法(只有O(1)的额外空间)。 困难在于将现场计算与快速算法相结合:这些计算通常以牺牲(可能很大)额外的临时空间为代价。 我们首先为任何双线性公式(因此对于多项式和矩阵乘法)提出了一种新的快速和现场积累算法的自动设计,然后将其扩展到函数集合的任何线性积累。 为此,我们将内部模型放宽到允许修改其输入的任何算法,前提是这些输入随后恢复到初始状态。 这使我们能够为快速多项式乘法和类似Strassen的矩阵乘法派生出就地积累算法。 然后,我们考虑同时快速和到位的计算欧几里定公的剩余部分R = A B。 如果 A 和 B 具有相应的度 m+n 和 n,并且 M(k) 表示(不位)算法乘以两个度-k多项式的复杂性,则我们的算法最多使用 O(n/m) log(m)log(m)) 算术运算。 如果 M(n) = Θ(n^1+ε) 对于一些 ε>0,那么我们的算法确实匹配了 O(n/m) M(m) 的不位置复杂边界。 我们还提出了计算 - 仍在原地并具有相同的复杂边界的变体 - A = A B,R += A B和R += AC B,这是有限场扩展中的乘法。 为了实现这一目标,我们开发了Toeplitz矩阵操作的技术,用于广义卷积,短产品和功率序列划分以及输出也是输入的一部分的剩余部分。
我们通过其D-finite生成函数的镜头研究P递归序列的算术性质。 基于来自微分代数的经典工具,我们重新审视了由于Klarzar和Luca的Motzkin型序列的积分标准,并提出了在更广泛的全基因组序列中分析全局边界和代数的统一方法。 核心贡献是一种算法,它决定了所有、没有或一维解决方案家族对某些二阶复发是否具有全球范围。 这种方法概括了早期的临时方法,并成功地应用于在线整数序列百科全书(OEIS)的几个知名序列。
在Hoare的开创性发明(后来称为Hoare logic)对计算机程序的正确性进行推理之后,我们提倡一种相关但根本不同的推理方法,即访问控制等计算机程序的安全。 我们定义了形式主义,我们表示访问Hoare逻辑,并展示了其有用性和与Hoare逻辑的根本区别的例子。 我们证明了访问Hoare逻辑的健全性和完整性,并在访问Hoare逻辑和标准Hoare逻辑之间提供了链接。
我们开发和比较了线性 Mahler 运算符中计算一阶右手因子的两种算法 l_r M^r + ... + l_1 M + l_0where l_0, ..., l_r 是 x 中的多项式,Mx = x^b M 对于某些整数 b ≥ 2。 换句话说,我们给出算法来查找线性函数方程l_r(x) f(x^b^r) + ... + l_1(x^b) f(x^b) + l_0(x) f(x) f(x) = 0。 我们的第一个算法是从Petkovšek的经典算法改编的,在线性复发的情况下处理类似的问题。 第二个通过计算函数方程的广义功率系列解的基础,并使用Hermite-Padé近似值来检测与一阶因子相对应的解决方案的线性组合。 我们介绍了两种算法的实现,并结合文献的标准讨论了它们的使用,以证明马勒方程的功率序列解的微分超越。
我们引入了基于反复递归展开的及时运行时程序转换策略。 我们的在线程序优化生成了几个版本的递归循环,其区别于覆盖的最小数量的递归步骤。 在我们的技术中忽略了递归的基本情况。 我们的方法是在单一线性直接递归规则的基础上引入的。 当在运行时遇到递归调用时,首先展开器创建相关的递归规则的专业化,然后解释器将这些规则应用于调用。 我们的方法将递归规则应用程序的数量减少到其对数,而牺牲引入了一个对数的通用展开规则。 我们证明了我们的在线优化技术的正确性,并确定其时间复杂性。 对于具有足够可简化展开的递归,超线性是可能的,即加速超过恒定因子。 必要的简化是特定于问题的,必须在编译时提供。 在我们的加速分析中,我们证明了一个充分的条件,以及一个充分和必要的条件,用于超线性加速,涉及原始规则的递归步骤的复杂性和展开的规则。 我们已经实现了一个展开器和元解释器,用于运行时重复递归展开,在Prolog中嵌入的Constraint Handling Rules(CHR)中只有五个规则。 我们通过简化、时间复杂性结果和一些基本可操作算法的基准来说明我们方法的可行性。 简化需要一些见解,并且是手动导出的。 运行时改进很快达到几个数量级,与我们的定理预测的超线性速度一致。
我们考虑由 *Elementary Inference Systems* I 定义的 set/relations/computations,这些集合/relations/computations 是从 Smullyan 的 *Elementary formal systems* 获得的,使用 Gentzen 的推理规则符号,以及原子 P(t_1, ...,t_n) 的证明树,其中谓词 P 表示被考虑的 set/relation/computation。 一阶理论Th(I),实际上是一组确定的Horn子句,是给I的。 I定义的对象的属性表示为一阶句子F,在Th(I)的*canonical*模型M中,F的*satisfaction*M |=F被证明是真或假的。 因此,我们称F为I的语义属性*。 由于规范模型通常是不可计算的,因此,我们展示了如何在Th(I)的*任意*模型中通过可理解性来证明语义属性。 我们将这些想法应用于编程语言和系统的属性分析,其计算可以通过基本推理系统来描述。 特别是基于重写的系统。
本文介绍了一种通用的符号算法,用于解决具有多对角线系数矩阵的线性代数方程系统。 该算法以伪代码给出。 给出算法正确性条件的定理被制定和证明。 获取多对角线数值算法复杂性的公式。
介绍了阿基米德二次模块中严格正多项式的计算证书的新结果。 结果建立在(i)Averkov生成严格正多项式的方法的基础上,其中会员证书可以比正在申请证书的输入多项式更容易计算,以及(ii)Lasserre通过连续近似一个非负多项式乘法的平方数来生成证书的方法。 首先,通过提供有关参数的详细信息,给出了基于Averkov结果的完全建设性方法;进一步说,他的结果扩展到任意子集的工作,特别是整个欧几里得空间 R^n, 产生全球严格的正多项式。 其次,Lasserre的方法与扩展的Averkov结构集成以生成证书。 第三,方法已经实施,其有效性得到说明。 给出了现有软件包RealCertify似乎挣扎的例子,而建议的方法成功地生成证书。 确定了几种情况,其中阿基米德多项式不必明确包含在阿基米德二次模块的一组生成器中。 与解决计算证书问题的其他方法不同,所提出的方法/方法更容易理解和实现。
边界基地是通用的Gröbner基地多项式环。 在这篇文章中,我们介绍了线性差分运算体的非交换环的边界基,即合理的Weyl代数。 我们详细阐述了它们的属性,并提出了与他们一起计算的算法。 我们应用这个理论明确地表示可集成的连接为循环 D 模块。 作为一个应用,我们访问微分方程背后的字符串,一个费曼以及宇宙学积分。 我们还解决了固定全息等级的特定D-ideals的分类,即具有恒定系数的线性PDE以及Frobenius理想的情况。 我们的方法基于希尔伯特在亲和空间中的点方案理论。
多年来,概念建模一直是建筑主义教育实践的重要组成部分,特别是在STEM(科学,技术,工程和数学)学科。 并不常见的是使用基于代理的模拟来为学生提供模型质量的反馈。 这需要自动将概念模型编译到其模拟中的能力。 VERA(虚拟实验研究助理)系统是自2016年以来用于的概念建模工具,为入门大学生物学学生提供生态领域的概念建模和基于代理的模拟能力。 本文介绍了VERA及其耦合概念建模和仿真的方法,重点是如何将模型的可视化语法编译成NetLogo仿真引擎上可执行的代码。 在几所大学的入门生物学课程中,通过史密森学会的《生命百科全书》网站的经验是相关的。
我们世界的许多系统老化,降解或以其他方式缓慢但稳步地朝着某个方向前进。 当通过传感器监控这些系统时,人们通常假设数据中存在某种形式的“年龄”,但也许可用的传感器不容易提供这种有用的信息。 我们在本文中研究的任务是从可用的多变量时间序列中提取这个“年龄”的潜在代理,而没有关于“年龄”实际是什么的明确数据。 我们认为,当我们找到一个传感器,或者更有可能是可用的传感器的一些发现功能时,这是足够单调的,该功能可以作为我们正在寻找的代理。 使用精心定义的语法,并在单调性方面优化生成的方程,定义为时间和候选公式之间的绝对Spearman的等级相关性,建议的方法生成一组候选特征,然后根据单调性进行安装和评估。 拟议的系统是根据人工生成的数据集和两个真实世界数据集进行评估的。 在所有实验中,我们表明该系统能够将具有低个体单调性的传感器结合到具有高单调性的潜在特征中。 对于结构健康监测项目InfraWatch的真实世界数据集,我们展示了两个具有单个绝对Spearman ρ 值为0.13和0.09的特征,可以组合成绝对Spearman ρ 0.95的代理。 这表明我们提出的方法可以找到可解释方程,可以作为系统“年龄”的代理。
继续最近使用翻转图对矩阵乘法的张力等级进行边界调查,我们在这里提出了大约30种矩阵格式的等级边界。
在这里,我介绍了使用R编程语言与Clifford代数合作的“clifford”软件包。 描述代数,并给出包成语。
在本文中,我们提供了对周期性Golay对进行详尽搜索的算法方法。 我们的方法列举了一些超出目前已知最先进的搜索的长度:我们使用我们的方法对所有长度的周期性Golay对v ≤ 72进行了详尽的搜索,而以前只有长度v ≤ 34以前被详尽地列举过。 我们的方法适用于一般周期性互补序列。 我们使用序列压缩,这是Djoković和Kotsireas在2013年衍生的序列生成方法。 我们还介绍并实现了一种“多级”压缩的新方法,其中序列在几个步骤中未压缩。 这种方法允许我们使用不到10个CPU年彻底搜索所有长度v ≤ 72。 对于无法进行解压缩的互补序列的情况,我们引入了一些新的序列生成方法,其灵感来自有序生成的无异构详尽生成算法。 最后,我们对周期性Golay对的结构提出了一个猜想,并证明它具有许多长度,包括所有长度v 100。 我们通过提供有史以来第一个周期性 Golay 对长度 v = 90 的例子来证明我们的算法的有用性。 周期性Golay对存在的最小长度为未定,现在是106。
给定 Z^n 中 n 向量的格子基础,我们提出了一个使用 12n^3+O(n^2) 浮点运算的算法来检查基础是否被 LLL 还原。 如果基础减少,那么算法有望回答“是”。 如果基础没有减少,或者使用的精度不足以用于n,并且对基础的数值属性,则算法将回答“失败”。 因此,一个肯定的答案是一个严格的证书。 为了实现证书本身,我们提出了一个浮点算法,用于计算QR矩阵因子的R因子条目的误差边界。 该算法考虑了所有可能的近似和四舍五入错误。 证书的成本 12n^3+O(n^2) 比计算QR因子化本身的数值算法的成本仅高出6倍,证书只能使用矩阵库例程实现。 我们报告的实验表明,为了减少足够的尺寸和质量,证书成功,并确定证书的有效性。 这种有效性适用于认证LLL减少的最快现有浮点异构的输出,而不会减慢整个过程。
我们分析了计算类多项式的复杂性,这是椭圆曲线CM结构的重要成分,通过复杂的浮点近似其根源。 算法的核心是在几个参数中评估模块化函数。 最快的方法使用Dupont设计的技术,通过牛顿迭代评估涉及算术几何均值的表达式的模块化函数。 它运行在时间 O (|D| log^5 |D| loglog |D|) = O (|D|^1 + ε) = O (h^2 + ε)对于任何 ε > 0,其中 D 是 CM 判别器,h 是类多项式的程度。 另一种快速算法使用符号计算已知的多点评估技术;其渐近复杂度因日志 |D| 的因子而更糟。 高达对数因素,此运行时间与构造多项式的大小相匹配。 该估计还依赖于一个新的结果,即列举一个假象-二次顺序的类群的复杂性,以及严格证明的类多项式高度的上限。
继续滚动加载更多
