检索结果-内蒙古大学图书馆

International Workshop on Structured Object-Oriented Formal Language and Method, SOFL+MSVL 2020

作者： Zhao, Liang Feng, Zhe Wang, Xiaobing Shu, Xinfeng Institute of Computing Theory and Technology ISN Laboratory Xidian University Xi’an710071 China School of Computer Science and Technology Xi’an University of Posts and Telecommunications Xi’an710061 China

ISBN: (纸本)9783030774738

With the rapid development and wide application of artificial neural networks, formal modeling and verification of their security become more and more significant. As a basic step towards the direction, this work proposes a comprehensive modeling framework for back propagation (BP) neural networks based on the formal language MSVL. In this framework, the structure and behavior of a BP neural network are formalized as specifications of data structures and operations, and they are in turn implemented as MSVL structs and functions, respectively. Based on the formalization, models of BP neural networks can be constructed and trained according to the requirements of users. Experimental results show that these models have good performance in terms of metrics concerning training and prediction such as loss and accuracy. © 2021, Springer Nature Switzerland AG.

关键词： Formal verification

来源：评论

学校读者我要写书评

暂无评论

Propositional Projection Temporal Logic Specification Mining 14th

Propositional Projection Temporal Logic Specification Mining

引用

14th International Conference on Combinatorial Optimization and Applications, COCOA 2020

作者： Zhang, Nan Yuan, Xiaoshuai Duan, Zhenhua Institute of Computing Theory and Technology and ISN Laboratory Xidian University Xi’an710071 China

ISBN: (纸本)9783030648428

This paper proposes a dynamic approach of specification mining for Propositional Projection Temporal Logic (PPTL). To this end, a pattern library is built to collect some common temporal relation among events. Further, several algorithms of specification mining for PPTL are designed. With our approach, PPTL specifications are mined from a trace set of a target program by using patterns in the library. In addition, a specification mining tool PPTLMiner supporting this approach is developed. In practice, given a trace set and user selected patterns, PPTLMiner can capture PPTL specifications of target programs. © 2020, Springer Nature Switzerland AG.

关键词： Temporal logic

来源：评论

学校读者我要写书评

暂无评论

Dynamical-invariant-based holonomic quantum gates:theory and experiment

引用

Fundamental Research 2023年第2期3卷 229-236页

作者： Yingcheng Li Tao Xin Chudan Qiu Keren Li Gangqin Liu Jun Li Yidun Wan Dawei Lu State Key Laboratory of Surface Physics Department of PhysicsCenter for Field Theory and Particle Physicsand Institute for Nanoelectronic devices and Quantum computingFudan UniversityShanghai 200433China Shanghai Qi Zhi Institute Shanghai 200030China Shenzhen Institute for Quantum Science and Engineering and Department of Physics Southern University of Science and TechnologyShenzhen 518055China d Guangdong Provincial Key Laboratory of Quantum Science and Engineering Shenzhen 518055GuangdongChina Center for Quantum Computing Peng Cheng LaboratoryShenzhen 518055China Institute of Physics Chinese Academy of SciencesBeijing 100190China

Among existing approaches to holonomic quantum computing,the adiabatic holonomic quantum gates(HQGs)suffer errors due to decoherence,while the non-adiabatic HQGs either require additional Hilbert spaces or are difficult to ***,we report a systematic,scalable approach based on dynamical invariants to realize HQGs without using additional Hilbert *** presenting the theoretical framework of our approach,we design and experimentally evaluate single-qubit and two-qubits HQGs for the nuclear magnetic resonance *** single-qubit gates acquire average fidelity 0.9972 by randomized benchmarking,and the controlled-NOT gate acquires fidelity 0.9782 by quantum process *** approach is also platform-independent,and thus may open a way to large-scale holonomic quantum computation.

关键词： Geometric gates Dynamical invariant Nuclear magnetic resonance Holonomic gates Platform-independent

来源：评论

学校读者我要写书评

暂无评论

Experimental quantum simulation of a topologically protected Hadamard gate via braiding Fibonacci anyons

引用

The Innovation 2023年第5期4卷 41-46页

作者： Yu-ang Fan Yingcheng Li Yuting Hu Yishan Li Xinyue Long Hongfeng Liu Xiaodong Yang Xinfang Nie Jun Li Tao Xin Dawei Lu Yidun Wan Shenzhen Institute for Quantum Science and Engineering and Department of Physics Southem University of Science and Technology Shenzhen 518055China State Key Laboratory of Surface Physics Department of PhysicsCenter for Field Theory and Particle Physicsand Institute for Nanoelectronic Devices and Quantum ComputingFudan UniversityShanghai 200433and Shanghai Qi Zhi InstituteShanghai 200030China School of Physics Hangzhou Normal UniversityHangzhou 311121China

Topological quantum computation(TQC)is one of the most striking architectures that can realize fault-tolerant quantum *** TQC,the logical space and the quantum gates are topologically protected,i.e.,robust against local *** topological protection,however,requires complicated lattice models and hard-to-manipulate dynamics;even the simplest system that can realize universal TQC-the Fibonacci anyon system—lacks a physical realization,let alone braiding the non-Abelian ***,we propose a disk model that can simulate the Fibonacci anyon system and construct the topologically protected logical spaces with the Fibonacci *** braiding the Fibonacci anyons,we can implement universal quantum gates on the logical *** disk model merely requires two physical qubits to realize three Fibonacci anyons at the *** 15 sequential braiding operations,we construct a topologically protected Hadamard gate,which is to date the least-resource requirement for *** showcase,we implement a topological Hadamard gate with two nuclear spin qubits,which reaches 97.18%fidelity by randomized *** further prove by experiment that the logical space and Hadamard gate are topologically protected:local disturbances due to thermal fluctuations result in a global phase *** a platform-independent proposal,our work is a proof of principle of TQC and paves the way toward fault-tolerant quantum computation.

关键词： Fibonacci Hadamard TQC

来源：评论

学校读者我要写书评

暂无评论

Using Experience Classification for Training Non-Markovian Tasks

arXiv

引用

arXiv 2023年

作者： Miao, Ruixuan Lu, Xu Tian, Cong Yu, Bin Duan, Zhenhua Institute of Computing Theory and Technology State Key Laboratory of Integrated Services Networks Xidian University China

Unlike the standard Reinforcement Learning (RL) model, many real-world tasks are non-Markovian, whose rewards are predicated on state history rather than solely on the current state. Solving a non-Markovian task, frequently applied in practical applications such as autonomous driving, financial trading, and medical diagnosis, can be quite challenging. We propose a novel RL approach to achieve non-Markovian rewards expressed in temporal logic LTLf (Linear Temporal Logic over Finite Traces). To this end, an encoding of linear complexity from LTLf into MDPs (Markov Decision Processes) is introduced to take advantage of advanced RL algorithms. Then, a prioritized experience replay technique based on the automata structure (semantics equivalent to LTLf specification) is utilized to improve the training process. We empirically evaluate several benchmark problems augmented with non-Markovian tasks to demonstrate the feasibility and effectiveness of our approach. Copyright © 2023, The Authors. All rights reserved.

关键词： Reinforcement learning

来源：评论

学校读者我要写书评

暂无评论

Distributed exact Grover’s algorithm

引用

Frontiers of physics 2023年第5期18卷 255-279页

作者： Xu Zhou Daowen Qiu Le Luo Institute of Quantum Computing and Computer Theory School of Computer Science and EngineeringSun Yat-sen UniversityGuangzhou 510006China The Guangdong Key Laboratory of Information Security Technology Sun Yat-sen UniversityGuangzhou 510006China School of Physics and Astronomy Sun Yat-sen UniversityZhuhai 519082China QUDOOR Co Ltd.Beijing 100089China

Distributed quantum computation has gained extensive *** this paper,we consider a search problem that includes only one target item in the unordered *** that,we propose a distributed exact Grover’s algorithm(DEGA),which decomposes the original search problem into■n/2■***,(i)our algorithm is as exact as the modified version of Grover’s algorithm by Long,which means the theoretical probability of finding the objective state is 100%;(ii)the actual depth of our circuit is 8(n mod 2)+9,which is less than the circuit depths of the original and modified Grover’s algorithms,1+8■π/4√2^(n)■and 9+8■π/4√2^(n)-1/2■,*** only depends on the parity of n,and it is not deepened as n increases;(iii)we provide particular situations of the DEGA on MindQuantum(a quantum software)to demonstrate the practicality and validity of our *** our circuit is shallower,it will be more resistant to the depolarization channel noise.

关键词： distributed quantum computation search problem distributed exact Grover’s algorithm(DEGA) MindQuantum the depolarization channel noise

来源：评论

学校读者我要写书评

暂无评论

Graph Convolutional Network Robustness Verification Algorithm Based on Dual Approximation 1

引用

25th International Conference on Formal Engineering Methods, ICFEM 2024

作者： An, Dongdong Zhang, Hao Zhao, Qin Liu, Jing Shi, Jianqi Huang, Yanhong Yang, Yang Liu, Xu Qin, Shengchao Shanghai Engineering Research Center of Intelligent Education and Bigdata Shanghai Normal University Shanghai200234 China Shanghai Key Laboratory of Trustworthy Computing East China Normal University Shanghai200062 China Shanghai Formal-Tech Information Technology Co. LTD. Shanghai China Guangzhou Institute of Technolog Xidian University Shaanxi China ICCT and ISN Laboratory Xidian University Shaanxi China

ISBN: (数字)9789819606177

ISBN: (纸本)9789819606160

With the continuous development of Graph Neural Network (GNN) technologies, securing their robustness is crucial for their broad adoption in practical applications. Although various verification methods for training GNNs have been proposed, studies indicate that Graph Convolutional Networks (GCNs) remain vulnerable to adversarial attacks affecting both graph structure and node attributes. We propose a novel approach to verify the robustness of GCNs against perturbations in node attributes by employing a dual approximation technique to convexify nonlinear activation functions. This transformation changes the original non-convex problem into a more manageable convex forms. We start by applying linear relaxation to convert fixed-value features in each GCN layer into variables suitable for optimization. Next, we reframe the task of identifying the worst-case margin for a graph as a linear problem, which we solve using linear programming techniques. Given the discrete nature of graph data, we define a perturbation space that extends the data domain from discrete to continuous values. To improve the accuracy of the convex relaxation, we use a dual approximation algorithm to set bounds on the optimizable variables. Our method certifies the robustness of nodes against perturbations within a specified range and significantly improves verification accuracy compared to previous approaches. This method surpasses previous work in verification accuracy and is distinctively tailored to address the S-curve, an aspect less explored in prior research. Experimental results show that our method significantly refines the precision of robustness verification for GCNs. © The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2024.

关键词： Convolutional neural networks

来源：评论

学校读者我要写书评

暂无评论

Verifying a Carry Look-Ahead Adder with Propositional Projection Temporal Logic

引用

Chinese Journal of Electronics 2023年第1期22卷 21-24页

作者： Nan Zhang Zhenhua Duan Cong Tian Institute of Computing Theory and Technology Xidian University Xi'an China National Key Laboratory on Integrated Services Network Xidian University Xi'an China

This paper presents a case study for verifying a carry look-ahead adder using the axiom system of Propositional projection temporal logic (PPTL). To this end, the syntax, semantics and axiom system of PPTL are briefly introduced. Further, functions and architectures of the carry look-ahead adder are presented. In addition, four lemmas are proved with the axiom system of PPTL. Finally, the correctness of the adder is verified based on the lemmas and the axiom system of PPTL. The case study shows that the axiom system for PPTL is workable.

关键词： Protocols Semantics Computer architecture Syntactics Hardware Software Intserv networks

来源：评论

学校读者我要写书评

暂无评论

AutoSketch: automatic sketch-oriented compiler for query-driven network telemetry 24

AutoSketch: automatic sketch-oriented compiler for query-dri...

引用

Proceedings of the 21st USENIX Symposium on Networked Systems Design and Implementation

作者： Haifeng Sun Qun Huang Jinbo Sun Wei Wang Jiaheng Li Fuliang Li Yungang Bao Xin Yao Gong Zhang National Key Laboratory for Multimedia Information Processing School of Computer Science Peking University Institute of Computing Technology CAS Northeastern University China Huawei Theory Department

ISBN: (纸本)9781939133397

Recent network telemetry witnesses tremendous progress in two directions: query-driven telemetry that targets expressiveness as the primary goal, and sketch-based algorithms that address resource-accuracy trade-offs. In this paper, we propose AutoSketch that aims to integrate the advantages of both classes. In a nutshell, AutoSketch automatically compiles high-level operators into sketch instances that can be readily deployed with low resource usage and incur limited accuracy drop. However, there remains a gap between the expressiveness of high-level operators and the underlying realization of sketch algorithms. AutoSketch bridges this gap in three aspects. First, AutoSketch extends its interface derived from existing query-driven telemetry such that users can specify the desired telemetry accuracy. The specified accuracy intent will be utilized to guide the compiling procedure. Second, AutoSketch leverages various techniques, such as syntax analysis and performance estimation, to construct efficient sketch instances. Finally, AutoSketch automatically searches for the most suitable parameter configurations that fulfill the accuracy intent with minimum resource usage. Our experiments demonstrate that AutoSketch can achieve high expressiveness, high accuracy, and low resource usage compared to state-of-the-art telemetry solutions.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Analysis of the gluon distribution with next-to-leading order splitting function at small-x^(*)

引用

Chinese Physics C 2024年第6期48卷 38-44页

作者：陈京萱王晓鹏蔡燕兵陈旭荣王倩 Key Laboratory of Atomic and Subatomic Structure and Quantum Control(MOE) Guangdong Basic Research Center of Excellence for Structure and Fundamental Interactions of MatterInstitute of Quantum MatterSouth China Normal UniversityGuangzhou 510006China Guangdong-Hong Kong Joint Laboratory of Quantum Matter Guangdong Provincial Key Laboratory of Nuclear ScienceSouthern Nuclear Science Computing CenterSouth China Normal UniversityGuangzhou 510006China Institute of Modern Physics Chinese Academy of SciencesLanzhou 730000China University of Chinese Academy of Sciences Beijing 100049China Lanzhou University Lanzhou 730000China School of Nuclear Science and Technology University of Chinese Academy of SciencesBeijing 100049China Guizhou Key Laboratory in Physics and Related Areas Guizhou University of Finance and EconomicsGuiyang 550025China Southern Center for Nuclear-Science Theory(SCNT) Institute of Modern PhysicsChinese Academy of SciencesHuizhou 516000China

An approximated solution for the gluon distribution from DGLAP evolution equations with the NLO splitting function in the small-x limit is *** first obtain simplified forms of the LO and NLO splitting functions in the small-x *** these approximated splitting functions,we obtain the analytical gluon distribution using the Mellin *** free parameters in the boundary conditions are obtained by fitting the CJ15 gluon distribution *** find that the asymptotic behavior of the gluon distribution is consistent with the CJ15 data;however,the NLO results considering the"ladder"structure of gluon emission are slightly better than the LO *** results indicate that the corrections from NLO have a significant influence on the behavior of the gluon distribution in the small-x *** addition,we investigate the DGLAP evolution of the proton structure function using the analytical solution of the gluon *** differential structure function reveals that our results have a similar tendency to the CJ15 data at small-x.

关键词： DGLAP equation gluon distribution small-x structure function

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：