大型语言模型(LLM)在广泛的编程任务中表现出强大的性能,但其代码优化的潜力仍然不足。 这项工作调查了LLM是否可以优化汇编代码的性能,其中对执行的细粒度控制可以实现难以用高级语言表达的改进。 我们提出了一个强化学习框架,使用近端策略优化(PPO)训练LLM,该框架由奖励函数引导,该函数既考虑功能正确性,又通过测试用例验证,以及相对于行业标准编译器gcc-O3的执行性能。 为了支持这项研究,我们引入了8,072个现实世界计划的基准。 我们的模型Qwen2.5-Coder-7B-PPO实现了96.0基线,优于所有其他评估的20个模型,包括Claude-3.7-sonnet。 这些结果表明,强化学习可以释放LLM的潜力,作为汇编代码性能的有效优化器。
随着现代软件系统的规模和复杂性的扩展,与其建模和配方相关的挑战变得越来越复杂。 传统方法往往缺乏有效解决这些复杂性,特别是在诸如用于维护和评估的设计模式检测以及优化和长期可持续性的代码重构等任务中。 这种日益加剧的不足突出表明,在如何处理和解决这些挑战方面需要范式转变。 本文介绍了分析软件工程(ASE),这是一种新颖的设计范式,旨在平衡抽象,工具可访问性,兼容性和可扩展性。 ASE 能够有效建模和解决复杂的软件工程问题。 范式通过两个框架进行行为结构序列(BSS)和优化设计重构(ODR)评估,这两个框架都是根据ASE原则开发的。 BSS提供了紧凑的、与语言无关的代码库表示,以方便精确的设计模式检测。 ODR统一了人工制品和解决方案表示,通过方法优化代码重构,同时消除迭代计算开销。 通过提供针对软件设计挑战的结构化方法,ASE为未来编码和分析复杂软件指标的研究奠定了基础。
使用大型语言模型(LLM)自动生成寄存器传输级别(RTL)代码,为简化数字电路设计和减少人力工作提供了巨大的前景。 然而,目前基于LLM的方法面临着严峻的挑战,包括培训数据稀缺,规范代码对齐不良,缺乏验证机制以及平衡泛化与专业化。 受 DeepSeek-R1 的启发,我们引入了 VeriReason,这是一个集成了用于 RTL 生成的引导奖励近端优化 (GRPO) 强化学习的监督微调框架。 使用策划的训练示例和反馈驱动的奖励模型,VeriReason将测试台评估与结构方法论相结合,同时嵌入了自主纠错的自我检查功能。 在 VerilogEval 基准测试中,VeriReason 提供了显著改进:在 VerilogEval Machine 基准测试中实现了 83.1 的正确性,大大优于同类型号和更大的商业系统,如 GPT-4 Turbo。 此外,与基线方法相比,我们的方法表明,与基线方法相比,首次尝试的功能正确性增加了2.8倍,并且对看不见的设计表现出稳健的概括。 据我们所知,VeriReason代表了第一个成功集成明确推理能力与Verilog一代强化学习的系统,为自动化RTL合成建立了新的最先进的技术。 模型和数据集可在以下网址查阅:https://huggingface.co/collections/AI4EDA-CASE Code:https://github.com/NellyW8/VeriReason
信息流控制系统通常强制对进度不敏感的互不干涉,因为它易于理解和执行。 不幸的是,真正的程序需要解密结果并认可输入,这些输入是不干涉的,同时防止攻击者控制泄漏,包括通过进度渠道,而进度不敏感会忽略这些渠道。 这项工作将对进度敏感的安全与安全降级(解密和背书)相结合,以确定安全降级进度信息的概念。 我们使用超属性来提炼进度敏感和进度不敏感互不干涉之间的分离,并将其与非可销售信息流(安全降级的现有(进展不敏感)定义)相结合,以定义不可销售的进展泄漏(NMPL)。 我们介绍了第一个信息流类型系统,以便在执行 NMPL 时允许一些进度泄漏,我们展示了如何推断安全进度降级的位置。 所有定理都在Rocq中验证。
强化学习(RL)已被广泛采用,以提高大型语言模型(LLM)在Text-to-SQL任务上的性能。 然而,现有方法通常依赖于基于执行或基于LLM的Bradley-Terry奖励模型。 前者遭受重复数据库调用造成的高执行延迟,而后者则施加了大量的GPU内存开销,这两者都显着阻碍了RL管道的效率和可扩展性。 为此,我们提出了一个名为Graph-Reward-SQL的新型Text-to-SQL RL微调框架,它采用了GMNScore结果奖励模型。 我们利用 SQL 图形表示提供准确的奖励信号,同时显著减少推理时间和 GPU 内存使用情况。 在这一基础上,我们进一步引入了StepRTM,这是一种逐步奖励模型,为Common Table Expression(CTE)子查询提供中间监督。 这鼓励了 SQL 的功能正确性和结构清晰度。 包括Spider和BIRD在内的标准基准的广泛比较和消融实验证明,我们的方法始终优于现有的奖励模型。
大型语言模型(LLM)在广泛的编程任务中表现出强大的性能,但其代码优化的潜力仍然不足。 这项工作调查了LLM是否可以优化汇编代码的性能,其中对执行的细粒度控制可以实现难以用高级语言表达的改进。 我们提出了一个强化学习框架,使用近端策略优化(PPO)训练LLM,该框架由奖励函数引导,该函数既考虑功能正确性,又通过测试用例验证,以及相对于行业标准编译器gcc-O3的执行性能。 为了支持这项研究,我们引入了8,072个现实世界计划的基准。 我们的模型Qwen2.5-Coder-7B-PPO实现了96.0基线,优于所有其他评估的20个模型,包括Claude-3.7-sonnet。 这些结果表明,强化学习可以释放LLM的潜力,作为汇编代码性能的有效优化器。
1978年起,克拉伦斯·巴洛发展了“不可或缺性功能”。 它在一个公制树上运行,该公制树绑定到每个特定级别的所有子树的相同素数的分支。 它为这棵树的所有叶子柱分配了一个数值,该数值表明该位置的事件的声学存在对于该仪表被识别为该值的重要性。 Bernd Härpfer在2015年扩展了这一概念,以处理在树层次结构的任何位置具有任意分组的米数。 这被称为“扩展的不可或缺的算法”。 本文给出了Z规范语言的扩展算法的规范,以及对任意度量树的可能概括。
本文介绍了 PyEB 工具,这是 Event-B 细化演算的 Python 实现。 PyEB工具采用Python程序并生成几个证明义务,然后将其传递给Z3求解器以进行验证。 Python 程序代表 Event-B 模型。 这些证明义务的示例是机器不变保存,非确定性事件操作的可行性,事件守卫加强,事件模拟和机器变体的正确性。 Python程序遵循特定的面向对象语法;例如,操作、事件、上下文和机器被编码为Python类。 我们实现了 PyEB 作为 PyPI(Python 包索引)库,该库可在网上免费获得。 我们进行了关于使用PyEB的案例研究。 我们在Python中建模和验证了几种顺序算法,例如二进制搜索算法和平方根算法等。 我们的实验结果表明,PyEB验证了用Python编写的精细微积分模型。
随着大型语言模型(LLM)成为与代码相关的任务的组成部分,一个核心问题出现了:LLM是否真正理解程序执行语义? 我们引入了EquiBench,这是一个通过等值检查来评估LLM的新基准,即确定两个程序是否为所有可能的输入产生相同的输出。 与以前的代码生成基准不同,此任务直接测试模型对代码执行语义的理解。 EquiBench由2400个程序对组成,分为四种语言和六个类别。 这些对通过程序分析、编译器调度和超优化生成,确保高置信度标签、非平凡难度和完全自动化。 这些变换跨越句法编辑、结构修改和算法变化,涵盖了广泛的语义变化。 我们评估了19个最先进的LLM,发现在最具挑战性的类别中,最好的精度是53.8以上的句法相似性,而不是对执行语义表现出强大的推理,突出了基本限制。
本文介绍了Genesis,第一个旨在支持Hamiltonian Simulation的混合连续变量(CV)和离散变量(DV)量子计算系统的编译器。 Genesis是一个两级编译系统。 在第一个阶段,它使用目标混合CV-DV量子计算机的本地指令集将输入Hamiltonian分解为基础门。 在第二层,它解决了量子模/量子比特的映射和路由,以实现从第一层分解的大门的远程交互。 而不是依赖于类似于基于量子位(或DV)系统的SWAP原语的典型实现,我们提出了为混合CV-DV系统量身定制的连接感知门合成和波束分裂器SWAP插入的集成设计。 我们还引入了一种类似OpenQASM的域特异性语言(DSL),称为CVDV-QASM,用于代表Hamiltonian,用于从混合CV-DV门集的Pauli-exponentials和基本门序列。 Genesis已经成功编译了几个重要的Hamiltonians,包括Bose-Hubbard模型,Z_2-Higgs模型,Hubbard-Holstein模型,Heisenberg模型和Electron-vibration耦合Hamiltonians,这些在量子场论,凝聚态物理和量子化学等领域至关重要。 我们的实现可在 Genesis-CVDV-Compiler(https://github.com/ruadapt/Genesis-CVDV-Compiler)获得。
随着硬件设计复杂性的升级,电子设计自动化(EDA)迫切需要先进的自动化。 传统的寄存器传输水平(RTL)设计方法是手动的,耗时的,容易出错。 虽然商业(指令调整)大型语言模型(LLM)在自动化方面表现出有希望的性能,但它们带来了安全和隐私问题。 开源模型提供了替代方案;然而,它们往往缺乏质量/正确性,这主要是由于有限的高质量RTL代码数据对于有效培训和推广至关重要。 本文提出了RTL++,这是RTL代码生成的第一个LLM辅助方法,它利用代码结构的图形表示来增强生成的代码的质量。 通过将RTL代码编码为文本化控制流图(CFG)和数据流图(DFG),RTL++捕获了代码中固有的层次结构、依赖关系和关系。 这种基于图的结构化方法增强了LLM可用的上下文,使它们能够更好地理解和生成指令。 通过专注于通过图形表示生成数据,RTL++解决了以前仅依赖代码并缺乏多样性的方法的局限性。 实验结果表明,RTL++优于针对RTL一代进行微调的最先进的模型,使用VerilogEval基准的Pass@1/5/10度量以及RTLLM1.1模型进行评估,该模型突出了图形增强上下文在推进LLM辅助RTL代码生成功能方面的有效性。
类别理论在数学和计算机科学的最新发展中的重要性怎么强调都不为过。 然而,它的抽象性质使它起初难以理解。 图形语言已被开发来帮助管理这种抽象,但它们没有用于校对助手,其中大部分都是基于文本的。 我们相信,集成在通用证明助理中的分类证明的图形界面将允许学生在他们已经熟悉的具体证明上熟悉图表推理。 我们介绍了一个Coq插件的实现,它能够以图形方式实现可视化和与Coq证明的交互。
操作树形数据结构的程序通常需要复杂的、难以概括和自动化的专用证明。 本文介绍了验证此类程序的统一、基本方法。 我们的方法的核心是针织树编码,将每个程序执行建模为捕获输入、输出和中间状态的树结构。 利用针织树的成分性质,我们将这些结构编码为约束的角子子(CHC),减少对CHC可满足性任务的验证。 为了说明我们的方法,我们专注于内存安全,并展示它如何自然地导致简单,模块化的不变性。
大型语言模型(LLM)的激增在计算领域开辟了新的前沿,但控制和编排其超越简单文本生成的能力仍然是一个挑战。 当前的方法,如函数/工具调用和直接代码生成,在表现力、可扩展性、成本、安全性和强制精细控制能力方面受到限制。 本文介绍了Pel,一种专门用于弥合这一差距的新型编程语言。 受到Lisp,Elixir,Gleam和Haskell的优势的启发,Pel提供了一个句法简单,同质化和语义丰富的平台,为LLM提供安全有效地表达复杂的动作,控制流程和代理间通信。 Pel的设计强调一种极小、易于修改的语法,适用于受限的LLM生成,通过在语法级别启用能力控制,消除了对复杂沙盒的需求。 主要功能包括用于线性组合的强大管道机制,实现轻松部分应用和功能模式的一流关闭,内置支持LLM评估的自然语言条件,以及具有Common Lisp样式重新启动的高级Read-Eval-Print-Loop(REPeL)和用于自动纠错的LLM驱动的辅助代理。 此外,Pel还通过静态依赖性分析集成了独立操作的自动并行化,这对于高性能代理系统至关重要。 我们认为,Pel为LLM编排提供了更强大,更安全和更具表现力的范式,为更复杂和可靠的AI代理框架铺平了道路。
使用大型语言模型(LLM)自动生成寄存器传输级别(RTL)代码,为简化数字电路设计和减少人力工作提供了巨大的前景。 然而,目前基于LLM的方法面临着严峻的挑战,包括培训数据稀缺,规范代码对齐不良,缺乏验证机制以及平衡泛化与专业化。 受 DeepSeek-R1 的启发,我们引入了 VeriReason,这是一个集成了用于 RTL 生成的引导奖励近端优化 (GRPO) 强化学习的监督微调框架。 使用策划的训练示例和反馈驱动的奖励模型,VeriReason将测试台评估与结构方法论相结合,同时嵌入了自主纠错的自我检查功能。 在 VerilogEval 基准测试中,VeriReason 提供了显著改进:在 VerilogEval Machine 基准测试中实现了 83.1 的正确性,大大优于同类型号和更大的商业系统,如 GPT-4 Turbo。 此外,与基线方法相比,我们的方法表明,与基线方法相比,首次尝试的功能正确性增加了2.8倍,并且对看不见的设计表现出稳健的概括。 据我们所知,VeriReason代表了第一个成功集成明确推理能力与Verilog一代强化学习的系统,为自动化RTL合成建立了新的最先进的技术。 模型和数据集可在以下网址查阅:https://huggingface.co/collections/AI4EDA-CASE Code:https://github.com/NellyW8/VeriReason
信息流控制系统通常强制对进度不敏感的互不干涉,因为它易于理解和执行。 不幸的是,真正的程序需要解密结果并认可输入,这些输入是不干涉的,同时防止攻击者控制泄漏,包括通过进度渠道,而进度不敏感会忽略这些渠道。 这项工作将对进度敏感的安全与安全降级(解密和背书)相结合,以确定安全降级进度信息的概念。 我们使用超属性来提炼进度敏感和进度不敏感互不干涉之间的分离,并将其与非可销售信息流(安全降级的现有(进展不敏感)定义)相结合,以定义不可销售的进展泄漏(NMPL)。 我们介绍了第一个信息流类型系统,以便在执行 NMPL 时允许一些进度泄漏,我们展示了如何推断安全进度降级的位置。 所有定理都在Rocq中验证。
部署语言模型通常需要导航精度与性能权衡,以满足延迟限制,同时保持实用性。 传统模型蒸馏减少了尺寸,但通过培训单独的模型会产生大量成本。 我们引入了ModularStarEncoder(MoSE),这是一种10亿参数的多层编码器,用于代码检索和分类,采用新颖的自蒸馏机制。 这种方法显着增强了较低层的表示,使不同模型部分的灵活部署具有有利的性能权衡。 我们的架构通过将特定的编码器层作为退出头来改进文本到代码和代码到代码的搜索,其中更高层在训练改善中间表示时以最小的额外费用指导较早的层。 我们通过存储库级别的上下文损失进一步增强了 MoSE,从而最大限度地提高了培训上下文窗口的利用率。 此外,我们还发布了通过代码翻译创建的新数据集,该数据集扩展了具有跨语言代码对的代码对的文本到代码基准测试。 评估证明了自我蒸馏作为衡量各种代码理解任务准确性的标准方法的有效性。
随着软件系统的规模和复杂性急剧增加,确保其正确性、安全性和可靠性成为越来越艰巨的挑战。 尽管验证技术和工具取得了重大进展,但在将这些工具应用于复杂的现实世界场景时仍然存在困难。 为了解决这些困难,本文介绍了一种新的验证工具,称为合格C编程验证器(QCP)。 QCP采用精细化的前端 拟议的断言语言旨在阻碍验证工具,通过提高自动化来提高证明效率,并促进对程序及其验证结果的更深入了解。
在全球范围内处理在线旅行社需要高效灵活的软件解决方案架构。 当需要处理全球数千个代理和数十亿客户数据时。 微服务架构用于将大型程序分解为众多较小的服务,这些服务可以单独运行并执行单个任务。 本文分析并集成了独特的微服务云框架,旨在支持在线旅行平台(MCF-OTP)。 MCF-OTP的主要目标是通过云计算和微服务技术提高在线旅游平台的性能、灵活性和维护。 大型旅行应用程序,包括管理众多数据源,处理流量高峰和提供容错性,可以通过建议的框架来解决。 该框架增加了完美数据同步、微服务和基于需求技术的动态扩展之间的良好解释。 建议使用优化服务边界并最小化服务间依赖性的组织框架。 因此,这可能导致发展适应性的提高。 在这项研究中,主要目标是使用容错和响应时间的指标来评估MCF-OTP的效率。 调查结果表明,MCF-OTP结构在可靠性和可扩展性方面优于传统的单体设计,无缝管理流量峰值并减少停机时间。 具有成本效益的分析有助于确定启动费用和持续运营成本的净收益。 根据研究,基于云的环境用于降低断裂成本,这有助于提高资源分配的效率。
出现了两个概率论的高级“图片”:一个是随机变量概念的核心,一个是专注于分布和概率通道(Markov内核)。 虽然基于通道的图片已经成功地被公给公理化,并且被广泛推广,使用马尔可夫类别的概念,但随机变量图的分类语义仍然不太清楚。 辛普森的概率是最近的方法,其中允许随机变量等概率概念在样本空间的站点上有所不同。 辛普森在这些网站上发现了丰富的结构,最明显的是条件独立性的抽象概念,并给出了从数据库概率到名义集合的例子。 我们的目标是将这种发展与马尔可夫类别的一般性和抽象结合在一起:我们表明,对于任何合适的马尔可夫类别,可以定义一个满足辛普森公理的样本空间类别,并且概率棚理论可以在这个设置中纯粹合成地开发。 我们从著名的马尔可夫类别中以统一的方式恢复辛普森的例子,并考虑进一步的概括。
随着现代软件系统的规模和复杂性的扩展,与其建模和配方相关的挑战变得越来越复杂。 传统方法往往缺乏有效解决这些复杂性,特别是在诸如用于维护和评估的设计模式检测以及优化和长期可持续性的代码重构等任务中。 这种日益加剧的不足突出表明,在如何处理和解决这些挑战方面需要范式转变。 本文介绍了分析软件工程(ASE),这是一种新颖的设计范式,旨在平衡抽象,工具可访问性,兼容性和可扩展性。 ASE 能够有效建模和解决复杂的软件工程问题。 范式通过两个框架进行行为结构序列(BSS)和优化设计重构(ODR)评估,这两个框架都是根据ASE原则开发的。 BSS提供了紧凑的、与语言无关的代码库表示,以方便精确的设计模式检测。 ODR统一了人工制品和解决方案表示,通过方法优化代码重构,同时消除迭代计算开销。 通过提供针对软件设计挑战的结构化方法,ASE为未来编码和分析复杂软件指标的研究奠定了基础。
强化学习(RL)已被广泛采用,以提高大型语言模型(LLM)在Text-to-SQL任务上的性能。 然而,现有方法通常依赖于基于执行或基于LLM的Bradley-Terry奖励模型。 前者遭受重复数据库调用造成的高执行延迟,而后者则施加了大量的GPU内存开销,这两者都显着阻碍了RL管道的效率和可扩展性。 为此,我们提出了一个名为Graph-Reward-SQL的新型Text-to-SQL RL微调框架,它采用了GMNScore结果奖励模型。 我们利用 SQL 图形表示提供准确的奖励信号,同时显著减少推理时间和 GPU 内存使用情况。 在这一基础上,我们进一步引入了StepRTM,这是一种逐步奖励模型,为Common Table Expression(CTE)子查询提供中间监督。 这鼓励了 SQL 的功能正确性和结构清晰度。 包括Spider和BIRD在内的标准基准的广泛比较和消融实验证明,我们的方法始终优于现有的奖励模型。
文本序列化是现代计算中的一个基本概念,使复杂的数据结构能够转换为可以轻松存储、传输和重建的格式。 本文对文本序列化进行了广泛的概述,探讨了其重要性、流行格式、底层方法和比较性能特征。 我们深入研究了各种基于文本的序列化格式的优点和缺点,包括JSON,XML,YAML和CSV,检查它们的结构,可读性,冗长和适合不同的应用程序。 本文还讨论了序列化和反序列化过程中涉及的常见方法,例如解析技术和模式的作用。 为了说明选择序列化格式的实际意义,我们以表格的形式呈现假设的性能结果,根据序列化去序列化速度以及由此产生的数据大小等指标比较格式。 讨论分析了这些结果,强调了为特定用例选择文本序列化格式所涉及的权衡。 这项工作旨在为理解和应用各种计算领域的文本序列化提供全面的资源。
Tensor网络为压缩多维数据提供了强大的框架。 给定数据张量的最佳张量网络结构取决于数据特性和特定最优性标准,使张量网络结构搜索成为一个难题。 现有解决方案通常依赖于采样和压缩众多候选结构;这些程序计算成本很高,因此限制了实际应用。 我们通过将张量网络结构搜索视为程序合成问题并引入基于约束的高效评估方法来应对这一挑战,该方法避免了代价高昂的张量分解。 具体来说,我们在转换程序和网络结构之间建立对应关系。 我们还设计了一个名为输出导向拆分的新操作,以减少搜索空间,而不会阻碍表现力。 然后,我们提出了一个综合算法,通过约束解决来识别有前途的网络候选者,并避免除了最有希望的候选者之外的所有张量分解。 实验结果表明,我们的方法将搜索速度提高了10×,并且比最先进的压缩比提高了1.5×到3×。 值得注意的是,我们的方法扩展到以前工作无法实现的更大的张量。 此外,发现的拓扑结构很好地推广到类似的数据,比通用结构的压缩比好2.4×,而运行时保持在110秒左右。
大型语言模型(LLM)已成为传统静态程序分析方法的一种有希望的替代方案,例如符号执行,提供直接推理代码的能力,而无需依赖定理证明者或SMT求解器。 然而,LLM本质上也是概率性的,因此在实际应用中分析的准确性和规模方面面临重大挑战。 这些问题通常需要使用具有更高令牌限制的大型LLM,但这需要企业级硬件(GPU),从而限制了许多用户的可访问性。 在本文中,我们提出了基于LLM的符号执行 - 一种新颖的方法,通过基于路径的程序分析任务分解为更小(更易于处理的)子任务来增强LLM推理。 核心思想是使用基于通用代码的表示来概括路径约束,LLM可以直接推理,并且不翻译成另一种(不太表达)的形式语言。 我们以AutoExe的形式实现我们的方法,AutoExe是一个基于LLM的符号执行引擎,轻量级且与语言无关,使其成为分析传统方法具有挑战性的代码的实用工具。 我们表明,AutoExe可以提高基于LLM的程序分析的准确性和规模,特别是对于可以在消费级硬件上运行的小型LLM。