Showing 1–13 of 13 results for author: Chaki, S

Communication Trade-offs in Federated Learning of Spiking Neural Networks

Authors: Soumi Chaki, David Weinberg, Ayca Özcelikkale

Abstract: Spiking Neural Networks (SNNs) are biologically inspired alternatives to conventional Artificial Neural Networks (ANNs). Despite promising preliminary results, the trade-offs in the training of SNNs in a distributed scheme are not well understood. Here, we consider SNNs in a federated learning setting where a high-quality global model is created by aggregating multiple local models from the client… ▽ More Spiking Neural Networks (SNNs) are biologically inspired alternatives to conventional Artificial Neural Networks (ANNs). Despite promising preliminary results, the trade-offs in the training of SNNs in a distributed scheme are not well understood. Here, we consider SNNs in a federated learning setting where a high-quality global model is created by aggregating multiple local models from the clients without sharing any data. We investigate federated learning for training multiple SNNs at clients when two mechanisms reduce the uplink communication cost: i) random masking of the model updates sent from the clients to the server; and ii) client dropouts where some clients do not send their updates to the server. We evaluated the performance of the SNNs using a subset of the Spiking Heidelberg digits (SHD) dataset. The results show that a trade-off between the random masking and the client drop probabilities is crucial to obtain a satisfactory performance for a fixed number of clients. △ Less

Submitted 27 February, 2023; originally announced March 2023.

Comments: 5 pages, 7 figures, 1 algorithm, 1 table

A One class Classifier based Framework using SVDD : Application to an Imbalanced Geological Dataset

Authors: Soumi Chaki, Akhilesh Kumar Verma, Aurobinda Routray, William K. Mohanty, Mamata Jenamani

Abstract: Evaluation of hydrocarbon reservoir requires classification of petrophysical properties from available dataset. However, characterization of reservoir attributes is difficult due to the nonlinear and heterogeneous nature of the subsurface physical properties. In this context, present study proposes a generalized one class classification framework based on Support Vector Data Description (SVDD) to… ▽ More Evaluation of hydrocarbon reservoir requires classification of petrophysical properties from available dataset. However, characterization of reservoir attributes is difficult due to the nonlinear and heterogeneous nature of the subsurface physical properties. In this context, present study proposes a generalized one class classification framework based on Support Vector Data Description (SVDD) to classify a reservoir characteristic water saturation into two classes (Class high and Class low) from four logs namely gamma ray, neutron porosity, bulk density, and P sonic using an imbalanced dataset. A comparison is carried out among proposed framework and different supervised classification algorithms in terms of g metric means and execution time. Experimental results show that proposed framework has outperformed other classifiers in terms of these performance evaluators. It is envisaged that the classification analysis performed in this study will be useful in further reservoir modeling. △ Less

Submitted 2 December, 2016; originally announced December 2016.

Comments: presented at IEEE Students Technology Symposium (TechSym), 28 February to 2 March 2014, IIT Kharagpur, India. 6 pages, 7 figures, 2tables

A Novel Framework based on SVDD to Classify Water Saturation from Seismic Attributes

Authors: Soumi Chaki, Akhilesh Kumar Verma, Aurobinda Routray, William K. Mohanty, Mamata Jenamani

Abstract: Water saturation is an important property in reservoir engineering domain. Thus, satisfactory classification of water saturation from seismic attributes is beneficial for reservoir characterization. However, diverse and non-linear nature of subsurface attributes makes the classification task difficult. In this context, this paper proposes a generalized Support Vector Data Description (SVDD) based… ▽ More Water saturation is an important property in reservoir engineering domain. Thus, satisfactory classification of water saturation from seismic attributes is beneficial for reservoir characterization. However, diverse and non-linear nature of subsurface attributes makes the classification task difficult. In this context, this paper proposes a generalized Support Vector Data Description (SVDD) based novel classification framework to classify water saturation into two classes (Class high and Class low) from three seismic attributes seismic impedance, amplitude envelop, and seismic sweetness. G-metric means and program execution time are used to quantify the performance of the proposed framework along with established supervised classifiers. The documented results imply that the proposed framework is superior to existing classifiers. The present study is envisioned to contribute in further reservoir modeling. △ Less

Submitted 2 December, 2016; originally announced December 2016.

Comments: 6 pages, 8 figures, 2table Presented at Fourth International Conference on Emerging Applications of Information Technology (EAIT 2014), ISI Kolkata, India

A novel multiclassSVM based framework to classify lithology from well logs: a real-world application

Authors: Soumi Chaki, Aurobinda Routray, William K. Mohanty, Mamata Jenamani

Abstract: Support vector machines (SVMs) have been recognized as a potential tool for supervised classification analyses in different domains of research. In essence, SVM is a binary classifier. Therefore, in case of a multiclass problem, the problem is divided into a series of binary problems which are solved by binary classifiers, and finally the classification results are combined following either the on… ▽ More Support vector machines (SVMs) have been recognized as a potential tool for supervised classification analyses in different domains of research. In essence, SVM is a binary classifier. Therefore, in case of a multiclass problem, the problem is divided into a series of binary problems which are solved by binary classifiers, and finally the classification results are combined following either the one-against-one or one-against-all strategies. In this paper, an attempt has been made to classify lithology using a multiclass SVM based framework using well logs as predictor variables. Here, the lithology is classified into four classes such as sand, shaly sand, sandy shale and shale based on the relative values of sand and shale fractions as suggested by an expert geologist. The available dataset consisting well logs (gamma ray, neutron porosity, density, and P-sonic) and class information from four closely spaced wells from an onshore hydrocarbon field is divided into training and testing sets. We have used one-against-all strategy to combine the results of multiple binary classifiers. The reported results established the superiority of multiclass SVM compared to other classifiers in terms of classification accuracy. The selection of kernel function and associated parameters has also been investigated here. It can be envisaged from the results achieved in this study that the proposed framework based on multiclass SVM can further be used to solve classification problems. In future research endeavor, seismic attributes can be introduced in the framework to classify the lithology throughout a study area from seismic inputs. △ Less

Submitted 2 December, 2016; originally announced December 2016.

Comments: 5 pages, 5 figures, 4 tables Presented at INDICON 2015 at New Delhi, India

Development of a hybrid learning system based on SVM, ANFIS and domain knowledge: DKFIS

Authors: Soumi Chaki, Aurobinda Routray, William K. Mohanty, Mamata Jenamani

Abstract: This paper presents the development of a hybrid learning system based on Support Vector Machines (SVM), Adaptive Neuro-Fuzzy Inference System (ANFIS) and domain knowledge to solve prediction problem. The proposed two-stage Domain Knowledge based Fuzzy Information System (DKFIS) improves the prediction accuracy attained by ANFIS alone. The proposed framework has been implemented on a noisy and inco… ▽ More This paper presents the development of a hybrid learning system based on Support Vector Machines (SVM), Adaptive Neuro-Fuzzy Inference System (ANFIS) and domain knowledge to solve prediction problem. The proposed two-stage Domain Knowledge based Fuzzy Information System (DKFIS) improves the prediction accuracy attained by ANFIS alone. The proposed framework has been implemented on a noisy and incomplete dataset acquired from a hydrocarbon field located at western part of India. Here, oil saturation has been predicted from four different well logs i.e. gamma ray, resistivity, density, and clay volume. In the first stage, depending on zero or near zero and non-zero oil saturation levels the input vector is classified into two classes (Class 0 and Class 1) using SVM. The classification results have been further fine-tuned applying expert knowledge based on the relationship among predictor variables i.e. well logs and target variable - oil saturation. Second, an ANFIS is designed to predict non-zero (Class 1) oil saturation values from predictor logs. The predicted output has been further refined based on expert knowledge. It is apparent from the experimental results that the expert intervention with qualitative judgment at each stage has rendered the prediction into the feasible and realistic ranges. The performance analysis of the prediction in terms of four performance metrics such as correlation coefficient (CC), root mean square error (RMSE), and absolute error mean (AEM), scatter index (SI) has established DKFIS as a useful tool for reservoir characterization. △ Less

Submitted 2 December, 2016; originally announced December 2016.

Comments: 6 pages, 5 figures, 3tables Presented at Indicon 2015

Well Tops Guided Prediction of Reservoir Properties using Modular Neural Network Concept A Case Study from Western Onshore, India

Authors: Soumi Chaki, Akhilesh K Verma, Aurobinda Routray, William K Mohanty, Mamata Jenamani

Abstract: This paper proposes a complete framework consisting pre-processing, modeling, and post-processing stages to carry out well tops guided prediction of a reservoir property (sand fraction) from three seismic attributes (seismic impedance, instantaneous amplitude, and instantaneous frequency) using the concept of modular artificial neural network (MANN). The data set used in this study comprising thre… ▽ More This paper proposes a complete framework consisting pre-processing, modeling, and post-processing stages to carry out well tops guided prediction of a reservoir property (sand fraction) from three seismic attributes (seismic impedance, instantaneous amplitude, and instantaneous frequency) using the concept of modular artificial neural network (MANN). The data set used in this study comprising three seismic attributes and well log data from eight wells, is acquired from a western onshore hydrocarbon field of India. Firstly, the acquired data set is integrated and normalized. Then, well log analysis and segmentation of the total depth range into three different units (zones) separated by well tops are carried out. Secondly, three different networks are trained corresponding to three different zones using combined data set of seven wells and then trained networks are validated using the remaining test well. The target property of the test well is predicted using three different tuned networks corresponding to three zones; and then the estimated values obtained from three different networks are concatenated to represent the predicted log along the complete depth range of the testing well. The application of multiple simpler networks instead of a single one improves the prediction accuracy in terms of performance metrics such as correlation coefficient, root mean square error, absolute error mean and program execution time. △ Less

Submitted 23 September, 2015; originally announced September 2015.

Comments: in Journal of Petroleum Science and Engineering, 2014

Quantification of sand fraction from seismic attributes using Neuro-Fuzzy approach

Authors: Akhilesh K Verma, Soumi Chaki, Aurobinda Routray, William K Mohanty, Mamata Jenamani

Abstract: In this paper, we illustrate the modeling of a reservoir property (sand fraction) from seismic attributes namely seismic impedance, seismic amplitude, and instantaneous frequency using Neuro-Fuzzy (NF) approach. Input dataset includes 3D post-stacked seismic attributes and six well logs acquired from a hydrocarbon field located in the western coast of India. Presence of thin sand and shale layers… ▽ More In this paper, we illustrate the modeling of a reservoir property (sand fraction) from seismic attributes namely seismic impedance, seismic amplitude, and instantaneous frequency using Neuro-Fuzzy (NF) approach. Input dataset includes 3D post-stacked seismic attributes and six well logs acquired from a hydrocarbon field located in the western coast of India. Presence of thin sand and shale layers in the basin area makes the modeling of reservoir characteristic a challenging task. Though seismic data is helpful in extrapolation of reservoir properties away from boreholes; yet, it could be challenging to delineate thin sand and shale reservoirs using seismic data due to its limited resolvability. Therefore, it is important to develop state-of-art intelligent methods for calibrating a nonlinear map** between seismic data and target reservoir variables. Neural networks have shown its potential to model such nonlinear map**s; however, uncertainties associated with the model and datasets are still a concern. Hence, introduction of Fuzzy Logic (FL) is beneficial for handling these uncertainties. More specifically, hybrid variants of Artificial Neural Network (ANN) and fuzzy logic, i.e., NF methods, are capable for the modeling reservoir characteristics by integrating the explicit knowledge representation power of FL with the learning ability of neural networks. The documented results in this study demonstrate acceptable resemblance between target and predicted variables, and hence, encourage the application of integrated machine learning approaches such as Neuro-Fuzzy in reservoir characterization domain. Furthermore, visualization of the variation of sand probability in the study area would assist in identifying placement of potential wells for future drilling operations. △ Less

Submitted 23 September, 2015; originally announced September 2015.

Comments: Journal of Applied Geophysics, volume 111, page 141-155

A Novel Pre-processing Scheme to Improve the Prediction of Sand Fraction from Seismic Attributes using Neural Networks

Authors: Soumi Chaki, Aurobinda Routray, William K. Mohanty

Abstract: This paper presents a novel pre-processing scheme to improve the prediction of sand fraction from multiple seismic attributes such as seismic impedance, amplitude and frequency using machine learning and information filtering. The available well logs along with the 3-D seismic data have been used to benchmark the proposed pre-processing stage using a methodology which primarily consists of three s… ▽ More This paper presents a novel pre-processing scheme to improve the prediction of sand fraction from multiple seismic attributes such as seismic impedance, amplitude and frequency using machine learning and information filtering. The available well logs along with the 3-D seismic data have been used to benchmark the proposed pre-processing stage using a methodology which primarily consists of three steps: pre-processing, training and post-processing. An Artificial Neural Network (ANN) with conjugate-gradient learning algorithm has been used to model the sand fraction. The available sand fraction data from the high resolution well logs has far more information content than the low resolution seismic attributes. Therefore, regularization schemes based on Fourier Transform (FT), Wavelet Decomposition (WD) and Empirical Mode Decomposition (EMD) have been proposed to shape the high resolution sand fraction data for effective machine learning. The input data sets have been segregated into training, testing and validation sets. The test results are primarily used to check different network structures and activation function performances. Once the network passes the testing phase with an acceptable performance in terms of the selected evaluators, the validation phase follows. In the validation stage, the prediction model is tested against unseen data. The network yielding satisfactory performance in the validation stage is used to predict lithological properties from seismic attributes throughout a given volume. Finally, a post-processing scheme using 3-D spatial filtering is implemented for smoothing the sand fraction in the volume. Prediction of lithological properties using this framework is helpful for Reservoir Characterization. △ Less

Submitted 23 September, 2015; originally announced September 2015.

Comments: 13 pages, volume 8, no 4, pp. 1808-1820, April 2015 in IEE Journal of Selected Topics in Applied Earth Observations and Remote Sensing, 2015

Reservoir Characterization: A Machine Learning Approach

Authors: Soumi Chaki

Abstract: Reservoir Characterization (RC) can be defined as the act of building a reservoir model that incorporates all the characteristics of the reservoir that are pertinent to its ability to store hydrocarbons and also to produce them.It is a difficult problem due to non-linear and heterogeneous subsurface properties and associated with a number of complex tasks such as data fusion, data mining, formulat… ▽ More Reservoir Characterization (RC) can be defined as the act of building a reservoir model that incorporates all the characteristics of the reservoir that are pertinent to its ability to store hydrocarbons and also to produce them.It is a difficult problem due to non-linear and heterogeneous subsurface properties and associated with a number of complex tasks such as data fusion, data mining, formulation of the knowledge base, and handling of the uncertainty.This present work describes the development of algorithms to obtain the functional relationships between predictor seismic attributes and target lithological properties. Seismic attributes are available over a study area with lower vertical resolution. Conversely, well logs and lithological properties are available only at specific well locations in a study area with high vertical resolution.Sand fraction, which represents per unit sand volume within the rock, has a balanced distribution between zero to unity.The thesis addresses the issues of handling the information content mismatch between predictor and target variables and proposes regularization of target property prior to building a prediction model.In this thesis, two Artificial Neural Network (ANN) based frameworks are proposed to model sand fraction from multiple seismic attributes without and with well tops information respectively. The performances of the frameworks are quantified in terms of Correlation Coefficient, Root Mean Square Error, Absolute Error Mean, etc. △ Less

Submitted 22 July, 2015; v1 submitted 15 June, 2015; originally announced June 2015.

Comments: Supervisors: Prof. Aurobinda Routray and Prof. William K. Mohanty

Scalable Testing of Context-Dependent Policies over Stateful Data Planes with Armstrong

Authors: Seyed K. Fayaz, Yoshiaki Tobioka, Sagar Chaki, Vyas Sekar

Abstract: Network operators today spend significant manual effort in ensuring and checking that the network meets their intended policies. While recent work in network verification has made giant strides to reduce this effort, they focus on simple reachability properties and cannot handle context-dependent policies (e.g., how many connections has a host spawned) that operators realize using stateful network… ▽ More Network operators today spend significant manual effort in ensuring and checking that the network meets their intended policies. While recent work in network verification has made giant strides to reduce this effort, they focus on simple reachability properties and cannot handle context-dependent policies (e.g., how many connections has a host spawned) that operators realize using stateful network functions (NFs). Together, these introduce new expressiveness and scalability challenges that fall outside the scope of existing network verification mechanisms. To address these challenges, we present Armstrong, a system that enables operators to test if network with stateful data plane elements correctly implements a given context-dependent policy. Our design makes three key contributions to address expressiveness and scalability: (1) An abstract I/O unit for modeling network I/O that encodes policy-relevant context information; (2) A practical representation of complex NFs via an ensemble of finite state machines abstraction; and (3) A scalable application of symbolic execution to tackle state space explosion. We demonstrate that Armstrong is several orders of magnitude faster than existing mechanisms. △ Less

Submitted 8 June, 2015; v1 submitted 13 May, 2015; originally announced May 2015.

SMT-based Model Checking for Recursive Programs

Authors: Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki

Abstract: We present an SMT-based symbolic model checking algorithm for safety verification of recursive programs. The algorithm is modular and analyzes procedures individually. Unlike other SMT-based approaches, it maintains both "over-" and "under-approximations" of procedure summaries. Under-approximations are used to analyze procedure calls without inlining. Over-approximations are used to block infeasi… ▽ More We present an SMT-based symbolic model checking algorithm for safety verification of recursive programs. The algorithm is modular and analyzes procedures individually. Unlike other SMT-based approaches, it maintains both "over-" and "under-approximations" of procedure summaries. Under-approximations are used to analyze procedure calls without inlining. Over-approximations are used to block infeasible counterexamples and detect convergence to a proof. We show that for programs and properties over a decidable theory, the algorithm is guaranteed to find a counterexample, if one exists. However, efficiency depends on an oracle for quantifier elimination (QE). For Boolean Programs, the algorithm is a polynomial decision procedure, matching the worst-case bounds of the best BDD-based algorithms. For Linear Arithmetic (integers and rationals), we give an efficient instantiation of the algorithm by applying QE "lazily". We use existing interpolation techniques to over-approximate QE and introduce "Model Based Projection" to under-approximate QE. Empirical evaluation on SV-COMP benchmarks shows that our algorithm improves significantly on the state-of-the-art. △ Less

Submitted 25 May, 2014; v1 submitted 15 May, 2014; originally announced May 2014.

Comments: originally published as part of the proceedings of CAV 2014; fixed typos, better wording at some places

Automatic Abstraction in SMT-Based Unbounded Software Model Checking

Authors: Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke

Abstract: Software model checkers based on under-approximations and SMT solvers are very successful at verifying safety (i.e. reachability) properties. They combine two key ideas -- (a) "concreteness": a counterexample in an under-approximation is a counterexample in the original program as well, and (b) "generalization": a proof of safety of an under-approximation, produced by an SMT solver, are generaliza… ▽ More Software model checkers based on under-approximations and SMT solvers are very successful at verifying safety (i.e. reachability) properties. They combine two key ideas -- (a) "concreteness": a counterexample in an under-approximation is a counterexample in the original program as well, and (b) "generalization": a proof of safety of an under-approximation, produced by an SMT solver, are generalizable to proofs of safety of the original program. In this paper, we present a combination of "automatic abstraction" with the under-approximation-driven framework. We explore two iterative approaches for obtaining and refining abstractions -- "proof based" and "counterexample based" -- and show how they can be combined into a unified algorithm. To the best of our knowledge, this is the first application of Proof-Based Abstraction, primarily used to verify hardware, to Software Verification. We have implemented a prototype of the framework using Z3, and evaluate it on many benchmarks from the Software Verification Competition. We show experimentally that our combination is quite effective on hard instances. △ Less

Submitted 8 June, 2013; originally announced June 2013.

Comments: Extended version of a paper in the proceedings of CAV 2013

Verification Across Intellectual Property Boundaries

Authors: Sagar Chaki, Christian Schallhart, Helmut Veith

Abstract: In many industries, the importance of software components provided by third-party suppliers is steadily increasing. As the suppliers seek to secure their intellectual property (IP) rights, the customer usually has no direct access to the suppliers' source code, and is able to enforce the use of verification tools only by legal requirements. In turn, the supplier has no means to convince the custom… ▽ More In many industries, the importance of software components provided by third-party suppliers is steadily increasing. As the suppliers seek to secure their intellectual property (IP) rights, the customer usually has no direct access to the suppliers' source code, and is able to enforce the use of verification tools only by legal requirements. In turn, the supplier has no means to convince the customer about successful verification without revealing the source code. This paper presents an approach to resolve the conflict between the IP interests of the supplier and the quality interests of the customer. We introduce a protocol in which a dedicated server (called the "amanat") is controlled by both parties: the customer controls the verification task performed by the amanat, while the supplier controls the communication channels of the amanat to ensure that the amanat does not leak information about the source code. We argue that the protocol is both practically useful and mathematically sound. As the protocol is based on well-known (and relatively lightweight) cryptographic primitives, it allows a straightforward implementation on top of existing verification tool chains. To substantiate our security claims, we establish the correctness of the protocol by cryptographic reduction proofs. △ Less

Submitted 30 November, 2011; v1 submitted 29 January, 2007; originally announced January 2007.