Marcell J. Vazquez-Chanlatte

Research Interests

• Human-Robot Interaction
• Learning via Demonstrations
• Specification Inference
• Safety and AI

Education

Experience

1. 2020

   Google, Mountain View, CA: Researched techniques (e.g. Hindsight Experience Replay) for improving the sample complexity and exploration capabilities of the deephol neural network guided theorem prover. Primary challenges included managing combinatorial action spaces and sparse feedback signals.

2. 2019

   VMWare, Palo Alto, CA: Researched adapting classic automata query learning algorithms for extracting Moore Machines from Recurrent Neural Networks.

3. 2017

   SRI International, Menlo Park, CA: Began researching inference of specifications, such as temporal logic, from unlabeled (potentially noisy demonstrations). See Learning Task Specifications Research Project.

4. 2016

   Toyota, Gardena, CA: Worked in the Power Train Controls Department designing tools to mine temporal logic specifications from data. See Logical Clustering of Time-Series Data Research Project.

5. 2015

   Google, Pittsburgh, PA: Google Shopping Image Selection: Designed metrics Google, Pittsburgh, PA: Google Shopping Image Selection: Designed user study algorithm for determining which images users prefer to represent a given item. Used to measure effectiveness of automated image selection.

6. 2014

   Mozilla, Mountain View, CA: Helped add C/Javascript search functionality for Mozilla’s Code search tool DXR.

7. 2012/13

   Qualcomm, Boulder, CO/San Diego, CA: Helped develop an internal framework for testing of prototypes.

Publications

1. Lauffer, Niklas, Yalcinkaya, Beyazit, Vazquez-Chanlatte, Marcell, Shah, Ameesh, and Seshia. Sanjit A. "Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations." FMCAD (2022).
2. Vazquez-Chanlatte, Marcell, Junges, Sebastian, Daniel J. Fremont, Sanjit A. Seshia. "Entropy Guided Control Improvisation" (RSS 2021).
3. Junges, Sebastian, Seven Holtzen, Marcell Vazquez-Chanlatte, Todd Millstein, Guy Van den Broerk, Sanjit A. Seshia. "Model Checking Finite-Horizon Markov Chains with Probabilistic Inference" (CAV 2021).
4. 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.
5. Dreossi, Tommaso, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Hadi Ravanbakhsh, Marcell Vazquez-Chanlatte, and Sanjit A. Seshia. "Verifai: A toolkit for the formal design and analysis of artificial intelligence-based systems." In International Conference on Computer Aided Verification, pp. 432-442. Springer, Cham, 2019.
6. Seshia, Sanjit A., Ankush Desai, Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Sumukh Shivakumar, Marcell Vazquez-Chanlatte, and Xiangyu Yue. "Formal specification for deep neural networks." In International Symposium on Automated Technology for Verification and Analysis, pp. 20-34. Springer, Cham, 2018.
7. (Extended Abstract) Vazquez-Chanlatte, Marcell , et al. "Communicating Compositional and Temporal Specifications by Demonstration." IFAC Conference on Cyber-Physical & Human Systems. CPHS, 2018
8. Vazquez-Chanlatte, Marcell , Susmit Jha, Ashish Tiwari, Mark K. Ho, and Sanjit A. Seshia. "Learning Task Specifications from Demonstrations." In NeurIPS. 2018.
9. 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.
10. 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.
11. Vazquez-Chanlatte, Marcell, Jyotirmoy V. Deshmukh, Xiaoqing Jin, and Sanjit A. Seshia. "Logical clustering and learning for time-series data." In International Conference on Computer Aided Verification, pp. 305-325. Springer, Cham, 2017.

In Preparation for Publication and Preprints

1. Vazquez-Chanlatte, Marcell, Gil Lederman, Ameesh Shah, and Sanjit A. Seshia. "Demonstration Informed Specification Search", arXiv preprint arXiv:2112.10807 (2022, In submission)
2. Ameesh Shah, Vazquez-Chanlatte, Marcell, Sebastian Junges, and Sanjit A. Seshia. "Learning Concepts from Preference and Membership Queries", (2022, In submission)
3. Vazquez-Chanlatte, Marcell, Markus N. Rabe, and Sanjit A. Seshia. "A Model Counter's Guide to Probabilistic Systems." arXiv preprint arXiv:1903.09354 (2019).

Academic Service Activities

• Program Committee member for Association for the Advancement of Artificial Intelligence Conference (AAAI 2023)
• Program Committee member for Computer Aided Verification (CAV 2023)
• Program Committee member for Hybrid Systems and Control Conference (HSCC 2023)
• Program Committee member for Artifact Evaluation at Tools and Algorithms for the Construction and Analysis of Systems (TACAS 20)
• Reviewer for Automatica Journal (2020).
• Reviewer for Automonous Robotics (AURO 2021)
• Reviewer for Conference on Computer Aided Verification (CAV 2017-2021).
• Reviewer for Conference on Hybrid Systems: Computation and Control (HSCC 2017, 2018)
• Reviewer for Conference on Intelligent Robots and Systems (IROS 2020)
• Reviewer for Conference on Robot Learning (CoRL 2019)
• Reviewer for Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018).
• Reviewer for International Conference on Learning Representations (ICLR 2022-2023)
• Reviewer for International Conference on Machine Learning (ICML 2022)
• Reviewer for International Conference on Robotics and Automation (ICRA 2017-2021)
• Reviewer for Neural Information Processing Systems (NeurIPS 2021, 2022)
• Reviewer for Robotics: Science and Systems (RSS 2019, 2020)
• Student Coordinator for VeHICaL , an NSF Cyber-Physical Systems (CPS) Frontier project on Verified Human Interfaces, Control, and Learning for Semi-Autonomous Systems.
• Webmaster for 23rd ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2020)

Highlighted Software

I am the primary developer and maintainer of a number of widely used Python packages (over 25). A subset are listed below.

Time Series Analysis

• py-metric-temporal logic: A library for manipulating and evaluating metric temporal logic expressions over time series data. Known uses in code for falsification of Neural Networks and teaching embedded systems (EECS 149).
• Discrete Signal: A Time-Series Embedded Domain Specific Language used to manipulate time series. Used in py-metric-temporal logic.

Symbolic models of transition systems

• py-aiger : A popular python library for manipulating logic sequential circuits.
  • Used as the basis for the larger py-aiger eco system for modeling and studying (i) Automata, (ii) Stochastic Games and Markov Decision Processes (iii) Bounded Verification of Markov Chains (iv) Past Tense Temporal Logic.
  • One of the primary supported inputs for the award winning pySAT package which provides a unified interface to a number of state-of-the-art Boolean satisifability (SAT).
  • Used to create large data sets for training Neural Networks manipulate and solve temporal and propositional logic.

Learning Specifications and Controlled Improvisation

• Improvisers Reference Implementation of the Entropy Guided Recative Control Improvisation algorithm and our CAV 2020 Maximum Entropy Specification Inference algorithm.
• Logical Lens A reference implementation for the Logical Clustering algorithm presented at CAV 2017 and RV 2018.
• Monotone-Bipartition Library for manipulating and comparing implicitly defined monotone bipartitions on the unit box. Implement's Oded Maler's algorithm for representing the pareto front of a sub-class of multi-objective optimization. Used heavily in Logical Lens.
• DISS: Demonstration Informed Specification Search" Reference Implementation of algorithm for learning formal task specifications from demonstrations.
• lstar : Python implementation of discriminant tree variant of lstar, an automata learning algorithm. Used as post-processing step in learning specifications from demonstrations.
• dfa-identify : Python implementation of DFA identification from labeled examples via reduction to SAT.

Teaching - Graduate Student Instruction

• Spring 2018 Formal Methods: Specification, Verification, and Synthesis (EECS 219C)
• Fall 2018 Introduction to Embedded Systems (EECS 149)

Awards and Honors

• University of California, Berkeley, Eli Jury Award for outstanding achievement in the area of systems, communications, control, or signal processing (2021-2022)
• University of California, Berkeley, EECS Excellence Award (2015)
• University of Illinois, James Scholar (2011-2015)
• University of Illinois, Physics - High Distinction (2011-2015)
• University of Illinois, Computer Science - Honors (2011-2015)

Other

• Python (PyTorch, Tensorflow, Jax)
• C
• Haskell
• Java
• Rust

• Algorithmic Human Robot Interaction
• Artificial Intelligence
• Compilers and Programming Languages
• Computational Complexity
• Computational Models of Cognition
• Computer Aided Verification
• Computer Architecture
• Computer Graphics
• Embedded Systems
• Formal Verification of Cyber-Physical Systems
• Fundamental Algorithms and Data Structures
• Information Theory
• Machine Learning and Signal Processing
• Non-Linear Systems
• Numerical Analysis
• Theory of Computation