Reading
Here are some suggestions for reading this semester. Some of these papers should naturally be consumed together, e.g. similarly-themed papers with less technical content.
You’re welcome to suggest other papers for presentation. Whether you choose from this list or not, please confirm your choice with me.
Auto-formalization
- Guardians of the Agents
- SatLM: Satisfiability-Aided Language Models Using Declarative Prompting
- From Word Models to World Models
- Clover: Closed-Loop Verifiable Code Generation
- Autoformalization with Large Language Models
AI-driven verified software
- CLEVER: A Curated Benchmark for Formally Verified Code Generation
- dafny-annotator: AI-Assisted Verification of Dafny Programs
- Axon Verified Compiler
- Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler
Agentic programming and verification
- Guardians of the Agents
- Securing Agents with Tracked Capabilities
- Language-based Agent Control (Draft)
- ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models
- Statically Contextualizing Large Language Models with Typed Holes
AI discovery
- Advancing Mathematics with AI-Driven Formal Proof Search
- Draft, sketch, and prove: guiding formal theorem provers with informal proofs
- Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2
- Mathematical discoveries from program search with large language models
- AlphaEvolve: A coding agent for scientific and algorithmic discovery
- Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs
- Olympiad-level formal mathematical reasoning with reinforcement learning
- Learning Formal Mathematics From Intrinsic Motivation
- Why am and eurisko appear to work
- Automated conjecturing I: Fajtlowicz’s Dalmatian heuristic revisited
Self-improvement, autonomy, self modeling, reasoning about agents
- Gödel Machine: self-referential universal problem solvers making provably optimal self-improvements
- Darwin Gödel Machine: open-ended evolution of self-improving agents
- Self-Taught Optimizer (STOP): Recursively Self-Improving Code Generation
- SKILLAXE: Sharpening LLM-Authored Agent Skills Through Evaluation-Guided Self-Refinement
- Conniving With Continuations: Representing Goals in a Domain-Specific Language of Thought
- Gauguin, Descartes, Bayes: A Diurnal Golem’s Brain
- A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (Or: A Memo on memo)
Realizability of synthesis problems
- Languages with decidable learning: a meta-theorem
- Learning formulas in finite variable logics
- Synthesizing DSLs for Few-Shot Learning
- Unrealizability Logic
- Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
Abstraction and reasoning
- On the Measure of Intelligence
- Combining Induction and Transduction for Abstract Reasoning
- The ConceptARC Benchmark: Evaluating Understanding and Generalization in the ARC Domain
- RLSF: Fine-tuning LLMs via Symbolic Feedback
- Embers of autoregression show how large language models are shaped by the problem they are trained to solve
Symbolic learning & language learning
- DreamCoder: bootstrapping inductive program synthesis with wake-sleep library learning
- Top-Down Synthesis for Library Learning
- babble: Learning Better Abstractions with E-Graphs and Anti-unification
- Finding structure in logographic writing with library learning
- LILO: Learning Interpretable Libraries by Compressing and Documenting Code
- Playing ZendoWorld: Challenging AI Agents on Active Visual Concept Induction
- Programmatic Representation Learning with Language Models
- Languages with decidable learning: a meta-theorem
- Learning formulas in finite variable logics
- Synthesizing DSLs for Few-Shot Learning
- Learning-based Axiom Synthesis
Logic and neural networks
- What Do Hebbian Learners Learn? Reduction Axioms for Iterated Hebbian Learning
- DeepProbLog: Neural Probabilistic Logic Programming
Expressivity of neural networks
- What Formal Languages Can Transformers Express? A Survey
- The Expressive Capacity of State Space Models: A Formal Language Perspective
- The Illusion of State in State Space Models
- Thinking Like Transformers
Bonus theory
Some miscellaneous articles, notes, and repos of some relevance to our discussions.
Creativity
- Why A.I. Isn’t Going to Make Art
- Human versus artificial creativity: A case study in poetry
- AI Translates Pushkin
- Evaluating In Silico Creativity: An Expert Review of AI Chess Compositions