Semantics-based program manipulation in the age of LLMs
summary
Panel records concrete experiments and workflows: VS Code + Copilot generates SystemVerilog that is iteratively checked and fixed against model checking counterexamples; LLMs help produce proofs that are then verified in dependent type checkers; student-run experiments show LLM-generated homework often reaches roughly A- quality; fuzzing comparisons sometimes find more bugs than LLMs; prototype tools perform type error localization and synthesis of specs, suggesting a pragmatic combo of stepwise refinement and verification rather than outright replacement.
AI-written summary · about
chapters (24)
- 0:00Introduction
- 3:14Semantics in neuro-symbolic AI
- 4:20LLMs' program limits
- 7:08LLMs with formal verification
- 11:48Branch and bound in LLMs
- 13:18Hallucinations vs randomness
- 16:58DSLs and LLM capabilities
- 20:11LLMs for logical specs
- 22:18LLMs learn structure best
- 24:42Formalizing prompt languages
- 26:34Semantics vs statistical learning
- 28:47DSLs for LLM integration
- 30:52Learning to ask the right questions with LLMs
- 32:37LLMs in stepwise proofs
- 34:47Democratizing code generation
- 37:35Program transformation with LLMs
- 38:16Reliability via verification
- 41:07LLMs in education
- 44:37Coding is dead long live coding
- 46:46Creativity over implementation
- 48:56Future of semantics techniques
- 50:03Extracting LLM explanations
- 51:48Explanations bridge users and LLMs
- 52:35Summary
related talks
22mTowards Verified Code Reasoning by LLMs
21mA Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
01h 01mDiscussion
38mNobody Pages the LLM: Engineering Rigour for Vibe Coding
40mSafe Coding with LLMs - Verifiable Scala Silver Bullet
01h 16mHow Will LLMs Change Haskell, Programming and Open Source?
26mLanguage Model Agents Enable Semi-Formal Programming
15mCurrent Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can Do Better