
INI Innovators Speakers Series: Rahul Kumar Showcases Automated Reasoning at AWS
By Evan Lybrand
Media InquiriesAmazon Web Services (AWS) Senior Applied Science Manager Dr. Rahul Kumar headlined the first INI Innovators Speakers Series event this February. Traveling from Seattle, he spoke to a packed room of Carnegie Mellon University (CMU) students about how AWS has been investing in automated reasoning technology.
Automated reasoning is a field of study that utilizes logic and mathematics to guarantee the correct answer to a query. Where Large Language Models (LLMs) predict the best-guess response, they are often designed to come up with an answer even when the prompt does not provide enough context to be certain — leading to many reported hallucinations.
“That's where automated reasoning provides you the guardrails and the necessary theories allowing for the detection of hallucinations,” said Kumar. “In some cases, [automated reasoning] automatically fixes them for you.”
Representing AWS, Kumar is part of the INI’s Innovators program, through which industry, government and research organizations sponsor INI students for a semester-long project called Practicum. AWS is one of the first INI innovators, an expansion on the prior Practicum sponsorship that includes a range of benefits, including unlimited resume books, priority on Practicum projects and the opportunity to give a talk on the CMU campus.
For Kumar, this meant a chance to share the innovative work he’s doing with automated reasoning. “I’m using the opportunity to bring out the ideas of automated reasoning and how they can be used in the modern day to do things like neuro-symbolic Artificial Intelligence (AI), where we combine LLMs and automated reasoning.,” said Kumar. “I’m also using this opportunity to showcase what AWS is doing with automated reasoning, and how powerful the techniques are.”

Kumar (right) speaking with students at the INI Practicum Showcase
Kumar has been a project manager for a series of Practicum projects over the past two years, working with bicoastal students in the M.S. in Information Technology - Information Security (MSIT-IS) and M.S. in Mobile and IoT Engineering (MSMITE) at CMU in Silicon Valley (CMU-SV). Students work in teams to help Practicum sponsors test proofs of concept or advance open-source projects with real-world impact.
In 2024, he worked with INI students to verify the safety of the programming language Rust. “It’s a great story,” said Kumar. “I met an INI student in 2024 who was having an issue using one of our tools to do a proof for a piece of code. This student reached out to me, and we tried to work through a problem.
“Eventually, we successfully helped solve the problem, and I was highly impressed by the drive and passion she had. We ended up meeting for lunch, and she mentioned Practicum. I thought that was a great way for AWS and myself to engage with bright and talented students.”
The success of the initial AWS Practicum projects was enough for Kumar and AWS to return in 2025 and expand the scope of their projects. Verifying the Rust Standard Library is by no means an easy task,” said Kumar “However, I met these students who had never learned Rust and, within three weeks, were making proofs and doing hard math. It was very edifying to be a part of that.”
For the 2025 Practicum, AWS sponsored five total projects working on topics like techniques for property-based testing, automatic model-based testing and the new AWS initiative called Strata. The idea behind Strata is that verification of multiple languages can be done using multiple different techniques in the backend.
Beyond his role as a project manager and technical lead, Kumar is passionate about mentorship and shared advice for students. “Connecting with people is important — finding a strong mental and emotional connection with others who are like-minded,” said Kumar “It’s not always about finding the job; you never know who ends up becoming your next best friend. And if you find these connections, ideas grow out of them which can snowball into larger outcomes.”
