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

41st International Conference on Machine Learning, ICML 2024

作者： Wei, Siwei Zhang, Xudong Zhou, Zhiyang Cai, Yan State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences University of Chinese Academy of Sciences Beijing China

The application of machine learning methods to solve combinatorial problems has garnered considerable research interest. In this paper, we propose MAGG (Metamorphic Aggregation), a method to augment machine learning models for combinatorial problems at inference time using metamorphic relations. MAGG models metamorphic relations using directed graphs, which are then fed to a Graph Neural Network (GNN) model to improve the aggregation of predictions across transformed input instances. By incorporating metamorphic relations, MAGG essentially extends standard Test-Time Augmentation (TTA), eliminating the necessity of label-preserving transformations and expanding its applicability to a broader range of supervised learning tasks for combinatorial problems. We evaluate the proposed MAGG method on three mainstream machine learning tasks for combinatorial problems, namely Boolean Satisfiability Prediction (SAT), Decision Traveling Salesman Problem Satisfiability Prediction (Decision TSP), and Graph Edit Distance Estimation (GED). The evaluation result shows significant improvements over base models in all three tasks, corroborating the effectiveness and versatility of the proposed method. Copyright 2024 by the author(s)

关键词： Directed graphs

来源：评论

学校读者我要写书评

暂无评论

Exponential Time Complexity of the Complex Weighted Boolean #CSP 29th

Exponential Time Complexity of the Complex Weighted Boolea...

引用

29th International Computing and Combinatorics Conference, COCOON 2023

作者： Liu, Ying State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences University of Chinese Academy of Sciences Beijing China

ISBN: (纸本)9783031491894

Cai, Lu, and Xia [8] proved a dichotomy for complex weighted Boolean #CSP. If the parameter set of Boolean constraint functions F is a subset of either of the affine-type function set A and the product type function set P, then #CSP(F ) is polynomial-time solvable;otherwise, #CSP(F ) is #P-hard. Furthermore, the result holds for # R3 -CSP(F ), which additionally restricts every variable constrained by no more than 3 constraint functions (not necessarily distinct). We strengthen the #P-hardness to the tight sub-exponential time lower bound under the counting Exponential Time Hypothesis (#ETH). We demonstrate that, if #ETH holds, then #CSP(F ) with F A and F P has no sub-exponential time algorithm. The result also holds for # RD -CSP(F ) with some integer D> 0, even D= 3. Additionally, we demonstrate that a vital tool pinning, forcing some variables to be 0 or 1, is still available in the context of # RD -CSP when proving the sub-exponential time lower bound. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.

关键词： Polynomial approximation

来源：评论

学校读者我要写书评

暂无评论

Model Checking for Probabilistic Multiagent Systems

引用

Journal of computer science & Technology 2023年第5期38卷 1162-1186页

作者：付辰 Andrea Turrini 黄小炜宋磊冯元张立军 State Key Laboratory of Computer Science Institute of SoftwareChinese Academy of SciencesBeijing 100190China University of Chinese Academy of Sciences Beijing 100049China Institute of Intelligent Software Guangzhou 511455China Department of Computer Science University of LiverpoolLiverpool L693BXU.K Microsoft Research Beijing 100190China Centre for Quantum Software and Information University of Technology SydneySydney 2007Australia

In multiagent systems,agents usually do not have complete information of the whole system,which makes the analysis of such systems *** incompleteness of information is normally modelled by means of accessibility relations,and the schedulers consistent with such relations are called *** this paper,we consider probabilistic multiagent systems with accessibility relations and focus on the model checking problem with respect to the probabilistic epistemic temporal logic,which can specify both temporal and epistemic ***,the problem is undecidable in *** show that it becomes decidable when restricted to memoryless uniform ***,we present two algorithms for this case:one reduces the model checking problem into a mixed integer non-linear programming(MINLP)problem,which can then be solved by Satisfiability Modulo Theories(SMT)solvers,and the other is an approximate algorithm based on the upper confidence bounds applied to trees(UCT)algorithm,which can return a result whenever *** algorithms have been implemented in an existing model checker and then validated on *** experimental results show the efficiency and extendability of these algorithms,and the algorithm based on UCT outperforms the one based on MINLP in most cases.

关键词： probabilistic multiagent system model checking uniform scheduler probabilistic epistemic temporal logic

来源：评论

学校读者我要写书评

暂无评论

Empirically revisiting and enhancing automatic classification of bug and non-bug issues

引用

Frontiers of computer science 2024年第5期18卷 25-44页

作者： Zhong LI Minxue PAN Yu PEI Tian ZHANG Linzhang WANG Xuandong LI State Key Laboratory for Novel Software Technology Nanjing UniversityNanjing 210023China Department of Computer Science and Technology Nanjing UniversityNanjing 210023China Software Institute Nanjing UniversityNanjing 210093China Department of Computing The Hong Kong Polytechnic UniversityHong KongChina

A large body of research effort has been dedicated to automated issue classification for Issue Tracking Systems(ITSs).Although the existing approaches have shown promising performance,the different design choices,including the different textual fields,feature representation methods and machine learning algorithms adopted by existing approaches,have not been comprehensively compared and *** fill this gap,we perform the first extensive study of automated issue classification on 9 state-of-the-art issue classification *** experimental results on the widely studied dataset reveal multiple practical guidelines for automated issue classification,including:(1)Training separate models for the issue titles and descriptions and then combining these two models tend to achieve better performance for issue classification;(2)Word embedding with Long Short-Term Memory(LSTM)can better extract features from the textual fields in the issues,and hence,lead to better issue classification models;(3)There exist certain terms in the textual fields that are helpful for building more discriminating classifiers between bug and non-bug issues;(4)The performance of the issue classification model is not sensitive to the choices of ML *** on our study outcomes,we further propose an advanced issue classification approach,DEEPlabEL,which can achieve better performance compared with the existing issue classification approaches.

关键词： issue tracking issue type prediction empirical study

来源：评论

学校读者我要写书评

暂无评论

ParLS-PBO: A Parallel Local Search Solver for Pseudo Boolean Optimization 30

ParLS-PBO: A Parallel Local Search Solver for Pseudo Boolean...

引用

30th International Conference on Principles and Practice of Constraint Programming, CP 2024

作者： Chen, Zhihan Lin, Peng Hu, Hao Cai1, Shaowei State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing China School of Computer Science and Technology University of Chinese Academy of Sciences Beijing China

ISBN: (纸本)9783959773362

As a broadly applied technique in numerous optimization problems, recently, local search has been employed to solve Pseudo-Boolean Optimization (PBO) problem. A representative local search solver for PBO is LS-PBO. In this paper, firstly, we improve LS-PBO by a dynamic scoring mechanism, which dynamically strikes a balance between score on hard constraints and score on the objective function. Moreover, on top of this improved LS-PBO, we develop the first parallel local search PBO solver. The main idea is to share good solutions among different threads to guide the search, by maintaining a pool of feasible solutions. For evaluating solutions when updating the pool, we propose a function that considers both the solution quality and the diversity of the pool. Furthermore, we calculate the polarity density in the pool to enhance the scoring function of local search. Our empirical experiments show clear benefits of the proposed parallel approach, making it competitive with the parallel version of the famous commercial solver Gurobi. © Zhihan Chen, Peng Lin, Hao Hu, and Shaowei Cai.

关键词： Local search (optimization)

来源：评论

学校读者我要写书评

暂无评论

A Derivative-Based Membership Algorithm for Enhanced Regular Expressions 10th

A Derivative-Based Membership Algorithm for Enhanced Regula...

引用

10th International Symposium on Dependable software Engineering: Theories, Tools and Applications, SETTA 2024

作者： Wang, Mengxi Dong, Chunmei Su, Weihao Peng, Chengyao Chen, Haiming and State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing China University of Chinese Academy of Sciences Beijing China

ISBN: (纸本)9789819606016

Enhanced regular expressions (EREs), which extend standard regular expressions with shuffle and counting operators, provide exponentially more succinct descriptions of regular languages. The membership problem, determining whether a given word w belongs to the language generated by an ERE E, is fundamental to numerous applications. However, efficient solutions for the membership problem of unconstrained EREs have remained elusive. This paper introduces a derivative for the counting operator and rigorously proves its correctness. We then leverage this derivative to design a membership algorithm for unconstrained EREs and analyze its time complexity based on a lemma establishing the relationship between the size of the derivative and the expression. We further propose algorithms based on the proposed derivatives to generate positive and negative words of specific lengths for EREs. The performance of the membership algorithm is then evaluated on real-world EREs. Finally, we validate the correctness of two existing inference algorithms that previously lacked formal correctness guarantees due to the absence of practical membership algorithms for unconstrained EREs. © The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2025.

关键词： Formal languages

来源：评论

学校读者我要写书评

暂无评论

An Efficient Local Search Solver for Mixed Integer Programming 30

An Efficient Local Search Solver for Mixed Integer Programmi...

引用

30th International Conference on Principles and Practice of Constraint Programming, CP 2024

作者： Lin, Peng Zou, Mengchuan Cai, Shaowei State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing China School of Computer Science and Technology University of Chinese Academy of Sciences Beijing China

ISBN: (纸本)9783959773362

Mixed integer programming (MIP) is a fundamental model in operations research. Local search is a powerful method for solving hard problems, but the development of local search solvers for MIP still needs to be explored. This work develops an efficient local search solver for solving MIP, called Local-MIP. We propose two new operators for MIP to adaptively modify variables for optimizing the objective function and satisfying constraints, respectively. Furthermore, we design a new weighting scheme to dynamically balance the priority between the objective function and each constraint, and propose a two-level scoring function structure to hierarchically guide the search for high-quality feasible solutions. Experiments are conducted on seven public benchmarks to compare Local-MIP with state-of-the-art MIP solvers, which demonstrate that Local-MIP significantly outperforms CPLEX, HiGHS, SCIP and Feasibility Jump, and is competitive with the most powerful commercial solver Gurobi. Moreover, Local-MIP establishes 4 new records for MIPLIB open instances. © Peng Lin, Mengchuan Zou, and Shaowei Cai.

关键词： Mixed-integer linear programming

来源：评论

学校读者我要写书评

暂无评论

Formal Verification of RISC-V Processor Chisel Designs 10th

Formal Verification of RISC-V Processor Chisel Designs

引用

10th International Symposium on Dependable software Engineering: Theories, Tools and Applications, SETTA 2024

作者： Shen, Shidong Liu, Yicheng Zhang, Lijun Song, Fu Wu, Zhilin and State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing China University of Chinese Academy of Sciences Beijing China

ISBN: (纸本)9789819606016

Chisel is an open-source high-level hardware construction language embedded in Scala to facilitate parameterizable, reusable circuit design generators. It is becoming increasingly popular and has been used to design many RISC-V processor variants. Formal verification has been adapted to check the (functional) correctness of RISC-V processor designs. However, the RISC-V instructions therein are specified in the low-level hardware languages Verilog/SystemVerilog, which are challenging to develop, maintain, and extend. This considerably lowers the advantage of RISC-V for designing highly customizable processors. In this work, we present the first end-to-end approach for formally verifying the correctness of RISC-V processor designs, fully at the Chisel high-level. Specifically, by utilizing the object-oriented and functional programming constructs offered by Chisel, we develop a high-level reference model of RISC-V instructions in Chisel. This reference model is a succinct, modular, and parameterized RISC-V processor design generator, thus can produce customized RISC-V processor variants. We then devise a novel queue-based synchronization mechanism between the RISC-V processor Chisel design and the reference model by which the correctness verification of the RISC-V processor design is reduced to the model-checking problem and off-the-shelf model-checkers can be harnessed. We implement our approach in an open-source tool and demonstrate its efficacy on two representative open-source RISC-V processor designs in Chisel (i.e., riscv-mini and NutShell). The experiment results confirm the efficacy of our approach, capable of discovering 7 real-world unknown non-conformance bugs and all the 10 manually injected bugs. It is also three-orders-of-magnitude more efficient than the state-of-the-art symbolic-execution based approach. © The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2025.

关键词： Formal verification

来源：评论

学校读者我要写书评

暂无评论

Superconducting properties of rare-earth boron hydrides at high pressure studied by first-principles calculations

引用

Physical Review B 2024年第6期110卷 L060514页

作者： Simin Li Weiguo Sun Hanyu Liu Cheng Lu Feng Peng College of Physics and Electronic Information Institute of High Pressure Physics School of Physical Science and Technology International Center for Computational Method and Software and State Key Lab of Superhard Materials College of Physics School of Mathematics and Physics

It is a long-thought proposal that dense light-element molecular hydrides, such as diborane (B2H6) and methane (CH4), offer an ideal platform to search for phonon-mediated superconductors. However, these hydrides are often unstable under sufficiently high pressure, e.g., B2H6 decomposed into BH and H2 at pressures of above 153 GPa, which are unlikely to exhibit high superconductivity. Here, we find a feasible route to stabilize these light-element molecular hydrides with high superconductivity under high pressure by high-throughput structure searches and first-principles calculations. We uncover a series of stable H-rich rare-earth (R) metal based boron hydrides RB2H10 with polydiborane networks. Strikingly, YB2H10 is predicted to be a high-temperature superconductor with unprecedentedly critical temperature ( Tc ) of up to 93 K under 150 GPa. The present findings open a route to stabilize the unstable diborane by bringing the additional R metals into the lattice under high pressure, as well as tuning the superconductivity among diborane-based hydrides and other similar dense light-element molecular hydrides.

关键词： Pressure effects Structural properties Superconducting phase transition High-temperature superconductors Density functional theory First-principles calculations

来源：评论

学校读者我要写书评

暂无评论

An Axiom System of Probabilistic Mu-Calculus

引用

Tsinghua science and Technology 2022年第2期27卷 372-385页

作者： Wanwei Liu Junnan Xu David N.Jansen Andrea Turrini Lijun Zhang College of Computer Science National University of Defense TechnologyChangsha 410073China State Key Laboratory of Computer Science Institute of SoftwareChinese Academy of SciencesBeijing 100190China University of Chinese Academy of Sciences Beijing 100039China Institute of Intelligent Software Guangzhou 511458China

Mu-calculus(a.k.a.μTL)is built up from modal/dynamic logic via adding the least fixpoint operatorμ.This type of logic has attracted increasing attention since Kozen’s seminal work.PμTL is a succinct probabilistic extension of the standardμTL obtained by making the modal operators *** of this logic,such as expressiveness and satisfiability decision,have been studied *** consider another important problem:the axiomatization of that *** extending the approaches of Kozen and Walukiewicz,we present an axiom system for Pμ*** addition,we show that the axiom system is complete for aconjunctive formulas.

关键词： PμTL axiom system aconjunctive formula tableau approach

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：