Showing 1–11 of 11 results for author: Tomita, T

SMT-Based Model Checking of Industrial Simulink Models

Authors: Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Thi Bich Ngoc Do, Hideaki Takai

Abstract: The development of embedded systems requires formal analysis of models such as those described with MATLAB/Simulink. However, the increasing complexity of industrial models makes analysis difficult. This paper proposes a model checking method for Simulink models using SMT solvers. The proposed method aims at (1) automated, efficient and comprehensible verification of complex models, (2) numericall… ▽ More The development of embedded systems requires formal analysis of models such as those described with MATLAB/Simulink. However, the increasing complexity of industrial models makes analysis difficult. This paper proposes a model checking method for Simulink models using SMT solvers. The proposed method aims at (1) automated, efficient and comprehensible verification of complex models, (2) numerically accurate analysis of models, and (3) demonstrating the analysis of Simulink models using an SMT solver (we use Z3). It first encodes a target model into a predicate logic formula in the domain of mathematical arithmetic and bit vectors. We explore how to encode various Simulink blocks exactly. Then, the method verifies a given invariance property using the k-induction-based algorithm that extracts a subsystem involving the target block and unrolls the execution paths incrementally. In the experiment, we applied the proposed method and other tools to a set of models and properties. Our method successfully verified most of the properties including those unverified with other tools. △ Less

Submitted 6 June, 2022; originally announced June 2022.

Comments: 16 pages, 5 figures, 1 table, submitted to ICFEM 2022

Deep Discriminative to Kernel Density Graph for In- and Out-of-distribution Calibrated Inference

Authors: Jayanta Dey, Haoyin Xu, Will LeVine, Ashwin De Silva, Tyler M. Tomita, Ali Geisa, Tiffany Chu, Jacob Desman, Joshua T. Vogelstein

Abstract: Deep discriminative approaches like random forests and deep neural networks have recently found applications in many important real-world scenarios. However, deploying these learning algorithms in safety-critical applications raises concerns, particularly when it comes to ensuring confidence calibration for both in-distribution and out-of-distribution data points. Many popular methods for in-distr… ▽ More Deep discriminative approaches like random forests and deep neural networks have recently found applications in many important real-world scenarios. However, deploying these learning algorithms in safety-critical applications raises concerns, particularly when it comes to ensuring confidence calibration for both in-distribution and out-of-distribution data points. Many popular methods for in-distribution (ID) calibration, such as isotonic and Platt's sigmoidal regression, exhibit excellent ID calibration performance. However, these methods are not calibrated for the entire feature space, leading to overconfidence in the case of out-of-distribution (OOD) samples. On the other end of the spectrum, existing out-of-distribution (OOD) calibration methods generally exhibit poor in-distribution (ID) calibration. In this paper, we address ID and OOD calibration problems jointly. We leveraged the fact that deep models, including both random forests and deep-nets, learn internal representations which are unions of polytopes with affine activation functions to conceptualize them both as partitioning rules of the feature space. We replace the affine function in each polytope populated by the training data with a Gaussian kernel. Our experiments on both tabular and vision benchmarks show that the proposed approaches obtain well-calibrated posteriors while mostly preserving or improving the classification accuracy of the original algorithm for ID region, and extrapolate beyond the training data to handle OOD inputs appropriately. △ Less

Submitted 7 June, 2024; v1 submitted 31 January, 2022; originally announced January 2022.

Compositional Test Generation of Industrial Synchronous Systems

Authors: Daisuke Ishii, Takashi Tomita, Kenji Onishi, Toshiaki Aoki

Abstract: Synchronous systems provide a basic model of embedded systems and industrial systems are modeled as Simulink diagrams and/or Lustre programs. Although the test generation problem is critical in the development of safe systems, it often fails because of the spatial and temporal complexity of the system descriptions. This paper presents a compositional test generation method to address the complexit… ▽ More Synchronous systems provide a basic model of embedded systems and industrial systems are modeled as Simulink diagrams and/or Lustre programs. Although the test generation problem is critical in the development of safe systems, it often fails because of the spatial and temporal complexity of the system descriptions. This paper presents a compositional test generation method to address the complexity issue. We regard a test case as a counterexample in safety verification, and represent a test generation process as a deductive proof tree built with dedicated inference rules; we conduct both spatial- and temporal-compositional reasoning along with a modular system structure. A proof tree is generated using our semi-automated scheme involving manual effort on contract generation and automatic processes for counterexample search with SMT solvers. As case studies, the proposed method is applied to four industrial examples involving such features as enabled/triggered subsystems, multiple execution rates, filter components, and nested counters. In the experiments, we successfully generated test cases for target systems that were difficult to deal with using the existing tools. △ Less

Submitted 10 December, 2021; originally announced December 2021.

Comments: 22 pages, 5 figures, 2 tables. Rejected from VMCAI 2021

Approximate Translation from Floating-Point to Real-Interval Arithmetic

Authors: Daisuke Ishii, Takashi Tomita, Toshiaki Aoki

Abstract: Floating-point arithmetic (FPA) is a mechanical representation of real arithmetic (RA), where each operation is replaced with a rounded counterpart. Various numerical properties can be verified by using SMT solvers that support the logic of FPA. However, the scalability of the solving process remains limited when compared to RA. In this paper, we present a decision procedure for FPA that takes adv… ▽ More Floating-point arithmetic (FPA) is a mechanical representation of real arithmetic (RA), where each operation is replaced with a rounded counterpart. Various numerical properties can be verified by using SMT solvers that support the logic of FPA. However, the scalability of the solving process remains limited when compared to RA. In this paper, we present a decision procedure for FPA that takes advantage of the efficiency of RA solving. The proposed method abstracts FP numbers as rational intervals and FPA expressions as interval arithmetic (IA) expressions; then, we solve IA formulas to check the satisfiability of an FPA formula using an off-the-shelf RA solver (we use CVC4 and Z3). In exchange for the efficiency gained by abstraction, the solving process becomes quasi-complete; we allow to output unknown when the satisfiability is affected by possible numerical errors. Furthermore, our IA is meticulously formalized to handle the special value NaN. We implemented the proposed method and compared it to four existing SMT solvers in the experiments. As a result, we confirmed that our solver was efficient for instances where rounding modes were parameterized. △ Less

Submitted 6 December, 2021; originally announced December 2021.

Comments: 21 pages, 9 figures, 4 tables

Towards a theory of out-of-distribution learning

Authors: Jayanta Dey, Ali Geisa, Ronak Mehta, Tyler M. Tomita, Hayden S. Helm, Haoyin Xu, Eric Eaton, Jeffery Dick, Carey E. Priebe, Joshua T. Vogelstein

Abstract: Learning is a process wherein a learning agent enhances its performance through exposure of experience or data. Throughout this journey, the agent may encounter diverse learning environments. For example, data may be presented to the leaner all at once, in multiple batches, or sequentially. Furthermore, the distribution of each data sample could be either identical and independent (iid) or non-iid… ▽ More Learning is a process wherein a learning agent enhances its performance through exposure of experience or data. Throughout this journey, the agent may encounter diverse learning environments. For example, data may be presented to the leaner all at once, in multiple batches, or sequentially. Furthermore, the distribution of each data sample could be either identical and independent (iid) or non-iid. Additionally, there may exist computational and space constraints for the deployment of the learning algorithms. The complexity of a learning task can vary significantly, depending on the learning setup and the constraints imposed upon it. However, it is worth noting that the current literature lacks formal definitions for many of the in-distribution and out-of-distribution learning paradigms. Establishing proper and universally agreed-upon definitions for these learning setups is essential for thoroughly exploring the evolution of ideas across different learning scenarios and deriving generalized mathematical bounds for these learners. In this paper, we aim to address this issue by proposing a chronological approach to defining different learning tasks using the provably approximately correct (PAC) learning framework. We will start with in-distribution learning and progress to recently proposed lifelong or continual learning. We employ consistent terminology and notation to demonstrate how each of these learning frameworks represents a specific instance of a broader, more generalized concept of learnability. Our hope is that this work will inspire a universally agreed-upon approach to quantifying different types of learning, fostering greater understanding and progress in the field. △ Less

Submitted 7 June, 2024; v1 submitted 29 September, 2021; originally announced September 2021.

Robust Similarity and Distance Learning via Decision Forests

Authors: Tyler M. Tomita, Joshua T. Vogelstein

Abstract: Canonical distances such as Euclidean distance often fail to capture the appropriate relationships between items, subsequently leading to subpar inference and prediction. Many algorithms have been proposed for automated learning of suitable distances, most of which employ linear methods to learn a global metric over the feature space. While such methods offer nice theoretical properties, interpret… ▽ More Canonical distances such as Euclidean distance often fail to capture the appropriate relationships between items, subsequently leading to subpar inference and prediction. Many algorithms have been proposed for automated learning of suitable distances, most of which employ linear methods to learn a global metric over the feature space. While such methods offer nice theoretical properties, interpretability, and computationally efficient means for implementing them, they are limited in expressive capacity. Methods which have been designed to improve expressiveness sacrifice one or more of the nice properties of the linear methods. To bridge this gap, we propose a highly expressive novel decision forest algorithm for the task of distance learning, which we call Similarity and Metric Random Forests (SMERF). We show that the tree construction procedure in SMERF is a proper generalization of standard classification and regression trees. Thus, the mathematical driving forces of SMERF are examined via its direct connection to regression forests, for which theory has been developed. Its ability to approximate arbitrary distances and identify important features is empirically demonstrated on simulated data sets. Last, we demonstrate that it accurately predicts links in networks. △ Less

Submitted 21 August, 2020; v1 submitted 27 July, 2020; originally announced July 2020.

Comments: Submitted to NeurIPS 2020

A Simple Lifelong Learning Approach

Authors: Joshua T. Vogelstein, Jayanta Dey, Hayden S. Helm, Will LeVine, Ronak D. Mehta, Tyler M. Tomita, Haoyin Xu, Ali Geisa, Qingyang Wang, Gido M. van de Ven, Chenyu Gao, Weiwei Yang, Bryan Tower, Jonathan Larson, Christopher M. White, Carey E. Priebe

Abstract: In lifelong learning, data are used to improve performance not only on the present task, but also on past and future (unencountered) tasks. While typical transfer learning algorithms can improve performance on future tasks, their performance on prior tasks degrades upon learning new tasks (called forgetting). Many recent approaches for continual or lifelong learning have attempted to maintain perf… ▽ More In lifelong learning, data are used to improve performance not only on the present task, but also on past and future (unencountered) tasks. While typical transfer learning algorithms can improve performance on future tasks, their performance on prior tasks degrades upon learning new tasks (called forgetting). Many recent approaches for continual or lifelong learning have attempted to maintain performance on old tasks given new tasks. But striving to avoid forgetting sets the goal unnecessarily low. The goal of lifelong learning should be to use data to improve performance on both future tasks (forward transfer) and past tasks (backward transfer). In this paper, we show that a simple approach -- representation ensembling -- demonstrates both forward and backward transfer in a variety of simulated and benchmark data scenarios, including tabular, vision (CIFAR-100, 5-dataset, Split Mini-Imagenet, and Food1k), and speech (spoken digit), in contrast to various reference algorithms, which typically failed to transfer either forward or backward, or both. Moreover, our proposed approach can flexibly operate with or without a computational budget. △ Less

Submitted 11 June, 2024; v1 submitted 27 April, 2020; originally announced April 2020.

Manifold Oblique Random Forests: Towards Closing the Gap on Convolutional Deep Networks

Authors: Adam Li, Ronan Perry, Chester Huynh, Tyler M. Tomita, Ronak Mehta, Jesus Arroyo, Jesse Patsolic, Benjamin Falk, Joshua T. Vogelstein

Abstract: Decision forests (Forests), in particular random forests and gradient boosting trees, have demonstrated state-of-the-art accuracy compared to other methods in many supervised learning scenarios. In particular, Forests dominate other methods in tabular data, that is, when the feature space is unstructured, so that the signal is invariant to a permutation of the feature indices. However, in structur… ▽ More Decision forests (Forests), in particular random forests and gradient boosting trees, have demonstrated state-of-the-art accuracy compared to other methods in many supervised learning scenarios. In particular, Forests dominate other methods in tabular data, that is, when the feature space is unstructured, so that the signal is invariant to a permutation of the feature indices. However, in structured data lying on a manifold (such as images, text, and speech) deep networks (Networks), specifically convolutional deep networks (ConvNets), tend to outperform Forests. We conjecture that at least part of the reason for this is that the input to Networks is not simply the feature magnitudes, but also their indices. In contrast, naive Forest implementations fail to explicitly consider feature indices. A recently proposed Forest approach demonstrates that Forests, for each node, implicitly sample a random matrix from some specific distribution. These Forests, like some classes of Networks, learn by partitioning the feature space into convex polytopes corresponding to linear functions. We build on that approach and show that one can choose distributions in a manifold-aware fashion to incorporate feature locality. We demonstrate the empirical performance on data whose features live on three different manifolds: a torus, images, and time-series. Moreover, we demonstrate its strength in multivariate simulated settings and also show superiority in predicting surgical outcome in epilepsy patients and predicting movement direction from raw stereotactic EEG data from non-motor brain regions. In all simulations and real data, Manifold Oblique Random Forest (MORF) algorithm outperforms approaches that ignore feature space structure and challenges the performance of ConvNets. Moreover, MORF runs fast and maintains interpretability and theoretical justification. △ Less

Submitted 5 September, 2022; v1 submitted 25 September, 2019; originally announced September 2019.

Comments: Updated manuscript based on review at SIMODS

MSC Class: 68T05

Forest Packing: Fast, Parallel Decision Forests

Authors: James Browne, Tyler M. Tomita, Disa Mhembere, Randal Burns, Joshua T. Vogelstein

Abstract: Machine learning has an emerging critical role in high-performance computing to modulate simulations, extract knowledge from massive data, and replace numerical models with efficient approximations. Decision forests are a critical tool because they provide insight into model operation that is critical to interpreting learned results. While decision forests are trivially parallelizable, the travers… ▽ More Machine learning has an emerging critical role in high-performance computing to modulate simulations, extract knowledge from massive data, and replace numerical models with efficient approximations. Decision forests are a critical tool because they provide insight into model operation that is critical to interpreting learned results. While decision forests are trivially parallelizable, the traversals of tree data structures incur many random memory accesses and are very slow. We present memory packing techniques that reorganize learned forests to minimize cache misses during classification. The resulting layout is hierarchical. At low levels, we pack the nodes of multiple trees into contiguous memory blocks so that each memory access fetches data for multiple trees. At higher levels, we use leaf cardinality to identify the most popular paths through a tree and collocate those paths in cache lines. We extend this layout with out-of-order execution and cache-line prefetching to increase memory throughput. Together, these optimizations increase the performance of classification in ensembles by a factor of four over an optimized C++ implementation and a actor of 50 over a popular R language implementation. △ Less

Submitted 19 June, 2018; originally announced June 2018.

Sparse Projection Oblique Randomer Forests

Authors: Tyler M. Tomita, James Browne, Cencheng Shen, Jaewon Chung, Jesse L. Patsolic, Benjamin Falk, Jason Yim, Carey E. Priebe, Randal Burns, Mauro Maggioni, Joshua T. Vogelstein

Abstract: Decision forests, including Random Forests and Gradient Boosting Trees, have recently demonstrated state-of-the-art performance in a variety of machine learning settings. Decision forests are typically ensembles of axis-aligned decision trees; that is, trees that split only along feature dimensions. In contrast, many recent extensions to decision forests are based on axis-oblique splits. Unfortuna… ▽ More Decision forests, including Random Forests and Gradient Boosting Trees, have recently demonstrated state-of-the-art performance in a variety of machine learning settings. Decision forests are typically ensembles of axis-aligned decision trees; that is, trees that split only along feature dimensions. In contrast, many recent extensions to decision forests are based on axis-oblique splits. Unfortunately, these extensions forfeit one or more of the favorable properties of decision forests based on axis-aligned splits, such as robustness to many noise dimensions, interpretability, or computational efficiency. We introduce yet another decision forest, called "Sparse Projection Oblique Randomer Forests" (SPORF). SPORF uses very sparse random projections, i.e., linear combinations of a small subset of features. SPORF significantly improves accuracy over existing state-of-the-art algorithms on a standard benchmark suite for classification with >100 problems of varying dimension, sample size, and number of classes. To illustrate how SPORF addresses the limitations of both axis-aligned and existing oblique decision forest methods, we conduct extensive simulated experiments. SPORF typically yields improved performance over existing decision forests, while mitigating computational efficiency and scalability and maintaining interpretability. SPORF can easily be incorporated into other ensemble methods such as boosting to obtain potentially similar gains. △ Less

Submitted 3 October, 2019; v1 submitted 10 June, 2015; originally announced June 2015.

Comments: 31 pages; submitted to Journal of Machine Learning Research for review

MSC Class: 68T10 ACM Class: I.5.2

Journal ref: Journal of Machine Learning Research 21(104), 1-39, 2020

A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking

Authors: Takashi Tomita, Shigeki Hagihara, Naoki Yonezaki

Abstract: Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL) are often used to describe specifications of probabilistic properties for discrete time and continuous time, respectively. In PCTL and CSL, the possibility of executions satisfying some temporal properties can be quantitatively represented by the probabilistic extension of the path quantifiers in their basic Computat… ▽ More Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL) are often used to describe specifications of probabilistic properties for discrete time and continuous time, respectively. In PCTL and CSL, the possibility of executions satisfying some temporal properties can be quantitatively represented by the probabilistic extension of the path quantifiers in their basic Computation Tree Logic (CTL), however, path formulae of them are expressed via the same operators in CTL. For this reason, both of them cannot represent formulae with quantitative temporal properties, such as those of the form "some properties hold to more than 80% of time points (in a certain bounded interval) on the path." In this paper, we introduce a new temporal operator which expressed the notion of frequency of events, and define probabilistic frequency temporal logic (PFTL) based on CTL\star. As a result, we can easily represent the temporal properties of behavior in probabilistic systems. However, it is difficult to develop a model checker for the full PFTL, due to rich expressiveness. Accordingly, we develop a model-checking algorithm for the CTL-like fragment of PFTL against finite-state Markov chains, and an approximate model-checking algorithm for the bounded Linear Temporal Logic (LTL) -like fragment of PFTL against countable-state Markov chains. △ Less

Submitted 14 November, 2011; originally announced November 2011.

Comments: In Proceedings INFINITY 2011, arXiv:1111.2678

Journal ref: EPTCS 73, 2011, pp. 79-93