Publications | Mike He

crush: Extensible Proof Automation for Lean

Mike He, Dexin Zhang, Aarti Gupta

ArXiV · 2026

Paper Code

Soteria: Formally Verified Planning with Runtime Enforcement for Safe LLM Agents

Mike He, Ankush Desai, Sharad Malik, Aarti Gupta

Neural Information Processing Systems (NeurIPS), To Appear · 2026 Oral

Specy: Learning Specifications for Distributed Systems from Event Traces

Mike He, Ankush Desai, Aishwarya Jagarapu, Doug Terry, Sharad Malik, Aarti Gupta

Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) · 2026

Paper Code

AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms

Haoyu Zhao*, Ziran Yang*, Jiawei Li*, Deyuan He*, Zenan Li*, Chi Jin, Venugopal V. Veeravalli, Aarti Gupta, Sanjeev Arora

International Conference on Machine Learning (ICML) · 2026 Spotlight

Paper Code

Göedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification

Zenan Li*, Ziran Yang*, Deyuan He, Haoyu Zhao, Andrew Zhao, Shange Tang, Kaiyu Yang, Aarti Gupta, Zhendong Su, Chi Jin

Conference on Language Modeling (COLM) · 2026

Project Paper Code

Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases

Marcus Min, Mike He, Zhaoyu Li, Zixuan Yi, Sharad Malik, Aarti Gupta, Xujie Si, Osbert Bastani

International Conference on Machine Learning (ICML), Position Track · 2026 Spotlight

Paper

Verification of Compiler-to-Accelerator Mappings for Machine Learning Accelerators

Akash Gaonkar, Mike He, Yi Li, Bo-Yuan Huang, Andrew Cheung, Vishal Canumalla, Gus Smith, Zachary Tatlock, Grigory Fedyukovich, Sharad Malik, Aarti Gupta

ArXiV · 2026

Paper

A benchmark of expert-level academic questions to assess AI capabilities

Center for AI Safety, Scale AI, HLE Contributors Consortium

Nature · 2026

Project Paper Code

Ranking Formal Specifications using LLMs

Mike He, Zhendong Ang, Ankush Desai, Aarti Gupta

Proceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages · 2025

Project Paper Code

Application-level Validation of Accelerator Designs Using a Formal Software/Hardware Interface

Bo-Yuan Huang, Steven Lyubomirsky, Yi Li, Mike He, Gus Henry Smith, Thierry Tambe, Akash Gaonkar, Vishal Canumalla, Andrew Cheung, Gu-Yeon Wei, Aarti Gupta, Zachary Tatlock, Sharad Malik

ACM Trans. Des. Autom. Electron. Syst. (TODAES) · 2024

Project Paper

Improving Term Extraction with Acyclic Constraints

Mike He, Haichen Dong, Sharad Malik, Aarti Gupta

E-Graph Research, Applications, Practices, and Human-factors Symposium (PLDI/EGRAPHS'23) · 2023

Project Paper Code

Dynamic Tensor Rematerialization

Marisa Kirisame*, Steven Lyubomirsky*, Altan Haan*, Jennifer Brennan, Mike He, Jared Roesch, Tianqi Chen, Zachary Tatlock

International Conference on Learning Representations (ICLR) · 2021 Spotlight

Project Paper Code

From DSLs to Accelerator-rich Platform Implementations: Addressing the Mapping Gap

Bo-Yuan Huang*, Steven Lyubomirsky*, Thierry Tambe*, Yi Li, Mike He, Gus Smith, Gu-Yeon Wei, Aarti Gupta, Sharad Malik, Zachary Tatlock

Workshop on Languages, Tools, and Techniques for Accelerator Design (LATTE'21) · 2021

Project Paper Poster