{"podcast":{"title":"Gradient Dissent: Conversations on AI","slug":"gradient-dissent","podcast_index_feed_id":1020509,"rss_url":"https://feeds.captivate.fm/gradient-dissent/","website_url":"https://wandb.ai/site/resources/podcast","image_url":"https://artwork.captivate.fm/25fd1181-b46e-459b-85a5-d397eec4cdcf/JDLDW81K-wlJoAWL7ZnxLdTp.jpg","author":"Lukas Biewald","episode_count":136,"summary":"Join Lukas Biewald on Gradient Dissent, an AI-focused podcast brought to you by Weights & Biases. Dive into fascinating conversations with industry giants from NVIDIA, Meta, Google, Lyft, OpenAI, and more. Explore the cutting-edge of AI and learn the intricacies of bringing models into production.","last_synced_at":null,"page_url":"https://stenobird.com/podcast/gradient-dissent"},"episode":{"title":"The $64M Bet on an AI That Has to Be Right | Carina Hong, CEO of Axiom","slug":"the-64m-bet-on-an-ai-that-has-to-be-right-carina-hong-ceo-of-axiom","published_at":"2026-02-05T10:46:00+00:00","page_url":"https://stenobird.com/podcast/gradient-dissent/the-64m-bet-on-an-ai-that-has-to-be-right-carina-hong-ceo-of-axiom","show_page_url":"https://stenobird.com/podcast/gradient-dissent","url":"https://wandb.ai/site/resources/podcast","audio_url":"https://episodes.captivate.fm/episode/d8dca4ed-165a-4b82-8e9e-3634835493aa.mp3","summary":"Axiom is building a self-improving reasoning engine that uses formal languages like Lean to bridge the gap between probabilistic AI and deterministic verification. The company aims to automate the tedious manual labor of formal mathematics, hardware, and software verification.","meta_description":"Learn how Axiom uses AI to automate formal verification in math, software, and hardware to solve the bottleneck of high-stakes system reliability.","key_points":["Main idea: Axiom combines generative AI with formal verification to create a self-improving reasoning engine","Practical takeaway: Automating formalization can drastically reduce the years of human effort required for hardware and software verification","Failure mode: Relying solely on probabilistic models for high-stakes systems without a deterministic verification layer leads to unreliability","Market opportunity: The 'verification lag' in hardware and software design presents a massive opening for automated reasoning tools","Core philosophy: Maintaining an 'underdog mindset' and the hunger of a startup is essential for tackling complex, established scientific domains"],"chapters":[{"start_ms":60000,"title":"The Mission of Axiom","summary":"Introduction to Axiom's goal of building a reasoning engine that combines generation and verification using formal languages like Lean."},{"start_ms":510000,"title":"AI as a Diligent Grad Student","summary":"Discussing how AI can handle the low-level, tedious proofs while humans focus on high-level mathematical intuition."},{"start_ms":1180000,"title":"The Verification Bottleneck","summary":"Exploring how the massive gap between design speed and verification speed in hardware and software creates a critical industry need."},{"start_ms":1400000,"title":"Use Cases in Software and Databases","summary":"Applying automated reasoning to code review, legacy code equivalence, and ensuring consistency in distributed databases."},{"start_ms":2125000,"title":"Auto-formalization and Test Cases","summary":"The technical challenge of using input-output pairs to automatically formalize software specifications."},{"start_ms":2815000,"title":"The Intersection of Math and AI","summary":"Reflecting on the unique synergy between programming languages, mathematics, and machine learning research."},{"start_ms":3035000,"title":"The Underdog Mindset","summary":"Carina Hong discusses the importance of maintaining curiosity and the 'hunger' of a startup despite achieving major milestones."}],"topics":["Formal Verification","Artificial Intelligence","Mathematical Reasoning","Software Engineering","Lean Theorem Prover","Automated Reasoning","Machine Learning","Hardware Design"],"duration_seconds":3040,"processing_state":"processed","actions":[{"name":"request_transcript","method":"POST","url":"https://stenobird.com/v1/public/podcasts/gradient-dissent/episodes/the-64m-bet-on-an-ai-that-has-to-be-right-carina-hong-ceo-of-axiom/transcription-requests","description":"Idempotently request low-priority transcript generation for this episode."},{"name":"read_markdown","method":"GET","url":"https://stenobird.com/podcast/gradient-dissent/the-64m-bet-on-an-ai-that-has-to-be-right-carina-hong-ceo-of-axiom.md","description":"Read the agent-friendly Markdown representation of this episode resource."}]}}