| CARVIEW |
Marcell J. Vazquez-Chanlatte
About Me
Dr. Elizabeth Polgreen.
Click here to see Original
I received my PhD in Computer Science at the University of California, Berkeley advised by Prof. Sanjit A. Sesha; and received a B.S. in Computer Science and a B.S. Physics at the University of Illinois at Urbana-Champaign. I have also spent time at VMWare, SRI, Toyota, Google, Mozilla, and Qualcomm. I am currently an AI Research Scientist at Nissan's Alliance Innovation Lab, Silicon Valley.
Please take the time to explore this site and learn more about my research interests, active software projects, and publications.
Research Interests 🔬
My research interests span the areas of Human Robot Interaction, Formal Methods, Robotics, and Safety in Artificial Intelligence.
During my PhD dissertation my focus was on learning formal specifications, e.g., automata, logic or programs, from expert demonstrations and using demonstrations to teach back the learned formal specifications.
Post Phd: Since graduating, I've had opportunities to have more hands on automotive experience and run a machine learning research group. Our interests include, but are not limited to, data-driven prediction and understanding of driving scenes.
University collaborations have resulted in work ranging from natural language informed map reconstruction, using DMV crash reports to reconstruct driving scenarios, learning automata using natural language and expert demonstrations, and embedding automata for use in multi-task RL.
A full list of my research can be found on my google scholar profile.
PhD Dissertation
Committee Sanjit A. Seshia, Chair, S. Shankar Sastry, Professor Anca Dragan, Professor Steven Piantadosi
Select Software Projects 💻
See Github for a more exhaustive list.
Sequential Circuits
pyAiger: A python library for convenient modeling/ manipulation of sequential circuits, combinatorial circuits, and boolean expressions represented as (A)nd (I)nverter (G)ates (AIGs). Co-developed with Markus N. Rabe.
pyAiger-BV: Word Level (bitvector) abstractions on top of pyAiger. Co-developed with Markus N. Rabe.
There are a number of other projects that I have spawned off the py-aiger code base for supporting bdds, SAT solvers, past tense LTL, gridworlds, and conversion to and from DFAs.
Time-Series
py-Metric-Temporal-Logic: Python library for working with Metric Temporal Logic (MTL). Metric Temporal Logic is an extension of Linear Temporal Logic (LTL) for specifying properties over time series.
DiscreteSignals: A Python embedded domain specific language for modeling and manipulating discrete time signals. The key distinction between many other timeseries libraries is the lightweight encoding of non-uniform time steps. This abstraction made implementing the py-Metric-Temporal-Logic library much easier.
Specification Inference
Demonstration Informed Specification Search (DISS): a tool for learning "Boolean Task Specifications", in the form of automata or logic, from demonstrations.
Gridworld Visualizer: Python Code for visualizing gridworlds used in my research
Monotone Bipartition:
This library enable manipulating and comparing implicitly
defined monotone bipartitions on the unit box using
adaptive mesh refinement.
Inspired by
Maler, Oded. "Learning Monotone Partitions of Partially-Ordered Domains
(Work in Progress)." (2017). and the main work horse our series of
papers on Logical Lens and Logical Clustering.
Logical Lens:0 Implementation of Logical Lens algorithm for (1) using a parametric specification to map data to an abstract boundary and (2) compute the induced "Logical Distance" between data w.r.t. a parametric specification.
Automata
DFA: A simple python implementation of a Deterministic Finite Automata and Moore Machines. Notable features include implicit/lazy definitions, immutable/frozen design, and hashability.
lstar: Python implementation of the discriminant tree for learning DFA and Moore Machines from membership and equivalence queries. Supports a co-routine API for interfacing with other learning algorithms. Works well with my dfa library :)
dfa-identify: Python implementation of SAT based Deterministic Finite Automata identification from a set of accepting and rejecting strings.
Other
Lazy Tree: Python library for manipulating infinite trees. Used in a number of my libraries. For example, the adaptive mesh-refinement in monotone-bipartition and the counterexample search tree in lstar. Useful when a problem can be framed as a search on infinite trees which themselves may be functions of infinite trees.
Select Publications 📃
Please consult Google Scholar for a more complete list.
Preprints
Publications
-
Lauffer, Niklas, Yalcinkaya Beyazit,
Vazquez-Chanlatte, Marcell, Shah,
Ameesh, Seshia, Sanjit A.,
"Learning Deterministic Finite Automata Decompositions
from Examples and Demonstrations." Formal Methods in
Computer-Aided Design 2022
pdf arxiv slides -
Vazquez-Chanlatte, Marcell, Junges,
Sebastian, Daniel J. Fremont, Sanjit A. Seshia. "Entropy
Guided Control Improvisation", Robotics Science and Systems 2021
pdf arxiv slides video -
Junges, Sebastian, Steven Holtzen, Marcell
Vazquez-Chanlatte, Todd Millstein, Guy Van den Broerk, Sanjit
A. Seshia. "Model Checking Finite-Horizon Markov Chains with
Probabilistic Inference", In International Conference on
Computer Aided Verification, 2021.
arxiv -
Vazquez-Chanlatte, Marcell, and Sanjit
A. Seshia. "Maximum Causal Entropy Specification Inference
from Demonstrations." In International Conference on
Computer Aided Verification, pp. 255-278. Springer, Cham,
2020.
pdf arxiv bibtex slides CAV 2020 Talk -
Vazquez-Chanlatte, Marcell , Susmit
Jha, Ashish Tiwari, Mark K. Ho, and Sanjit
A. Seshia. "Learning Task Specifications from
Demonstrations." In NeurIPS. 2018.
pdf arxiv bibtex - (Extended Abstract) Vazquez-Chanlatte, Marcell , et al. "Communicating Compositional and Temporal Specifications by Demonstration." IFAC Conference on Cyber-Physical & Human Systems. CPHS, 2018
-
Vazquez-Chanlatte, Marcell, Shromona
Ghosh, Jyotirmoy V. Deshmukh, Alberto
Sangiovanni-Vincentelli, and Sanjit
A. Seshia. "Time-series learning using monotonic logical
properties." In International Conference on Runtime
Verification, pp. 389-405. Springer, Cham, 2018.
pdf arxiv bibtex slides - Vazquez-Chanlatte, Marcell J., Shromona Ghosh, Vasumathi Raman, Alberto Sangiovanni-Vincentelli, and Sanjit A. Seshia. "Generating dominant strategies for continuous two-player zero-sum games." IFAC-PapersOnLine 51, no. 16 (2018): 7-12.
-
Vazquez-Chanlatte, Marcell, Jyotirmoy V. Deshmukh,
Xiaoqing Jin, and Sanjit A. Seshia.
"Logical Clustering and Learning for Time-Series Data."
pdf arxiv bibtex