Calendar

Introduction to Software Verification

Oct 22
Introduction to software verification as search.

Readings:

  1. The Bitter Lesson
  2. Mathematical discoveries from program search with large language models (FunSearch)
  3. AlphaEvolve

Assignment

Download OpenEvolve and go through its tutorial.

Oct 29
The internals of an enumerative checker for Java. [slides]

Readings:

  1. The Spin Model Checker
  2. Model Checking for Programming Languages using Verisoft

Assignment

Download JMC and go through its tutorial.

Nov 5
Heuristics for enumerative search. Randomization.

Readings:

  1. Stochastic Local Search Algorithms: An Overview
Nov 12
Stochastic search continued. Estimation. Population-based approaches and evolutionary algorithms.

Readings:

  1. Estimating the efficiency of backtrack programs
  2. (Optional) Go with the winners
  3. (Optional) Stochastic enumeration
Nov 19
Symbolic search and SAT solving. How to verify assertions by a powerful agent?

Readings:

  1. SAT Solving
  2. SATLution
  3. (Optional) Quanta article
Nov 26
Autoformalization

Readings:

  1. Specifications: The missing link to making the development of LLM systems an engineering discipline
  2. Autoformalization with Large Language Models
  3. A Neurosymbolic Approach to Natural Language Formalization and Verification
Dec 3
No Class. Work on reading list.

Readings:

See below for the next weeks.

Dec 10
``AI Scientist’’: Search in scientific discovery

Readings

  1. AI-Scientist
  2. AI-Scientist 2
  3. Open ended scientific discovery via Bayesian surprise
Dec 17
AI for Systems Research

Readings

  1. Barbarians at the gate
  2. Metastable failures
Jan 07
AI for Math

Readings

  1. AlphaProof Blog Post
  2. AlphaProof paper
  3. Mathematical exploration and discovery at scale
Jan 14
Agents. Cooperation, equilibria.

Readings

  1. ADAS
  2. Program equilibria
  3. Agree to disagree
  4. Bayesian persuasion.
Jan 21
Multi-agent systems.

Readings

  1. Generative Agents: Interactive Simulacra of Human Behavior
  2. Towards a Science of Scaling Agent Systems
  3. Autogen: Enabling Next-Gen LLM Applications via Multi-Agent Conversation
Jan 28
Learning to discover at test time

Readings

  1. Learning to discover at test time
  2. [Optional] Measures as ends
  3. [Optional] Context Windoes
Feb 04
Student presentations
Feb 05
Student presentations