Author name cluster

Akshay Agrawal

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

2 author rows

NeurIPS Conference 2019 Conference Paper

Differentiable Convex Optimization Layers

Akshay Agrawal
Brandon Amos
Shane Barratt
Stephen Boyd
Steven Diamond
J. Zico Kolter

Recent work has shown how to embed differentiable optimization problems (that is, problems whose solutions can be backpropagated through) as layers within deep learning architectures. This method provides a useful inductive bias for certain problems, but existing software for differentiable optimization layers is rigid and difficult to apply to new settings. In this paper, we propose an approach to differentiating through disciplined convex programs, a subclass of convex optimization problems used by domain-specific languages (DSLs) for convex optimization. We introduce disciplined parametrized programming, a subset of disciplined convex programming, and we show that every disciplined parametrized program can be represented as the composition of an affine map from parameters to problem data, a solver, and an affine map from the solver’s solution to a solution of the original problem (a new form we refer to as affine-solver-affine form). We then demonstrate how to efficiently differentiate through each of these components, allowing for end-to-end analytical differentiation through the entire convex program. We implement our methodology in version 1. 1 of CVXPY, a popular Python-embedded DSL for convex optimization, and additionally implement differentiable layers for disciplined convex programs in PyTorch and TensorFlow 2. 0. Our implementation significantly lowers the barrier to using convex optimization problems in differentiable programs. We present applications in linear machine learning models and in stochastic control, and we show that our layer is competitive (in execution time) compared to specialized differentiable solvers from past work.

PDF Details

FormaliSE Conference 2014 Conference Paper

Formalization of software models for cyber-physical systems

Sandeep Neema
Gabor Simko
Tihamer Levendovszky
Joseph Porter
Akshay Agrawal
Janos Sztipanovits

The involvement of formal methods is indispensable for modern software engineering. This especially holds for Cyber-Physical Systems (CPS). In order to deal with the complexity and heterogeneity of the design, model-based engineering is widely used. The complexity of detailed verification in the final source code makes it imperative to introduce formal methods earlier in the design process. Because of the widespread use of customized modeling languages (domain-specific modeling languages, DSMLs), it is crucial to formally specify the DSML, and verify if the model meets fundamental correctness criteria. This is achieved by specifying behavioral and structural semantics of the modeling language. Significant model-driven tools have emerged incorporating advanced model checking methods that can provide some assurance regarding the quality and correctness of the models. However, the code generated from these models, using auto code generators remains circumspect, since the correctness of the code generators cannot be assumed as a given, and remains intractable to prove. Therefore, we propose a pragmatic approach, instead of verifying explicit implementation of code generator, verifies the correctness of the generated code with respect to a specific set of user-defined properties to establish that the code-generators are property-preserving. In order to make the verification workflow conducive to domain engineers, who are not often trained in formal methods, we include a mechanism for high-level specification of temporal properties using pattern-based verification templates. The presented toolchain leverages state-of-the-art verification tools, and a small case-study illustrates the approach.

Details