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

algorithm selection for Software Verification Using Graph Neural Networks

ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY 2024年第3期33卷 1-36页

作者： Leeson, Will Dwyer, Matthew B. Univ Virginia 85 Engineers Way Charlottesville VA 22903 USA

The field of software verification has produced a wide array of algorithmic techniques that can prove a variety of properties of a given program. It has been demonstrated that the performance of these techniques can vary up to 4 orders of magnitude on the same verification problem. Even for verification experts, it is difficult to decide which tool will perform best on a given problem. For general users, deciding the best tool for their verification problem is effectively impossible. In this work, we present GRAVES, a selection strategy based on graph neural networks (GNNs). GRAVES generates a graph representation of a program from which a GNN predicts a score for a verifier that indicates its performance on the program. We evaluate GRAVES on a set of 10 verification tools and over 8,000 verification problems and find that it improves the state-of-the-art in verification algorithm selection by 12%, or 8 percentage points. Further, it is able to verify 9% more problems than any existing verifier on our test set. Through a qualitative study on model interpretability, we find strong evidence that the GRAVES model learns to base its predictions on factors that relate to the unique features of the algorithmic techniques.

关键词： algorithm selection graph neural networks

来源：评论

学校读者我要写书评

暂无评论

algorithm selection for SMT MachSMT: Machine Learning Driven algorithm selection for SMT Solvers

引用

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER 2023年第2期25卷 219-239页

作者： Scott, Joseph Niemetz, Aina Preiner, Mathias Nejati, Saeed Ganesh, Vijay 200 Univ Ave Waterloo ON Canada 450 Jane Stanford Way Stanford CA 94305 USA

This paper presents MachSMT, an algorithm selection tool for Satisfiability Modulo Theories (SMT) solvers. MachSMT supports the entirety of the SMT-LIB language and standardized SMT-LIB theories, and is easy to extend with support for new theories. MachSMT deploys machine learning methods to construct both empirical hardness models and pairwise ranking comparators over state-of-the-art SMT solvers. Given an input formula in SMT-LIB format, MachSMT leverages these learnt models to output a ranking of solvers based on predicted runtimes. We provide an extensive empirical evaluation of MachSMT to demonstrate the efficiency and efficacy of MachSMT over three broad usage scenarios on theories and theory combinations of practical relevance (e.g., bit-vectors, (non)linear integer and real arithmetic, arrays, and floating-point arithmetic). First, we deploy MachSMT on state-of-the-art solvers in SMT-COMP 2019 and 2020. We observe MachSMT frequently improves on the best performing solvers in the competition, winning 57 divisions outright, with up to a 99.4% improvement in PAR-2 score. Second, we evaluate MachSMT to select configurations from a single underlying solver. We observe that MachSMT solves 898 more benchmarks and up to a 93.4% improvement in PAR-2 score across 23 configurations of the SMT solver cvc5. Last, we evaluate MachSMT on domain-specific problems, namely network verification with simple domain-specific features, and observe an improvement of 77.3% in PAR-2 score.

关键词： SMT solvers Machine learning algorithm selection

来源：评论

学校读者我要写书评

暂无评论

algorithm selection on a meta level

引用

MACHINE LEARNING 2023年第4期112卷 1253-1286页

作者： Tornede, Alexander Gehring, Lukas Tornede, Tanja Wever, Marcel Huellermeier, Eyke Paderborn Univ Heinz Nixdorf Inst D-33098 Paderborn Germany Univ Munich LMU D-80538 Munich Germany

The problem of selecting an algorithm that appears most suitable for a specific instance of an algorithmic problem class, such as the Boolean satisfiability problem, is called instance-specific algorithm selection. Over the past decade, the problem has received considerable attention, resulting in a number of different methods for algorithm selection. Although most of these methods are based on machine learning, surprisingly little work has been done on meta learning, that is, on taking advantage of the complementarity of existing algorithm selection methods in order to combine them into a single superior algorithm selector. In this paper, we introduce the problem of meta algorithm selection, which essentially asks for the best way to combine a given set of algorithm selectors. We present a general methodological framework for meta algorithm selection as well as several concrete learning methods as instantiations of this framework, essentially combining ideas of meta learning and ensemble learning. In an extensive experimental evaluation, we demonstrate that ensembles of algorithm selectors can significantly outperform single algorithm selectors and have the potential to form the new state of the art in algorithm selection.

关键词： algorithm selection Meta learning Ensemble learning Bagging Boosting Stacking

来源：评论

学校读者我要写书评

暂无评论

algorithm selection of MPI Collectives Considering System Utilization

Algorithm Selection of MPI Collectives Considering System Ut...

引用

29th International Conference on Parallel and Distributed Computing (Euro-Par)

作者： Beni, Majid Salimi Hunold, Sascha Cosenza, Biagio Univ Salerno Dept Comp Sci Salerno Italy TU Wien Fac Informat Vienna Austria

ISBN: (纸本)9783031488023;9783031488030

MPI collective communications play an important role in coordinating and exchanging data among parallel processes in high performance computing. Various algorithms exist for implementing MPI collectives, each of which exhibits different characteristics, such as message overhead, latency, and scalability, which can significantly impact overall system performance. Therefore, choosing a suitable algorithm for each collective operation is crucial to achieve optimal performance. In this paper, we present our experience with MPI collectives algorithm selection on a large-scale supercomputer and highlight the impact of network traffic and system workload as well as other previously-investigated parameters such as message size, communicator size, and network topology. Our analysis shows that network traffic and system workload can make the performance of MPI collectives highly variable and, accordingly, impact the algorithm selection strategy.

关键词： High Performance Computing MPI Collectives Broadcast algorithm selection Tuning

来源：评论

学校读者我要写书评

暂无评论

algorithm selection and Data Utilization in Machine Learning for Medical Imaging Classification

Algorithm Selection and Data Utilization in Machine Learning...

引用

18th IEEE Long Island Systems, Applications and Technology Conference

作者： Toma, Milan Husain, Gazi NYIT Dept Osteopath Manipulat Med Coll Osteopath Med Old Westbury NY 11568 USA NYIT Dept Anat Coll Osteopath Med Old Westbury NY USA

ISBN: (纸本)9798331506674;9798331506667

The process of selecting an appropriate Machine Learning (ML) algorithm for medical image classification is inherently complex. This complexity arises from the diverse nature of medical conditions and the varying characteristics of imaging data. For instance, the imaging data for a brain tumor would differ significantly from that of a lung nodule, necessitating different ML approaches. Moreover, different ML algorithms may be more suitable for different types of data and medical conditions. For example, Convolutional Neural Networks (CNNs) have shown exceptional performance in image data, making them a popular choice for medical imaging tasks. On the other hand, algorithms like Support Vector Machines (SVMs) or Decision Trees (DTs) might be more suitable for structured, tabular data. The potential transformative impact of ML in healthcare is vast and multi-faceted. It ranges from predicting disease progression, which can help in early intervention and better patient management, to personalizing treatment plans, which can lead to improved patient outcomes. Furthermore, ML can automate routine tasks, such as image analysis or patient triage, thereby reducing the workload of healthcare professionals and allowing them to focus on more complex tasks. The influence of ML on medical imaging is significant. It offers innovative solutions for image analysis and interpretation, which can enhance diagnostic accuracy and efficiency. For instance, ML algorithms can be used for image classification, where images are categorized into different classes representing various medical conditions. They can also be used for image segmentation, where specific regions of interest within an image are identified and separated. Additionally, ML can enhance images, improving their quality and making it easier for healthcare professionals to identify abnormalities. However, a model trained on data from one hospital, or one population group, might not perform well when applied to data from a dif

关键词： machine learning medical imaging algorithm selection real-world data image classification

来源：评论

学校读者我要写书评

暂无评论

Machine Learning based algorithm selection and Genetic algorithms for serial-batch scheduling

引用

COMPUTERS & OPERATIONS RESEARCH 2025年 173卷

作者： Uzunoglu, Aykut Gahm, Christian Tuma, Axel Augsburg Univ Chair Business Adm Prod & Supply Chain Management D-86135 Augsburg Germany

Whenever combinatorial optimization problems cannot be solved by exact solution methods in reasonable time, tailor-made algorithms (heuristics, meta-heuristics) are developed. Often, these heuristics exploit structural properties and perform well on selected subsets of the problem space. For example, this is how the two bestknown construction heuristics solve the scheduling problem investigated in this study (i.e., the scheduling of parallel serial-batch processing machines with incompatible job families, restricted batch capacities, arbitrary batch capacity demands, and sequence-dependent setup times). However, when the properties change, the performance of one algorithm might decrease, and another algorithm might have been the better choice. To resolve this issue, we propose using Machine Learning to exploit the strengths of different algorithms and to select the probably best-performing algorithm for each problem instance individually. To that, we investigate a variety of methods from the "learning-to-rank" literature and propose several adaptations. Furthermore, because there is no algorithm for the considered scheduling problem that is capable to explore the entire solution space, we developed two Genetic algorithms for the improvement of initial solutions computed by the selected algorithms. Here, we put special emphasis on ensuring that the solution representation (encoding) reflects the entire solution space and that the operators (e.g., for recombination and mutation) are appropriate to explore and exploit this space completely. Our computational experiments show an average increase of 39.19% in solution quality.

关键词： Serial batching Total weighted tardiness algorithm selection Genetic algorithm Machine learning

来源：评论

学校读者我要写书评

暂无评论

Automatic algorithm selection for Pseudo-Boolean optimization with given computational time limits

引用

COMPUTERS & OPERATIONS RESEARCH 2025年 173卷

作者： Pezo, Catalina Hochbaum, Dorit Godoy, Julio Asin-Acha, Roberto Univ Calif Berkeley Dept Ind Engn & Operat Res Berkeley CA USA Univ Concepcion Dept Comp Sci Concepcion Chile Univ Tecn Federico Santa Maria Dept Informat Valparaiso Chile

Machine learning (ML) techniques have been proposed to automatically select the best solver from a portfolio of solvers. They have been applied to various problems including Boolean Satisfiability, Traveling Salesperson and Graph Coloring. These techniques are used to implement meta-solvers that receive, as input, the instance of a problem, predict the best-performing solver in the portfolio, and execute it to deliver a solution. Typically, the quality of the solution improves with a longer computational time. This has led to the development of anytime meta-solvers, , which consider both the instance and a user-prescribed computational time limit. Anytime meta-solvers predict the best-performing solver within the specified time limit. In this study, we focus on designing anytime meta-solvers for the NP-hard optimization problem of Pseudo-Boolean Optimization (PBO), which generalizes Satisfiability and Maximum Satisfiability problems. The effectiveness of our approach is demonstrated via extensive empirical study in which our anytime meta-solver, named PBO_MS, improves dramatically on the performance of Mixed Integer Programming solver Gurobi, which is the best-performing single solver in the portfolio. We generalize the anytime meta-solver by predicting a given number p >= 1 of best solvers in the portfolio and then run these, each with equal share of the specified time limit. This anytime p-meta-solver is shown here to outperform both the anytime 1-meta-solver as well as a fixed selection of p solvers by a wide margin.

关键词： algorithm selection PBO Combinatorial optimization ML

来源：评论

学校读者我要写书评

暂无评论

algorithm selection Framework for Legalization Using Deep Convolutional Neural Networks and Transfer Learning

引用

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS 2022年第5期41卷 1481-1494页

作者： Netto, Renan Fabre, Sheiny Fontana, Tiago Augusto Livramento, Vinicius Pilla, Laercio L. Behjat, Laleh Guntzel, Jose Luis Univ Fed Santa Catarina Dept Comp Sci & Stat BR-88040900 Florianopolis SC Brazil Univ Fed Santa Catarina Dept Automat & Syst Engn BR-88040900 Florianopolis SC Brazil Lab Rech Informat F-91190 Gif Sur Yvette France Lab Bordelais Rech Informat F-33405 Talence France Univ Calgary Dept Elect & Comp Engn Calgary AB T2N 1N4 Canada

Machine learning (ML) models have been used to improve the quality of different physical design steps, such as timing analysis, clock tree synthesis, and routing. However, so far very few works have addressed the problem of algorithm selection during physical design, which can drastically reduce the computational effort of some steps. This work proposes a legalization algorithm selection framework using deep convolutional neural networks (CNNs). To extract features, we used snapshots of circuit placements and used transfer learning to train the models using pretrained weights of the Squeezenet architecture. By doing so, we can greatly reduce the training time and required data even though the pretrained weights come from a different problem. We performed extensive experimental analysis of ML models, providing details on how we chose the parameters of our model, such as CNN architecture, learning rate, and number of epochs. We evaluated the proposed framework by training a model to select between different legalization algorithms according to cell displacement and wirelength variation. The trained models achieved an average F-score of 0.98 when predicting cell displacement and 0.83 when predicting wirelength variation. When integrated into the physical design flow, the cell displacement model achieved the best results on 15 out of 16 designs, while the wirelength variation model achieved that for 10 out of 16 designs, being better than any individual legalization algorithm. Finally, using the proposed ML model for algorithm selection resulted in a speedup of up to 10x compared to running all the algorithms separately.

关键词： algorithm selection convolutional neural network (CNN) machine learning (ML) multirow legalization physical design

来源：评论

学校读者我要写书评

暂无评论

A dynamic AI-based algorithm selection for Virtual Network Embedding

引用

ANNALS OF TELECOMMUNICATIONS 2025年第3-4期80卷 265-281页

作者： Bouroudi, Abdelmounaim Outtagarts, Abdelkader Hadjadj-Aoul, Yassine Nokia Networks Bell Labs Nozay France Univ Rennes INRIA CNRS IRISA Rennes France

With the increasing sophistication and heterogeneity of network infrastructures, the need for Virtual Network Embedding (VNE) is becoming more critical than ever. VNE consists of mapping virtual networks on top of the physical infrastructure to optimize network resource use and improve overall network performance. Considered as one of the most important bricks of network slicing, it has been proven to be an NP-hard problem with no exact solution. Several heuristics and meta-heuristics were proposed to solve it. As heuristics do not provide satisfactory solutions, meta-heuristics allow a good exploration of the solutions' space, though they require testing several solutions, which is generally unfeasible in a real world environment. Other methods relying on deep reinforcement learning (DRL) and combined with heuristics yield better performance without revealing issues such as sticking at local minima or poor space exploration limits. Nevertheless, these algorithms present varied performances according to the employed approach and the problem to be treated, resulting in robustness problems. To overcome these limits, we propose a robust placement approach based on the algorithm selection paradigm. The main idea is to dynamically select the best algorithm from a set of learning strategies regarding reward and sample efficiency at each time step. The proposed strategy acts as a meta-algorithm that brings more robustness to the network since it dynamically selects the best solution for a specific scenario. We propose two selection algorithms. First, we consider an offline selection in which the placement strategies are updated outside the selection period. In the second algorithm, the different agents are updated simultaneously with the selection process, which we call an online selection. Both solutions proved their efficiency and managed to dynamically select the best algorithm regarding acceptance ratio of the deployed services. Besides, the proposed solutions succeed

关键词： Virtual Network Embedding AI Deep reinforcement learning algorithm selection B5G/6 G

来源：评论

学校读者我要写书评

暂无评论

Anytime Automatic algorithm selection for the Multi-Agent Path Finding Problem

引用

IEEE ACCESS 2024年 12卷 62177-62188页

作者： Zapata, Angelo Godoy, Julio Asin-Acha, Roberto Univ Concepcion Dept Comp Sci Concepcion 4070409 Chile Univ Tecn Federico Santa Maria Dept Informat Valparaiso 234000 Chile

In this study, we propose and develop a Machine Learning-based metasolver for the Multi-Agent Path Finding (MAPF) problem, with the aim of selecting the most suitable solver based on the specific characteristics of the problem and a user-provided time constraint. The approach aims to improve the performance of the best-performing solver on average and approximate the performance of a perfect selector. To achieve this, a comprehensive and diverse dataset was compiled, and state-of-the-art algorithms were selected and modified to efficiently handle the time constraint. Also, relevant features were identified, and a precise and robust Machine Learning model was constructed using the XGBoost algorithm. The model was evaluated and compared against other state-of-the-art methods. The results demonstrate that the proposed approach is effective and consistent, outperforming the Single Best Solver and approximating the performance of the Virtual Best Solver.

关键词： algorithm design and analysis Multi-agent systems Path planning Time factors Approximation algorithms Performance evaluation algorithm selection multi-agent path finding machine learning

来源：评论

学校读者我要写书评

暂无评论

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

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：