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
AI for Math
LLMs are making measurable advances in reasoning, with most new proofs coming from informal prose. Formal methods offer an avenue for benchmarking reasoning and objectively evaluating proofs for correctness and higher-order properties.
- GPT-Erdős | 2026 | LLM-Driven Proof Search, Autoformalization, and Proof Novelty
Evaluated across all open Erdős problems. GPT 5.2-generated proof for #397 verified by Daniel Larsen and #281 endorsed by Terence Tao. Prior literature was later found, motivating PriorProof, which formalizes a definition of proof novelty. Code (GPT-Erdos) | Code (PriorProof) | Talk - AutomataBench | 2026 | Reasoning Benchmark for Reversible Cellular Automata
A benchmark to test whether LLMs can deduce the hidden initial state of a reversible Margolus block cellular automaton from partial observations; uniqueness enforced via a CSP solver. Website | Code
Verifiable Neural Systems
Interpretability work often involves plausible explanations and heuristics for safety, but formal verification can make these claims provable.
- 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. It forms part of a broader line of work on solver-checkable neural systems, continued in Verifiable Transformers below & covered in its talk. Code - VeriCUDA | 2025 | Formal Verifier for Rust CUDA Kernels
A pipeline that translates Rust GPU code into formal Coq models with executable semantics, as a foundation for memory model proofs. Code
Selected 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 | Independent Verification (Lean) | Talk - 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 Talks
- PriorProof: A Point-in-Time Measure of Technique Novelty for Formal Proofs | 2026: YouTube
- Towards Verifiable Transformers: Solver-Checkable Circuit Explanations | 2026: YouTube
- Challenges & Advantages of Parallel VM Layer-2s | 2024: YouTube
Explainers
- Power 2026 - Electricity Pricing in the Age of AI | 2026: Essay
- Deriving Mixture-of-Experts | 2025: YouTube
- Deriving 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, San Ramon Valley Education Foundation - 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