Machine learning models need to be continually updated or corrected to ensure that the prediction accuracy remains consistently high. In this study, we consider scenarios where developers should be careful to change the prediction results by the model correction, such as when the model is part of a complex system or software. In such scenarios, the developers want to control the specification of the corrections. To achieve this, the developers need to understand which subpopulations of the inputs get inaccurate predictions by the model. Therefore, we propose correction rule mining to acquire a comprehensive list of rules that describe inaccurate subpopulations and how to correct them. We also develop an efficient correction rule mining algorithm that is a combination of frequent itemset mining and a unique pruning technique for correction rules. We observed that the proposed algorithm found various rules which help to collect data insufficiently learned, directly correct model outputs, and analyze concept drift.

In practical machine learning, models are frequently updated, or corrected, to adapt to new datasets. In this study, we pose two challenges to model correction. First, the effects of corrections to the end-users need to be described explicitly, similar to standard software where the corrections are described as release notes. Second, the amount of corrections need to be small so that the corrected models perform similarly to the old models. In this study, we propose the first model correction method for classification models that resolves these two challenges. Our idea is to use an additional decision tree to correct the output of the old models. Thanks to the explainability of decision trees, the corrections are describable to the end-users, which resolves the first challenge. We resolve the second challenge by incorporating the amount of corrections when training the additional decision tree so that the effects of corrections to be small. Experiments on real data confirm the effectiveness of the proposed method compared to existing correction methods.

Several graph libraries have been developed in the past few decades, and they were basically designed to work with a few graphs. However, there are many problems in which we have to consider all subgraphs satisfying certain constraints on a given graph. Since the number of subgraphs can increase exponentially with the graph size, explicitly representing these sets is infeasible. Hence, libraries concerned with efficiently representing a single graph instance are not suitable for such problems. In this paper, we develop Graphillion, a software library for very large sets of (vertex-)labeled graphs, based on zero-suppressed binary decision diagrams. Graphillion is not based on a traditional representation of graphs. Instead, a graph set is simply regarded as a “set of edge sets” ignoring vertices, which allows us to employ powerful tools of a “family of sets” (a set of sets) and permits large graph sets to be handled efficiently. We also utilize advanced graph enumeration algorithms, which enable the simple family tools to understand the graph structure. Graphillion is implemented as a Python library to encourage easy development of its applications, without introducing significant performance overheads. In experiments, we consider two case studies, a puzzle solver and a power network optimizer, in which several operations and heavy optimization have to be performed over very large sets of constrained graphs (i.e., cycles or forests with complicated conditions). The results show that Graphillion allows us to manage a huge number of graphs with very low development effort.

Article Formal verification based on assume and guarantee approach — a case study (short paper) Share on Authors: Subir K. Roy Fujitsu Laboratories Ltd., 1-1 kamikodanaka 4-chome, Nakahara-ku, Kawasaki 211-8588, Japan Fujitsu Laboratories Ltd., 1-1 kamikodanaka 4-chome, Nakahara-ku, Kawasaki 211-8588, JapanView Profile , Hiroaki Iwashita Fujitsu Laboratories Ltd., 1-1 kamikodanaka 4-chome, Nakahara-ku, Kawasaki 211-8588, Japan Fujitsu Laboratories Ltd., 1-1 kamikodanaka 4-chome, Nakahara-ku, Kawasaki 211-8588, JapanView Profile , Tsuneo Nakata Fujitsu Laboratories Ltd., 1-1 kamikodanaka 4-chome, Nakahara-ku, Kawasaki 211-8588, Japan Fujitsu Laboratories Ltd., 1-1 kamikodanaka 4-chome, Nakahara-ku, Kawasaki 211-8588, JapanView Profile Authors Info & Claims ASP-DAC '00: Proceedings of the 2000 Asia and South Pacific Design Automation ConferenceJanuary 2000 Pages 77–80https://doi.org/10.1145/368434.368530Online:28 January 2000Publication History 1citation146DownloadsMetricsTotal Citations1Total Downloads146Last 12 Months1Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

Forward model checking is an efficient symbolic model checking method for verifying realistic properties of sequential circuits and protocols. We present the techniques that modify the order of state traversal on forward model checking, and that dramatically improve average CPU time for finding design errors. A failing property has to be checked again and again to analyze the bug until it is corrected. The techniques, therefore, can have significant impacts on actual verification tasks. We use a modified regular//spl omega/-regular expression to represent a set of illegal state transition sequences of an FSM. It makes the problem clear and gives us a sense of depth-first traversal, not on the state space, but on the property.

We present a CTL model checking algorithm based mainly on forward state traversal, which can check many realistic CTL properties without doing backward state traversal. This algorithm is effective in many situations where backward state traversal is more expensive than forward state traversal. We combine it with BDD-based state traversal techniques using partitioned transition relations. Experimental results show that our method can verify actual CTL properties of large industrial models which cannot be handled by conventional model checkers.