Why should we care about computer proofs?

• Computation has deep connections to mathematics
• Leveraging this, we can write proofs that are machine-checkable

Promising examples in math

We can also write proofs about computer programs as mathematical artifacts

Promising examples in software

• When AI writes paper proofs, there are trust issues
• But when it writes computer proofs, we can mechanistically check them
• Untrusted proof search + trusted verifier = ❤️

AI and Computer Proofs:

A Match Made in Heaven

There are many ways to marry AI and proofs

• In particular, not many LLMs!
• And not even all AI!

What does it mean to prove software correct?

1. Structuring Proofs

For the rest of this talk we'll cover three stages of proof writing that AI can assist

2. Synthesizing Steps

3. Searching for QED

Proof

Specification

Proof

Specification

Like other proofs, computer proofs need decomposition

Proof

Specification

Like other proofs, computer proofs need decomposition

Helper Lemmas Are Everywhere

Program

Specification

[1] Sivaraman, Aishwarya, Alex, Sanchez-Stern, Bretton, Chen, Sorin, Lerner, and Millstein Todd. "Data-Driven Lemma Synthesis for Interactive Proofs." . In Object-Oriented Programming, Systems, Languages & Applications. ACM SIGPLAN, 2022

Lemma Synthesis - LFind

LFind

Stuck Goal

rev

=

a :: x

(

rev x

++

(a :: nil)

)

Stuck Goal

=

.....

rev

(

.....

y

++

.....

z

)

rev

=

a :: x

(

rev x

++

(a :: nil)

)

Stuck Goal

=

.....

rev

(

.....

y

++

.....

z

rev

=

a :: x

(

rev x

++

(a :: nil)

)

)

.....

rev

(

.....

y

++

.....

z

)

=

(rev z) ++ (rev y)

Stuck Goal

=

.....

rev

(

.....

y

++

.....

z

)

(rev z) ++ (rev y)

.....

rev

(

.....

y

++

.....

z

)

=

.....

rev

(

.....

y

++

.....

z

)

=

(rev z) ++ (rev y)

rev

a :: x

(

rev x

++

(a :: nil)

)

=

Candidate

Lemmas

Stuck Goal

1.

rev (y ++ z)

= (rev z) ++ (rev y)

1.

2.

3.

rev

a :: x

(

rev x

++

(a :: nil)

)

=

.....

rev

(

.....

y

++

.....

z

)

=

.....

rev

(

.....

y

++

.....

z

)

=

(rev z) ++ (rev y)

(rev z) ++ (rev y)

.....

rev

(

.....

y

++

.....

z

)

=

1. Structuring Proofs

2. Synthesizing Steps

3. Searching for QED

?

1.23

2.34

3.45

4.56

1.23

2.34

3.45

4.56

forall (n: nat), (S n) > n.

induction n.

forall (n: nat), (S n) > n.

induction n.

Input (Proof Context)

Output (Proof Step)

forall (n: nat), (S n) > n.

induction n.

Input (Proof Context)

Output (Proof Step)

Command

Argument

forall (n: nat), (S n) > n.

induction n.

Input (Proof Context)

Output (Proof Step)

Command

Argument

Identifier Embeddings

induction n.

induction n.

1. Structuring Proofs

2. Synthesizing Steps

3. Searching for QED

90% prediction accuracy doesn’t mean much if you need to get 10 proof steps right.

Proof.

The Solution: Search!

Proof.

intros.

...

Unbounded Search Space

There are some techniques that can help us prune the search tree

It's hard to explore when you don't know where you are!

Easy

Medium

Hard

We can search more efficiently if we can evaluate proof states

Off-Policy vs On-Policy

1. Structuring Proofs

2. Synthesizing Steps

3. Searching for QED

Collaborators

Special Thanks

Emily First

Yousef Alhessi

Sorin Lerner

Zhanna Kaufman

Abhishek Varghese

Yuriy Brun

Talia Ringer

Timothy Zhou

Aishwarya Sivaraman

Todd Millstein

Bretton Chen

Ana Brendel

Machine-Checkable Proofs + Search + AI = ❤️

Rango

LFind