Omar Muhammad | Personal Academic Website

About Me

I am an undergrad at IISc specializing in Mathematics annd Computing. I'm interested in Automated Reasoning, specifically looking at how we can leverage statistical learning to assist formal reasoning—and vice versa

I am interested in using neuro-symbolic approaches to solve "synthesis bottlenecks"—like generating loop invariants or library contracts—that currently limit fully automated program verification. I also work on Interactive Theorem Proving, exploring how 'Hammer' techniques and neural models can automate proof search.

Education

B.Tech in Mathematics and Computing

Indian Institute of Science, Bengaluru (2023-2027)

CGPA: 9.5/10.0

STD 12 (CBSE)

Saraswathi Vidyanikethan, Ernakulam (2022-2023)

98.4% | School Top

STD 10 (CBSE)

Rajagiri Public School, Ernakulam (2020-2021)

98%

Research & Experience

Enhancing Formal Verification with LLMs

Research Intern | University of Virginia, USA (Remote) | Aug 2025 – Present

Under the guidance of Prof. Wenxi Wang, developed ACPRO, a framework that uses a multi-agent LLM pipeline to transform low-level Z3 proofs into interpretable, high-level Verus verification steps. This work also produced the VSVerus dataset, a new resource for studying fine-grained LLM reasoning in formal verification.

Scaling Automated Verification with LLMs

Research Intern | IISc | UIUC | UW-Madison | May 2025 – July 2025

In a collaboration with Prof. D. D’Souza (IISc), Prof. M. Parthasarathy (UIUC), and Prof. A. Murali (UW-Madison), contributed to a framework for verifying programs by automatically synthesizing library contracts using LLMs and ICE-learning algorithms. Designed and built the core LLM pipeline responsible for generating specifications from logical rules and integrated it into a feedback loop with formal verifiers and testing engines to ensure correctness.

Formalization and Verified Implementation of Group Theoretic Algorithms

Summer Research Fellow | Krea University, Andhra Pradesh (Onsite) | May 2025 – July 2025

Collaborating with Dr. Rishi Vyas and Dr. T.V.H Prathamesh to formalize proofs for decision problems in geometric group theory (including the word, conjugacy, and subgroup membership problems) using the Lean 4 proof assistant. Key contributions include formalizing two definitions of the Dehn function and proving their equivalence and verifying the algorithm for the conjugacy problem in free groups. Current work focuses on the computability of the Dehn function for hyperbolic groups.

Intern | National Payments Corporation of India (NPCI)

Dec 2024 – June 2025

Working in a small team to develop an internal tool to enable NPCI employees to query databases and generate data visualizations via natural language prompts. Designing and implementing a pipeline that translates natural language queries to SQL queries, fetches data, determines correct visualization types, and renders visual output.

Intern | Applied Research Capability Network (ARC-Net), IISc Campus

July 2024 – Jan 2025

Fine-tuned LLMs with Tool Integrated reasoning for solving math and physics problems. Used proof assistants and symbolic solvers to verify the chain of thought of the models.

Other Projects

Image Denoising Algorithms

UMC203 Project, IISc | March 2025 - April 2025

Implemented and evaluated various frameworks for image restoration without clean data. Designed and conducted experiments to analyze the hyperparameter sensitivity of Zero-Shot Noise2Noise.

Rubik's Cube Solvability Conditions

Formalization Project | Feb 2025 - May 2025

Modeled the n x n x n Rubik's Cube as a group, formalized proof of validity of solvability conditions of the 4x4x4 cube and formulated the conditions for the n x n x n cube.

Robotic Arm Motion Planning

Lead at Vicharaka - IISc Robotics Team | Dec 2024 - March 2025

Responsible for motion planning for the rover's robotic arm using MoveIt2 and ROS 2 for the URC2025 competition.

Differential Topology and Knot Theory

Reading Project | May 2024 - July 2024

Explored topics under the guidance of Professor Subhojoy Gupta, Department of Mathematics, Indian Institute of Science.

Automated Refute Problem Generation

Developer at DataBased (CS club at IISc) | Oct 2023 – Dec 2023

Utilized Generative AI to develop components for an automated Refute Problem Generation system.

Curriculum Vitae

Download CV

Blog

This section is under construction. Please check back later for articles and updates.

Blog

This section is under construction. Please check back later for articles and updates.