AWS Podcast #747: Unpacking Automated Reasoning: From Mathematical Logic to Practical AI Security
12 snips
Nov 24, 2025 
Byron Cook, Vice President and Distinguished Scientist at AWS, shares his deep expertise in automated reasoning and AI safety. He delves into how AWS utilizes these tools for software correctness and trust in AI. Byron discusses the shift from academic to user-friendly reasoning systems. He highlights real-world applications, like mortgage approvals, where complex rules become automated decisions. The conversation explores how combining formal logic with generative AI can reduce hallucinations in models and improve overall trustworthiness in AI solutions.
AI Snips
Chapters
Books
Transcript
Episode notes
Logic-Based Reasoning Scales For Correctness
- Automated reasoning maps programs and policies into mathematical logic so you can prove properties about them.
- This approach contrasts with statistical AI and remains crucial for correctness at large scale.
Three Drivers Sparked Adoption At Amazon
- Three trends enabled automated reasoning at Amazon: better solvers, services model, and cloud security demands.
- Those forces created a 'perfect storm' that drove real business adoption, Byron recalls.
Language Models Unlock Theorem Provers
- Theorem provers historically needed PhD experts, but language models trained on proofs can now run them.
- This fusion (neurosymbolic) greatly expands what automated reasoning can do in practice.
