计算机科学
Computer Science
人工智能
Artificial Intelligence
计算与语言
Computation and Language
计算复杂性
Computational Complexity
评估用于仪器控制的大型语言模型(LLM)需要超越标准无状态算法基准的方法,因为仅通过单元测试无法完全捕获物理系统的行为。 在这里,我们介绍了EnvTrace,一种基于模拟的方法,用于评估执行跟踪以评估语义代码等同。 EnvTrace使用波束线控制逻辑数字孪生体进行演示,以促进仪器控制代码的评估,数字孪生本身也能够对现场实验进行执行前验证。 超过30个LLM使用跟踪对齐进行了评估,以生成跨关键行为维度的功能正确性的多方面评分,表明许多顶级模型可以在快速控制代码生成中接近人类级性能。 这是迈向更广阔视野的第一步,其中LLM和数字孪生共生工作:LLM提供直观的控制和代理编排,数字孪生提供安全和高保真环境,为自主体现AI铺平道路。
像Cerebras Wafer-Scale Engine这样的空间数据流架构通过利用跨处理元素(PE)和本地化计算之间的分布式内存,在AI和科学应用中实现卓越的性能。 然而,由于需要通过可重新配置的片上网络和由数据到达触发的异步计算来明确编排数据移动,因此对这些架构进行编程仍然具有挑战性。 现有的FPGA和CGRA编程模型强调循环调度,但忽略了空间数据流架构的独特功能,特别是常规网格上的高效数据流和复杂的路由管理。 我们介绍了SPADA,一种编程语言,可以精确控制数据位置,数据流模式和异步操作,同时抽象架构特定的低级细节。 我们为 SPADA 引入了严格的数据流语义框架,该框架定义了路由正确性、数据竞赛和死锁。 此外,我们设计和实现了一个针对Cerevaris CSL的编译器,具有多级降低。 SPADA既是高级编程接口,也是特定领域语言(DSL)的中间表示,我们用GT4Py模板DSL演示。 SPADA使开发人员能够比CSL少6-8倍的代码表达复杂的并行模式 - 包括管道减少和多维模板 - 在三个数量级之间几乎理想的弱缩放。 通过统一单个模型下的空间数据流架构编程,SPADA推进了这些新兴高性能计算平台的理论基础和实践可用性。
静态分析工具提供了一种强大的手段,通过指定编码易受攻击的代码模式的查询来检测安全漏洞。 然而,编写此类查询具有挑战性,需要在安全和程序分析方面具有多种专业知识。 为了应对这一挑战,我们展示了QLCoder - 一个代理框架,它自动合成CodeQL中的查询,CodeQL是一个强大的静态分析引擎,直接从给定的CVE元数据。 QLCode将LLM嵌入到具有执行反馈的合成循环中,同时使用自定义MCP接口限制其推理,该接口允许与语言服务器协议(用于语法指导)和RAG数据库(用于查询和文档的语义检索)进行结构化交互。 这种方法允许QLCoder生成语法和语义上有效的安全查询。 我们在 111 个 Java 项目中对 176 个现有 CVE 进行 QLCode 评估。 基于 Claude Code 代理框架,QLCoder 综合了正确的查询,检测易受攻击的 CVE ,但在 53.4% 的 CVE 的修补版本中检测 CVE。 相比之下,仅使用克劳德代码可以合成10%的正确查询。
动态行为在许多张量应用程序中越来越普遍。 例如,在机器学习中,输入张量是动态形状或破烂的,数据依赖的控制流在许多模型中被广泛使用。 然而,空间数据流加速器的先前编程抽象的有限表现力迫使动态行为静态实现,或者缺乏性能关键决策的可见性。 为了应对这些挑战,我们提出了流式张量程序(STeP),这是一个新的流抽象,使动态张量工作负载能够在空间数据流加速器上高效运行。 STeP引入了灵活的路由运算符、显式内存层次和符号形状语义,可以暴露动态数据速率和张量维度。 这些功能解锁了新的优化动态平铺,动态并行和配置时间-多路复用 - 适应动态行为,同时保持数据流效率。 使用具有真实世界痕迹的具有代表性的LLM层上的循环近似模拟器,动态平铺将片上内存需求减少了2.18倍,动态并行化将延迟提高了1.5倍,配置时间复用使计算利用率比先前抽象中可用的实现提高了2.57倍。
随着摩尔定律的放缓,诸如现场可编程门阵列(FPGA)等异构计算平台对加速HPC工作负载的兴趣越来越大。 在这项工作中,我们介绍了通过MLIR中的OpenMP目标指令首次实现选择性代码卸载到FPGA。 我们的方法将MLIR OpenMP方言与高级合成(HLS)方言相结合,提供针对FPGA的便携式编译流。 与以前依赖自定义编译器的OpenMP FPGA努力不同,相比之下,我们与MLIR集成,因此支持任何与MLIR兼容的前端,在这里用Flang演示。 基于一系列现有的MLIR构建模块,大大减少了所需的工作量,并证明了MLIR生态系统的可组合性优势。 我们的方法支持通过标准 OpenMP 指令手动优化卸载内核,这项工作为 MLIR 生态系统中集成的基于指令的 FPGA 加速建立了灵活和可扩展的路径。
使用频率域全息减小表示(FHRR),我们将Lisp 1.5的矢量符号架构(VSA)编码与使用剩余超维计算(RHC)的算术运算为正文扩展。 在高维向量空间上编码图灵完备的语法会增加神经网络状态的表达性,使网络状态能够包含具有固有可解释的任意结构化表示。 我们讨论了VSA编码在机器学习任务中的潜在应用,以及编码结构化表示和设计神经网络的重要性,这些神经网络的行为因其获得比目前更通用的智能代理而对其表示结构敏感。
Galois切片是一种用于来源的程序切片技术,由Perera和合作者开发。 Galois切片旨在通过演示如何跟踪输入和输出向前和向后沿着特定执行近似值来解释程序执行。 在本文中,我们探讨了Galois切片和可微分编程之间的类比,将前向和向后切片的实现视为一种自动分化。 使用CHAD方法自动区分Vákár和合作者,我们通过分类语义重新划分Galois切片。 在这样做的过程中,我们能够探索Galois切片思想的扩展到定量区间分析,并澄清这种方法的现有实例化中所做的隐性选择。
传统上,在线性类型语言中,消耗线性资源与其在程序中的句法发生同义。 然而,在非严格评估的视角下,线性性可以在语义上进一步理解,其中资源的句法发生并不一定意味着在执行程序时使用该资源。 虽然这种区别在很大程度上尚未探索,但在Haskell的优化编译器中却是不可避免的,该编译器在很大程度上重写了源程序,从而打破了语法线性度,但保留了程序的语义。 我们引入了线性核心(Linear Core),这是一种新颖的系统,它静态地接受线性的懒惰语义,适用于懒惰的语言,如格拉斯哥哈斯卡尔编译器的核心中间语言。 我们证明 Linear Core 是健全的,保证了线性资源的使用,并且多个优化转换保留了 Linear Core 中的线性度,同时在 Core 中未能这样做。 我们已经实现了线性核心作为编译器插件,以验证系统对抗线性重库,包括线性基。
符号执行有助于检查程序,探索基于符号输入的不同路径。 像KLEE这样的工具是常用的,因为它们可以自动检测bug并创建测试用例。 但是,KLEE最大的问题之一是,当程序有很多分支路径时,它的速度会有多慢 - 它通常变得过于资源繁重,无法运行在大型或复杂的代码上。 在这个项目中,我们想看看像GPT-4o这样的大型语言模型是否可以模拟KLEE生成的输出类型。 这个想法是探索LLM是否可以有一天取代符号执行的部分,以节省时间和资源。 一个具体目标是让GPT-4o识别程序中受约束的路径,这是具有最大象征意义条件的执行路径。 这些路径尤其重要,因为它们通常代表难以测试的边缘案例,并且更有可能包含深度错误。 然而,弄清楚这一点通常需要完全运行的KLEE,这可能是昂贵的。 因此,我们测试了GPT-4o是否可以使用100 C程序的数据集预测KLEE输出和最复杂的路径。 我们的结果显示,在生成类似KLEE的输出和识别最受限的路径方面,准确率约为20%。 虽然不是高度准确,但这项早期工作有助于显示当前LLM在模拟符号执行时可以做什么和不能做什么。
目前对代码生成的LLM的评价强调了功能的正确性,忽视了功能上正确的解决方案在算法复杂性方面可能有很大差异的事实。 例如,(O(n^2))与(O(n log n))排序算法可能会产生类似的输出,但在生产中产生截然不同的性能成本。 这种差异揭示了当前评估方法的一个关键限制:它们未能捕捉到正确解决方案之间的行为和性能多样性。 为了解决这个问题,我们引入了一个用于评估生成代码的动态稳定性的原则框架。 我们提出了来自opcode分布的两个指标:静态 Canonical Trace Divergence (SCTD),它捕获了生成解决方案的算法结构多样性,以及动态 Canonical Trace Divergence (DCTD),它量化运行时行为方差。 它们的比例,行为表达因子(BEF),作为诊断信号:当BEF≪1和BEF≫1时,它表示关键的运行时不稳定,当BEF≪1时,功能冗余。 BigOBench和CodeContests的经验结果表明,最先进的LLM即使在功能正确的输出中也表现出显著的算法差异。 值得注意的是,提高采样温度提高了pass@1速率,但降低了稳定性,揭示了一种未被认可的权衡:在不同的输出空间中寻找正确的解决方案引入了正确性和行为一致性之间的“不稳定性惩罚”。 我们的研究结果要求代码生成中的稳定性感知目标,以及具有无症状测试用例的新基准,以实现强大的真实世界LLM评估。
Damas-Hindley-Milner(ML)类型系统的成功归功于公国,每个类型良好的表达式都有独特的最通用类型。 这使得推理可以预测且高效。 不幸的是,ML的许多扩展(GADTs,更高等级的多态性和静态重载)通过引入抵抗主要推理的_fragile_结构来危及原则性。 现有方法通过定向推理算法恢复公国,该算法以固定(或静态)顺序(例如双向类型)传播_known_type信息,以消歧义此类结构。 然而,静态推理顺序的刚性往往导致其他类型良好的程序被拒绝。 我们提出 _omnidirectional_ 类型推理,其中类型信息以动态顺序流。 键入约束可以按任何顺序解决,当进度需要已知类型信息时暂停,并在可用后恢复,使用 _sspended match 约束。 对于简单的类型系统来说,这种方法很简单,但由于允许的概括,将其扩展到ML具有挑战性。 现有的ML推理算法以固定的顺序键入let-bindings(let x = e1 in e2):类型e1,泛化其类型,然后键入e2。 为了克服这一点,我们引入了 _incremental instantiation_,允许实例化包含暂停约束的部分解决类型方案,并在方案完善时逐步更新实例。 综合性为在脆弱特征下恢复公国提供了一个通用框架。 我们在 OCaml 的两个根本不同的特征上展示了它的多功能性:记录标签和数据类型构造函数的静态重载和半显式一等多态性。 在这两种情况下,我们获得了比 OCaml 当前类型 typechecker 更具表现力的主类型推断算法。
最近的技术,如账面支付,不可替代的令牌和智能合约,都是分布式账本技术的持续开发成果。 预见的趋势是,它们将在日常生活中发挥越来越明显的作用,而日常生活必须得到适当的业务资源的支持。 例如,由于需求增加,智能合约可能很快就会面临缺乏知识渊博的用户和工具来处理它们。 广泛的智能合约采用目前受到安全性,可用性和成本方面的限制。 由于学习曲线陡峭,智能合约的处理目前主要由专业开发人员执行,大多数研究工作都集中在智能合约安全性上,而可用性等其他方面则有些被忽视。 特定的工具将降低进入障碍,使感兴趣的非专家能够创建智能合约。 在本文中,我们设计、开发和测试了Blockly2Hooks,即使在具有挑战性的场景中,例如智能合约以C等高级语言编写时,也能填补这一空白。 以XRP Ledger作为具体工作案例,Blockly2Hooks通过利用经过验证的教学方法,如Visual Programming Languages,更具体地说,Google的Blockly Visual Programming库,帮助社区感兴趣的非专家轻松学习智能合约并采用该技术。 该平台经过开发和测试,结果有望使学习智能合约开发更加顺畅。
现代深度学习编译器依靠布局抽象来管理逻辑张量结构和物理内存排列之间的复杂映射。 CuTe布局和Triton线性布局是广泛采用的行业标准。 然而,这些布局系统以不同的数学基础独立运作,阻止了统一的正式分析和跨系统推理。 我们通过引入一种新颖的方法弥合这一差距,该方法利用整数集库(ISL)通过整数集关系为两个布局系统创建统一的数学表示,从而实现严格的形式分析,正确性验证以及未来跨系统优化策略的基础。 我们的方法通过整数集关系对CuTe布局进行布局,这些关系使用基于步幅的计算来编码从多维坐标到线性索引的变换,包括复杂的swizzle操作,执行位级操作,以增强内存访问模式。 对于 Triton 线性布局,我们构建整数集关系,对二进制向量空间变换进行建模,其中算术运算遵循有限字段 F_2 规则。 我们实现了一套完整的布局操作算法,用于组成,反转,使用ISL中的内置操作进行补充,以确保数学正确性并保留布局语义。 实验评估表明,该系统处理布局复杂性的全谱,从基本身份转换到复杂的多维张量安排,具有复杂的步幅配置和摆动模式,验证了跨不同布局范式的数学建模方法。
我们介绍了Cyclotron,一个使用递归方程表达流数据流算法的框架和编译器,然后将其可移植编译为相互关联的处理器的分布式拓扑。 我们的框架提供了一种在逻辑张量上重复的输入语言,然后将其降低到逻辑迭代空间上复发的中间语言,最后进入每个处理器特有的发送,接收和计算操作的程序。 在Cyclotron的IR中,程序进行了优化,使得外部内存交互仅限于迭代空间的边界。 在内部迭代空间中,所有数据访问都成为本地数据:数据访问驻留在本地快速存储器或邻近处理单元中的目标值,避免了昂贵的内存移动。 我们提供一种调度语言,允许用户定义数据如何在处理器之间流式传输和广播,从而通过处理元素的分布式拓扑结构实现计算内核的管道执行。 我们通过将我们的 IR 编译为系统阵列和芯片样式分布式硬件的可重新配置模拟器以及分布式内存 CPU 集群,展示了我们方法的可移植性。 在模拟可重新配置设置中,我们使用编译器进行硬件设计空间探索,其中可以指定链接成本和延迟。 在分布式 CPU 设置中,我们展示了如何使用 recurrences 和调度语言来表达各种矩阵乘法例程(Cannon、SUMMA、PUMMA、重量固定)和求解器(Triangular solve 和 Cholesky)。 对于矩阵乘法和三角形求解,我们生成与 ScaLAPACK 竞争的分布式实现。
非交互式零知识(NIZK)证明,如zkSNARKS,让一个人证明私人数据的知识,而不透露它或与验证者交互。 虽然现有的工具侧重于指定待验证的谓词,但现实世界的应用程序优化了谓词定义,以尽量减少证明生成开销,但必须相应地变换谓词输入。 实现这两个步骤分别重复了必须精确匹配的逻辑,以避免灾难性的安全漏洞。 我们用 zkStruDul 解决了这个缺点,zkStruDul 是一种将输入变换和谓词定义统一为单个组合抽象的语言,编译器可以从中投射这两个过程,从而消除重复的代码和有问题的不匹配。 zkStruDul 提供了一个高级抽象,在现有的 NIZK 技术之上分层,并支持诸如递归证明等重要功能。 我们提供源级语义,并证明其行为与预测语义相同,允许直接的标准推理。
本文研究编程语言的设计,处理程序设计具有高阶有效操作 - 有效的操作,可以在计算中作为参数或返回计算作为输出。 我们介绍并分析具有更高类型超种的超常性的核心演算,高阶有效操作的处理器以及可选的一般递归。 这种微积分的独特设计选择是,处理程序由无法无天的原始monads携带,而计算判断仍然满足monadic法律的判断。 我们用逻辑框架呈现演算,并使用可实现性语义给出演算的表示模型。 我们证明了使用合成Tait可计算性和新形式的⊤⊤提升技术对语言的递归无递归片段的闭门规范和参数化。
修辞模式在学术和非学术写作中都有用,可以在语言研究和计算建模中研究。 在这些领域之间建立概念桥梁可以使每个人都从其他领域中受益。 本文提出了基于二元性的模式操作(分裂统一,向前向后,扩展减少和正交二元性),以扩展一系列修辞模式,引入组合和概括等生成模式,从而增强跨多个应用的认识多样性。 它进一步提出了一个金字塔多层映射框架(例如,从修辞模型层到认知层和认识层的三层),从而降低了由此产生的认知复杂性。 表现多样性和复杂性降低的程度通过二项式组合和香农熵分析量化。 确定了边际修辞位(MRB),允许定义一个修辞可扩展参数,该参数测量每个阶段比特的表达增长速度。 直接熵测量表明,与所有模式的平面选择相比,较小的子集的分层选择显着减少了选择的不确定性。 这些考虑似乎将静态和不可测量的修辞分类转变为更动态、更可测量的话语设计系统。 从这项工作中,可以确定未来人工智能系统不仅可以在语言令牌上运行,还可以在分层修辞推理结构上运行,弥合语言,教学,学术和计算研究。
基于语言的测试将无上下文语法定义与语法元素的语义约束相结合,以生成测试输入。 通过将无上下文语法与约束配对,用户可以在保留简单结构的同时,具有不受限制语法的表现力。 然而,在存在这种限制的情况下提供投入可能具有挑战性。 在过去的方法中,SMT求解器在找到字符串解决方案方面非常缓慢;进化算法更快,更普遍,但目前的实现仍然难以应对编译器测试等域所需的复杂约束。 在本文中,我们提出了一种基于进化语言的测试的新方法,该方法在当前最先进的条件下将性能提高了3-4个数量级,将生成时间并减少了时间,并将解决时间限制到几秒钟。 我们通过(1)仔细将语法定义转换为 Rust 类型和 trait 实现来实现这一点,确保编译器可以近乎最大化地优化任意语法上的任意操作;(2)使用更好的进化算法,提高基于语言的测试解决复杂约束系统的能力。 这些性能和算法改进允许我们的原型FANDANGO-RS解决以前策略根本无法处理的限制。 我们通过C子集的案例研究证明了这一点,其中FANDANGO-RS每分钟能够为C编译器生成401个多样化,复杂和有效的测试输入。
编译器必须检查代码转换的合法性,以保证将代码转换序列应用于给定代码转换的正确性。 虽然这种合法性检查需要精确计算,但在某些情况下,我们可以使用近似的合法性预测模型,例如训练强化学习(RL)代理进行时间表预测。 在本文中,我们提出了一个近似的合法性检查方法。 我们提出了一种新的DL模型,用于预测变换的合法性。 该模型将代码表示和转换列表作为输入,并预测将这些转换应用于代码是否合法。 我们实施和评估拟议的模型,证明其有效性。 我们的评估显示,在一组随机生成的程序的测试中,F1的得分为0.91。 为了在实用场景中进一步评估模型,我们使用该模型来替换用于自动代码优化的RL代理训练时使用的合法性检查。 我们证明,这种替换使代理能够训练两倍的步骤,从而加快训练速度,减少CPU的资源使用量约80%,RAM减少35%。 使用这种方法训练的代理保持可比的性能,与传统方法相比,Polybench套件的基准仅减少了4%。
随着对计算能力的需求不断增长,通过编译器优化代码变得越来越重要。 在此背景下,我们专注于全自动代码优化技术,无需人工干预即可自动选择和应用代码转换以获得更好的性能。 了解这些转换的行为和交互方式是设计更有效的优化策略的关键。 编译器开发人员在构建这些启发式设计时必须做出许多设计选择。 例如,他们可以决定是否允许以任意顺序探索转换,或者执行固定序列。 虽然前者理论上可能提供最佳性能增益,但它显着增加了搜索空间。 这就提出了一个重要问题:应用转换的预定义、固定顺序能否在不严重损害优化潜力的情况下加快搜索速度? 在本文中,我们解决了自动代码优化算法设计中出现的这个问题和其他相关问题。 使用数据驱动的方法,我们生成大量的随机程序数据集,应用随机优化序列,并记录其执行时间。 通过统计分析,我们提供见解,指导更高效的自动代码优化算法的开发。
继续滚动加载更多
