AI基础研究具身智能 AI金融

本网站上的内容仅供参考，不提供医疗或其他专业建议，不代表活水快报、贡献者或合作伙伴的观点。

© 2024-2025 活水快报 - 42Digest.

|

京ICP备2024044642号-15

计算机科学中的逻辑研究快报

相关分类

计算机科学

Computer Science

人工智能

Artificial Intelligence

计算与语言

Computation and Language

计算复杂性

Computational Complexity

计算机科学

Computer Science

人工智能

Artificial Intelligence

计算与语言

Computation and Language

计算复杂性

Computational Complexity

最新研究

Parikh Automata 关于有限和无限字

我们研究Parikh自动机在有限和无限的单词。首先,我们在有限词上为Parikh自动机建立了一些结果。接下来,我们介绍了Parikh自动机在无限单词上的几个定义。我们考虑了确定性和非确定性变体,并研究闭包属性,表现力和常见决策问题,用于模型检查的应用程序。此外,我们将我们的模型与其他模型进行比较,计算机制在无限单词上运行。

形式语言与自动机理论计算机科学中的逻辑

用于 QBF 的半代数证明系统

我们为量化布尔公式(QBF)引入了新的半代数证明系统,类似于Nullstellensatz,Shereali-Adams和Sum-of-Squares的命题系统。我们从QBF文献(策略提取)和命题证明复杂性(大小度关系和伪期望)转移到这种设置技术。我们获得许多强大的QBF下界和这些系统之间的分离,即使无视命题硬度。

计算机科学中的逻辑计算复杂性逻辑学

HHLPar:用于并行混合通信顺序过程的自动定理支持器

我们提出了一个名为 HHLPar 的工具,用于验证以混合通信顺序过程 (HCSP) 建模的混合系统。 HHLPar建立在HCSP的混合嘶吱逻辑之上,该逻辑学能够推理微分方程的连续时间特性,以及并行HCSP过程的通信和并行组成,并具有参数化痕量计及其同步。该逻辑在Isabelle/HOL中是正式的,并且被证明是合理的,这构成了HHLPar进行的验证的可信赖的基础。 HHLPar在Python中实现了混合嗤疮逻辑,并支持自动验证:一方面,它提供了符号分解HCSP过程的功能,为单独的顺序过程生成规范,然后通过同步编写它们,以获得整个并行HCSP过程的最终规范;另一方面,它与外部求解器集成,用于处理微分方程和真实算术属性。我们已经对简化的巡航控制系统进行了实验,以验证该工具的性能。

计算机科学中的逻辑

令人信服的论点扩展是微弱的可接受,但不是相反

在本研究说明中,我们展示了两种不可接受的参数框架语义之间的关系:有说服力的和弱可接受的语义。我们证明,虽然令人信服的扩展是微弱的可接受性,但相反的情况并非如此。

人工智能计算机科学中的逻辑

约束和稳健的政策与满意度-Modulo-Probabilistic-Model-Checking

为给定和已知的有限马尔可夫决策过程(MDP)计算奖励最优策略的能力支持了跨规划、控制器合成和验证的各种应用。然而,我们通常希望政策(1)是稳健的,即,它们对MDP的扰动表现良好,(2)满足有关其表示或实施成本的额外结构性限制。计算这种强大和受限的策略在计算上确实更具挑战性。本文提供了第一个使用灵活和高效的框架有效计算受任意结构约束的稳健策略的方法。我们通过允许在一组MDP上一阶理论中表达我们的限制来实现灵活性,而我们效率的根源在于可满足性求解器的紧密集成,以处理问题的组合性质和概率模型检查算法来处理MDP的分析。对几百个基准的实验证明了受限和稳健的政策综合的可行性,以及针对问题的各种片段采用最先进的方法的竞争力。

计算机科学中的逻辑人工智能

人工智能如何导致知识为什么:亚里士多德后分析启发的探究

贝叶斯网络和因果模型提供了处理有关外部干预和反事实的查询的框架,使任务超出了概率分布本身可以解决的范围。虽然这些形式主义通常被非正式地描述为捕获因果知识,但缺乏一种正式的理论,表征预测外部干预效果所需的知识类型。这项工作引入了因果系统的理论框架,以澄清亚里士多德在人工智能中的知识和知识之间的区别。通过将现有的人工智能技术解释为因果系统,它调查了相应的知识类型。此外,它认为,预测外部干预的影响是可行的,只有了解原因,提供更精确的理解,必要的知识为此类任务。

人工智能计算机科学中的逻辑

自然语言形式化和验证的神经符号化方法

大型语言模型在自然语言解释和推理方面表现良好,但其固有的随机性限制了其在受监管行业的采用,如在严格政策下运作的金融和医疗保健行业。为了解决这一限制,我们提出了一个两阶段的神经符号框架,该框架(1)使用具有可选的人类指导的LLM来正式化自然语言策略,允许对形式化过程进行精细控制,(2)使用推理时间自动形式化来验证自然语言语句的逻辑正确性。当正确性至关重要时,我们在推理时执行多个冗余形式化步骤,交叉检查语义等价的正态化。我们的基准表明,我们的方法超过99%的稳健性,表明在识别逻辑有效性方面几乎为零的误报率。我们的方法产生可审计的逻辑工件,以证实验证结果,并可用于改进原始文本。

计算与语言人工智能机器学习计算机科学中的逻辑

量子模态逻辑

基于量子逻辑的模态逻辑以最简单的形式形式化。具体来说,提供了关系语义和隐性微积分,并证明了连接这两个概念的健全性和完整性定理。该框架旨在作为将量子逻辑的各种模态逻辑形式化的基础,例如量子极化逻辑、量子时间逻辑、量子认识论逻辑和量子动态逻辑。

计算机科学中的逻辑逻辑学

首行公理系统 E_d 和 E_da 扩展 Tarski 的 E_2 与定量欧几里得几何的距离和角度函数符号

Tarski 的 E_2 欧几里得几何学一阶公理系统 E_2 以其完整性和可判定性而著称。然而,毕达哥拉斯定理 - 无论是在其现代代数形式 a^2+b^2=c^2 还是在欧几里德的元素中 - 都不能直接用E_2表示,因为距离和面积都不是E_2语言中的原始概念。在本文中,我们引入了一种双排序语言的替代公理系统 E_d ,它以双位距离函数 d 作为唯一的几何原语。我们还介绍了它的保守扩展E_da,其中还包含一个三位角函数a。该系统 E_d 有两个显著特征:它简单(具有单一的几何原始),并且是定量的。数值距离可以用这种语言直接表达。相似性公理在 E_d 中起着核心作用,用一块石头有效地杀死两只鸟:它为比例和相似性理论提供了严谨的基础,它暗示了欧几里德的平行姿势(EPP)。相似性公理可以看作是EPP的定量表述。毕达哥拉斯定理和相似性理论的其他定量结果可以直接用E_d和E_da的语言表达,激励了Quantitative Euclidean Geometry的名称。传统的分析几何学可以在E_d的合成几何学下统一。也就是说,解析几何学不被视为E_d的模型,而是其语句可以用E_d的语言表示为一阶形式句子。系统 E_d 被证明是一致、完整和可决定的。最后,我们将理论扩展到高维度的双曲几何和欧几里得几何。

逻辑学计算机科学中的逻辑度量几何

认证分行和边界 MaxSAT 解决方案(扩展版本)

在过去的几十年中,组合式求解器已经看到了显着的性能改进,使他们能够在实际应用中实际应用。在其中一些应用程序中,确保求解器输出的正确性至关重要。然而,现代求解器的复杂性使他们容易受到源代码中的错误。在可理解性检查(SAT)领域,这个问题已通过证明记录来解决,其中求解器生成其答案的正确性的正式证明。对于更多的表现问题,如 SAT 的优化变体 MaxSAT,证明日志记录直到最近才出现类似的突破。在本文中,我们展示了如何在Branch-and-Bound MaxSAT解决中实现最先进的技术证明日志记录。这包括验证此类算法中使用的超前瞻方法,以及基于所谓的多有价值决策图(MDD)的伪布尔约束的高级类法规编码。我们在主要的分支和绑定求解器MaxCDCL中实现这些想法,并实验证明证明日志记录在有限的开销下是可行的,而证明检查仍然是一个挑战。

计算机科学中的逻辑

扩散拍卖的正式验证

在扩散拍卖中,卖家可以利用底层社交网络来扩大参与,从而增加他们的潜在收入。具体来说,卖家可以激励参与者通过网络传播有关拍卖的信息。虽然文献中最近研究了此类拍卖的许多变体,但正式验证和战略推理观点尚未进行调查。我们的贡献是三倍。首先,我们引入一种逻辑形式主义,捕捉扩散的动态及其战略维度。其次,对于这样的逻辑,我们提供模型检查程序,允许一个人验证属性作为纳什均衡,并为检查卖家策略的存在铺平道路。第三,我们为呈现的算法建立计算复杂性结果。

计算机科学与博弈论计算机科学中的逻辑

神经网络验证中的证明最小化

深度神经网络(DNN)的广泛采用需要验证其安全性的有效技术。 DNN验证器是复杂的工具,可能包含可能损害其健全性并破坏验证过程可靠性的bug。使用证明可以减轻这种担忧:由外部和可靠的证明检查器可检查的工件,并证明验证过程的正确性。然而,这种证明往往非常大,限制了它们在许多情况下的使用。在这项工作中,我们通过最小化DNN验证器产生的不满足性证明来解决这个问题。我们提出了删除在验证过程中学到的事实的算法,但对于证明本身来说是不必要的。从概念上讲,我们的方法分析了用于推断UNSAT的事实之间的依赖关系,并删除没有贡献的事实。然后,我们通过使用两个替代程序,消除剩余的不必要的依赖关系,进一步最小化了证明。我们在生成 DNN 验证器的证明之上实现了我们的算法,并在几个基准测试中对其进行了评估。我们的结果表明,我们表现最佳的算法将证明大小减少了37%-82%,验证检查时间减少了30%-88%,同时为验证过程本身引入了7%-20%的运行时开销。

计算机科学中的逻辑机器学习

蒙纳迪奇和受保护的二订单逻辑的数据日志可表达性

我们描述了Monadic二阶逻辑(MSO)中的句子,这些句子在存在鹅卵石游戏中等同于Datalog程序的有限结构。我们还表明,对于可以在MSO中表达并在同态下关闭的每个类有限结构的C类,对于所有整数l,k,在Feder和Verdi的意义上存在一个规范的宽度(l,k)数据程序Pi。相同的特征也适用于受保护的二阶逻辑(GSO),它正确地扩展了MSO。为了证明我们的结果,我们表明GSO中的每一个C类,其补充在同态下是约束满意度问题(CSP)的有限结合,可数分类结构。众所周知,MSO和Datalog的交集包含嵌套monadically定义查询(Nemodeq)的类;同样,我们表明GSO和Datalog的交集包含所有可以通过嵌套保护查询的更富有表现力的语言表达的问题。然而,通过利用我们的结果,我们可以证明这两种查询语言都不能作为表征,因为我们在MSO和Datalog的交叉中展示了一个在嵌套保护查询中无法表达的查询。

计算机科学中的逻辑计算复杂性逻辑学

TurboSAT:在GPU-CPU混合系统上加速的梯度引导布尔满意度

虽然加速计算已经改变了许多计算领域,但它对逻辑推理的影响,特别是布尔的可满足性(SAT),仍然有限。最先进的SAT求解器在很大程度上依赖于固有的顺序冲突驱动的搜索算法,这些算法提供了强大的启发式,但限制了并行性的数量,否则可以实现更具可扩展性的SAT解决。受神经网络训练的启发,我们将SAT问题制定为双线性矩阵乘法层,可以使用可微分的客观函数进行优化。通过这种编码,我们结合了并行可微分优化和顺序搜索的优势,以加速混合GPU-CPU系统的SAT。在这个系统中,GPU利用并行可微解来快速评估SAT子句,并使用梯度来随机探索解决方案空间并优化变量分配。 GPU 生成的有希望的部分赋值是在许多 CPU 线程上进行后处理的,这些线程利用冲突驱动的顺序搜索来进一步遍历解决方案子空间并识别完整的分配。在 NVIDIA DGX GB200 节点上对混合求解器进行原型,与 SAT 竞赛中基于公共可满足基准问题的最先进的基于 CPU 的求解器相比,我们的求解器实现了高达 200 倍的运行时速度。

计算机科学中的逻辑人工智能机器学习数学软件

Horn公式方程的抽象定点定理

我们考虑一阶逻辑中的一类公式方程,Horn公式方程,这是由对谓词变量发生的句法限制定义的。角方程在计算机科学的许多应用中发挥着重要作用。我们用最少的定点运算符在一阶逻辑中对 Horn 公式方程进行定点定理。我们的定点定理是抽象的,因为它适用于概括标准语义的抽象语义。我们描述了这个定点定理在计算逻辑的各个领域的几个推论,从程序验证的逻辑基础到归纳定理证明。

计算机科学中的逻辑逻辑学

基于输入的三值抽象精炼

与反例引导抽象精炼(CEGAR)不同,三有价值的抽象精炼(TVAR)能够验证mu-calculus的所有属性。我们为TVAR提出了一种新的算法框架,它采用类似模拟器的方法,通过基于输入的拆分来构建和完善抽象状态空间。这导致了一种状态空间形式主义,它比以前使用模态转换的TVAR框架要简单得多。我们在AVR架构的机床检查和机器代码系统的验证属性中实现了框架,展示了验证系统和mu-calculus属性的能力,这些属性不是通过天真的模型检查或CEGAR分别可以验证的。这是 TVAR 首次用于机器代码验证。

计算机科学中的逻辑

代理人意识的Epistemic Perspective

该论文建议将代理意识作为一种知识形式,打破现有文献中关于意识的传统。它区分了这种知识的de re和de dicto形式。这项工作引入了两种模式捕获这些形式,并使用2D语义版本正式指定其含义。主要的技术结果是描述两种拟议模式与标准“对事实的认识”模式之间的相互作用的健全和完整的逻辑系统。

人工智能计算机科学中的逻辑多智能体系统

使用许可 Oracle 语言模型中的 Steming 幻觉

语言模型表现出非凡的自然语言生成能力,但仍然容易产生幻觉,尽管产生了语法上一致的反应,却产生了事实上不正确的信息。本研究介绍了许可Oracle,这是一种架构解决方案,旨在通过对结构化知识图进行正式验证来强制实施真理约束来遏制LM中的幻觉。与依赖数据扩展或微调的统计方法不同,许可 Oracle 在模型的生成过程中嵌入了确定性验证步骤,确保只提出事实准确的声明。我们通过实验评估了许可Oracle的有效性,并将其与几种最先进的方法进行比较,包括基线语言模型生成,事实召回的微调,对弃权行为的微调和检索增强生成(RAG)。我们的结果表明,虽然RAG和微调提高了性能,但它们未能消除幻觉。相比之下,许可Oracle实现了完美的弃权精度(AP = 1.0)和零错误答案(FAR-NE = 0.0),确保仅生成有效的声明,在事实响应中准确率为89.1%。这项工作表明,架构创新,如许可甲骨文,为具有结构化知识表示的域中的幻觉提供了必要和足够的解决方案,提供了统计方法无法匹配的保证。尽管许可Oracle专门用于解决基于事实领域的幻觉,但其框架为未来AI系统中受真相限制的生成奠定了基础,为可靠的,基于认识的模型提供了新的途径。

计算与语言人工智能机器学习计算机科学中的逻辑

具有连接条件的平面图和平面线性正 λ 期之间的双子

线性λ-term的枚举最近引起了相当多的关注,部分原因是它们与组合图的联系。 Zeilberger和Giorgetti(2015)在平面线性正 λ-terms 和平面图之间进行了递归双击,当限制为2个连接的λ-terms(即没有封闭的子术语)时,会导致无桥平面图。受此限制的启发,Zeilberger和Reed(2019)推测,3连接的平面线性正常λ-terms与双部分平面图具有相同的计数公式。在这篇文章中,我们通过在这两个家庭之间进行直接的争吵来解决这个猜想。此外,使用类似的方法,我们在平面线性正态λ-terms和平面图之间给出直接的双子,其限制为2连接的λ-term导致无环平面图。这种双击似乎与Zeilberger和Giorgetti不同,即使在采取地图双重之后。我们还探讨了我们的双击的列举后果。

组合数学计算机科学中的逻辑

并行系统的一般安全保护精炼

众所周知,确保遵守信息流安全(IFS)具有挑战性,特别是对于具有大型代码库(如多核操作系统(OS)内核)的并发系统。精炼,它验证了一个实现保留了一个更抽象的规范的某些属性,对于应对这些挑战很有希望。然而,就基于改进的安全属性验证而言,现有技术仍然仅限于顺序系统,或者缺乏捕获并发系统复杂安全策略所需的表现力。在这项工作中,我们展示了一种通用的安全保护改进技术,特别是用于验证受潜在复杂安全策略支配的并发系统的IFS。我们正式化了并发系统的 IFS 属性,并提出了基于精细化的组合方法,以证明广义的安全属性(例如,非瞬态互不干涉)在实现和抽象之间保留。与以前的细化工作相比,实现这种推理的关键直觉是建立实现和抽象之间的逐步映射关系,这足以确保安全策略允许或禁止每个配对的步骤(分别在抽象和实现中)。我们采用我们的方法,根据一系列安全政策验证两个非平凡的案例研究。我们的证明在Isabelle/HOL中完全机械化,在此期间,我们发现ARINC 653单核标准先前报告的两个秘密通道也存在于ARINC 653多核标准中。我们随后证明了修订机制的正确性,展示了我们方法的有效性。

计算机科学中的逻辑密码学与安全

继续滚动加载更多