Neel Somani
University of California, Berkeley | Class of 2019
B.A. Mathematics | B.A. Computer Science | B.S. Business Administration
Bio
Neel Somani is a machine learning researcher working on formal methods for neural systems and neural methods for formal reasoning, with broader interests in interpretability and large-scale computation. He graduated from UC Berkeley with a triple major in Mathematics, Computer Science, and Business Administration. His research has been recognized at top conferences such as USENIX Security and OOPSLA, where Duet received the ACM SIGPLAN Distinguished Paper Award.
Neel's work spans two long-running threads: formal methods, which his current research continues; and large-scale and distributed computation, spanning distributed ML at RISELab (2018–2019), grid optimization at Citadel (2020–2022), and verifiable execution at Eclipse Labs (2022–2025). He supports education through a personal scholarship program and has been recognized as an Accel Scholar, Phi Beta Kappa, and Harmonic Rising Mathematician Award recipient.
Research
Research Interests: Formal methods and verification. LLM interpretability. LLM-driven proof search and autoformalization. Large-scale and distributed computation.
Past: Privacy-preserving ML and applied cryptography.
Current Research
- GPT-Erdős | 2026 | LLM-Driven Proof Search and Autoformalization for Erdős Problems
Evaluated across all open Erdős problems. Proofs for Problems #397 and #281 verified by Terence Tao. Code - Symbolic Circuit Distillation | 2025 | Formal Equivalence Prover from Circuits to Programs
This project extracts a Python program from a weight-sparse LLM circuit and uses an SMT solver to prove bounded-domain equivalence between them. Code - VeriCUDA | 2025 | Formal Verifier for Rust CUDA Kernels
A tool that formally verifies safety properties of Rust-based CUDA kernels. Code
Publications & Preprints
- Verifiable Transformers | 2025–2026 | Independent Research
"Towards Verifiable Transformers: Solver-Checkable Circuit Explanations"
N Somani (sole author)
Preprint, arXiv:2605.24033, 2026 | Code - PrivGuard | 2021–2022 | UC Berkeley, Prof. Dawn Song
"PrivGuard: Privacy Regulation Compliance Made Easier"
L Wang, U Khan, J Near, Q Pang, J Subramanian, N Somani, P Gao, et al.
31st USENIX Security Symposium, 2022 | NSF Award #1518899 - Data Capsule | 2019 | UC Berkeley, Prof. Dawn Song
"Data Capsule: A New Paradigm for Automatic Compliance with Data Privacy Regulations"
L Wang, JP Near, N Somani, P Gao, A Low, D Dao, D Song
Heterogeneous Data Management, Polystores, and Analytics for Healthcare, 2019 - Duet | 2018–2019 | UC Berkeley, Prof. Dawn Song
"Duet: An Expressive Higher-order Language and Linear Type System for Statically Enforcing Differential Privacy"
JP Near, D Darais, C Abuah, T Stevens, P Gaddamadugu, L Wang, N Somani, et al.
Proceedings of the ACM on Programming Languages (OOPSLA), 2019 | ACM SIGPLAN Distinguished Paper Award
Selected Honors and Awards
- Harmonic Rising Mathematician Award | 2026
- Phi Beta Kappa | 2019
- Magna Cum Laude | 2019
- Accel Scholar | 2017
- EECS Honors Program | 2017
- Upsilon Pi Epsilon | 2017
Teaching & Presentations
Teaching
- Head Lecturer | 2018–2019 | UC Berkeley, Prof. Thomas Lee
UGBA 198: Methods and Mathematical Foundations of Machine Learning for Business Decisions
Created and taught the first ML for business course at Haas with 200+ students per semester.
Managed team of 9 TAs and graders.
Selected Industry Talks
- From High Fees to High Speeds: Optimizing the SVM For Ethereum | 2024: YouTube
- Challenges & Advantages of Parallel VM Layer-2s | 2024: YouTube
- Design Trade-Offs for Persistent App-Specific Rollups | 2023: YouTube
YouTube Explainers
- Neel Somani Derives Mixture-of-Experts (Neural Architectures) | 2025: YouTube
- A First Principles Derivation of Transformer Attention | 2025: YouTube
Professional Activities
- Founder: Eclipse Labs (2022–2025) - Research on distributed execution & verifiable computation
- Quantitative Researcher: Citadel (2020–2022) - Large-scale electricity grid optimization
- Donor: Neel Somani Scholarship Program - Supporting education
- Board Member: Berkeley-Haas Alumni Network, San Francisco Chapter
Contact
- Email: ude.yelekreb@leen
- Website: neelsomani.com
- GitHub: neelsomani
- Blog: neelsomaniblog.com
- X/Twitter: @neelsomani
- Google Scholar: Publications