The Fundamentals Behind the Future of AI

There’s a pattern in technology. Revolutionary waves of innovation bring new and urgent languages, tools, and promises. Before AI it was big data, mobile computing, cloud computing, and the internet itself.

All of them relied on the same foundation: perform computations without making mistakes.

A recent talk by Byron Cook, vice president and distinguished scientist at Amazon, highlighted how the rise of neurosymbolic AI captures this broader tension in the field. Delivered as part of the Lecture Series in AI at Columbia’s Morningside campus on Apr. 17, Cook explored how emerging AI technologies appear to sit squarely within today’s hype cycle. Systems that combine machine learning with formal reasoning are increasingly positioned as the “next step” in AI. It’s easy to frame this as just another trend. But zoom out, and a different story appears.

Using Math to Eliminate Mistakes

Cook is an influential researcher in formal verification, a field that uses mathematics to develop and prove that systems are completely correct and free of errors. His work on automatic program termination proving — particularly the development of the Terminator prover — challenged long‑held assumptions in computer science. At Amazon, he founded the Automated Reasoning Group, which develops tools that provide provable security guarantees for Amazon Web Services (AWS). 

In his talk, Cook explained that since joining Amazon in 2015, he has seen how the rise of cloud computing has brought in customers with extremely high expectations around security. To meet those demands, his team created formal reasoning tools that don’t just test systems but mathematically prove they behave correctly. Because every AWS service depends on core components like networking, storage, virtualization, and cryptography, these proofs extend across the entire ecosystem. In effect, formal reasoning isn’t isolated to a single feature; “it underpins nearly every part of AWS, shaping how the platform ensures reliability and security at scale.”

“This is super important work for enterprise customers, and has added many zeros to the checks that companies are paying to AWS," said Cook. "And that's why AWS was pretty excited about this work.”

Scale Changes Tools, Not Fundamentals

More recently, this focus on correctness has extended into generative AI through what’s essentially auto-formalization. With tools like Automated Reasoning checks, natural language rules (from policies, regulations, or documentation) are automatically translated into formal logic and then verified against AI outputs. Instead of trusting that an AI response “sounds right,” the system checks it against encoded rules and can mathematically prove whether it is valid, incomplete, or incorrect. This shift is significant because it bridges the gap between messy natural language and precise computation, enabling organizations to scale correctness alongside computation. In other words, they aren’t just building smarter systems, “they’re building systems that can justify their answers with proof,” reinforcing the idea that in a world of changing tools, doing computation right still matters most.

And with agentic tools, there is a shift from AI as a passive assistant to AI as an active decision-maker. Instead of simply generating responses, these systems can take actions, like writing code, making API calls, or coordinating tasks across multiple tools. As agents become more capable, the risk isn’t just incorrect answers but incorrect actions. To address this, developers have begun layering formal reasoning systems, such as the policy language CEDAR, on top of agentic systems, defining rules for what an agent is allowed to do and verifying each action before it executes. In this model, machine learning generates possibilities, but logic enforces constraints. The result is a more trustworthy form of automation, one in which agents can move quickly and independently, but always within provable boundaries.

What This Means for Students

So, where does all of this leave students, especially those trying to figure out what to study in a field that seems to reinvent itself every year?

Cook’s advice is to “study the hard things, especially math and theory, because it lasts.” Programming languages will change. Frameworks will come and go. Even today’s most popular AI tools may look outdated in a few years (or months). But the underlying ideas—logic, computation, mathematical reasoning—don’t expire. As he put it, “The theory is invariant. The same principles people worked on centuries ago still shape the most advanced systems today.”

That doesn’t mean ignoring practical skills. In fact, Cook said the most effective approach is a combination of hands-on experience and deep theoretical understanding. Building things teaches you how systems break and how to fix them. Theory teaches you why they work in the first place and how to make them reliable. Together, they create a kind of flexibility that trends can’t take away. In a world full of shifting tools and hype cycles, that combination—rigor, curiosity, and range—is what endures.

“I would say that the pendulum swings on trends, and people shouldn't focus on what's hot this year. Really, it's the diversity of thought that is important,” said Cook.