Reasoning about 'Reasoning about Reasoning' Semantics and Contextual Equivalence
summary
Formal semantics for a core PPL with continuous distributions, scoring, nested queries and general recursion defines mutually recursive semantics so small-step, evaluation and measure definitions refer to each other and the paper proves limits exist for the induced step-indexed measures. A step-indexed biorthogonal logical relations model yields a soundness theorem: logical relatedness implies contextual equivalence. Mechanization uses Coq mechanization. Equivalences include mutually recursive MDP and coordination encodings that are semantically equal yet show large practical differences in inference runtime and memoization.
AI-written summary · about
chapters (10)
- 0:00Introduction to PPLs
- 0:55Modeling agents with queries
- 2:14Markov decision processes
- 4:32Program equivalence
- 5:54Formalizing semantics
- 7:09Small-step operational logic
- 13:09Logical relations model
- 15:37Coordination game case study
- 18:55MDP and performance analysis
- 21:19Conclusion
related talks
49mSemantic Foundations for Probabilistic Programming
16mA Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning(…)
01h 02mOut-of-Distribution Generalization as Reasoning: Are LLMs Competitive?
36mEnhanced and Efficient Reasoning in Large Language Models
27mExploring the Mechanisms of LLM Reasoning Capabilities
43mQuantitative Algebraic Reasoning
13mFormalizing a First-order Differentiable Logic with MathComp
24mHigher order programming with probabilistic effects: A model of stochastic memo...