Towards Verified Code Reasoning by LLMs
summary
Builds a pipeline that extracts an LLM’s code reasoning as predicates via an LLM-based formalizer, encodes code semantics and a verification condition in Souffle Datalog, and checks the agent’s claim with a verifier. Uses Gemini 2.5 Pro plus simple tools (cat, find) to produce relevant slices, targets minor local program equivalence on ~20–30 line examples, and on 20 program equivalence queries the verifier catches 6/8 incorrect agent judgments (conservative, misses some true equivalences).
AI-written summary · about
chapters (12)
- 0:00Verified code reasoning intro
- 1:06Program equivalence checks
- 3:12Formal verification of LLM claims
- 5:40Formal representation pipeline
- 8:51Code semantics with Datalog
- 10:41Benchmarking real-world code
- 12:49Results and false positives
- 15:41Limitations and future work
- 16:46Q&A: Conservative outputs
- 17:47Q&A: Scalability issues
- 19:13Q&A: Explanations and verifiers
- 20:18Q&A: Testing and alignment
related talks
53mSemantics-based program manipulation in the age of LLMs
21mA Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
15mCurrent Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can Do Better
33mLeveraging LLM Reasoning with Dual Horn Programs
19mLLM-Integrated Declarative Program Analysis
19mAutomated Program Refinement: Guide and Verify Code Large Language Model with(…)
31mBeyond LLMs and Maturing RAG use cases
01h 01mDiscussion