measuring "distance" from proof completion from `sorry`

Stream: lean4

[Quinn]

ok i have a bit of a galaxy-brained question

Is there a quantification of "how close" a proof is to completion from information like the type of a sorry? if that doesn't make sense happy to try clarifying.

Context: typically program synthesis problems have a spectrum of "how correct" solutions are (like an image is a percentage of pixels correct), so i'm wondering how much of regular program synthesis practices can be ported to proof generation

[Damiano Testa]

If something along these lines were possible in general, it would seem really close to giving an algorithm to prove anything.

However, any minimally complicated theory is undecidable.

So I am very skeptical that for a general theorem about the natural numbers such a distance can be computed systematically.

[Edward van de Meent]

indeed, such a quantification would give you a way to predict what direction a proof should move in to finish. you'd be able to do a kind of A* search through proofs. i suppose that would mean that if such a quantification existed (and were computable), it would probably either be not distinguishing enough to be useful (so you're basically still brute-forcing), or it would get stuck on some problems (i.e. the distance cannot be lowered from certain proof states, despite there being a route.)

[Edward van de Meent]

or it somehow gets stuck in an infinite descending chain which never reaches the actual goal

[Kim Morrison]

Theoretical objections based on decidability have nothing to do with the probable existence (and near term availability!) of extremely useful implementations of such a function. :-)

Realistically such a function is likely to either be an explicit component of, or extractable from, any system like AlphaProof that generates and tries to solve its own problems or variations. Training an approximation to "how provable does this goal look?" that is better than just "I can prove this, and disprove that, but everything else :woman_shrugging:" seems pretty useful!

[Jason Gross]

Define C(T) for a type T to be 0 if T cannot be proven and otherwise to be the sum over all proofs p : T of 2^-(length [in binary] of the trace of type checking p : T). C is not computable but it can be (expensively) approximated (upper-bounded) by enumerating all type checking traces. Then 1/C (or -C) is a measure of how close a proof is to completion.

(This is the brute force approach, but presumably whatever we'd extract from AlphaProof would approximate this)

[Edward van de Meent]

This specific measure quite possibly is infinite for all provable statements...

[Edward van de Meent]

In the sense that A: each provable statement can have an infinite number of proofs, and B: there are countably many provable statements. From this we can create an encoding where proofs of length $a2^{i}$ (with $a$ and $2$ coprime) are only those proving the $i$-th provable statement (ordering by length, then lexicographically).

[Edward van de Meent]

I suppose that in this sense, "how provable" really does only mean "is it provable"

[Damiano Testa]

Ok, I misunderstood the context. In fact, some tactics introduce implicitly or explicitly an approximation to such measure and work towards diminishing its value. For instance, this measure might the length of the target expression or the number of - symbols.

[llllvvuu]

An early work that attempts to do this is Polu et al 2022 "We depart from Polu & Sutskever (2020) and use a proofsize objective" (as opposed to presumably a success probability objective)

[Quinn]

Realistically such a function is likely to either be an explicit component of, or extractable from, any system like AlphaProof that generates and tries to solve its own problems or variations.

extractable only assuming language model interpretability goes really well, but indeed!

[Quinn]

thanks for the thought provoking responses!