universal oracle

Stream: Machine Learning for Theorem Proving

[Daniel Selsam]

FYI @Jesse Michael Han @Leonardo de Moura @Patrice Godefroid and I just posted a preprint on a new way to leverage ML for theorem proving: https://arxiv.org/abs/2012.11401 We are planning to build something like this into Lean4, but there are still many open design questions. Feedback very welcome.

[Kevin Lacker]

it looks pretty neat... what data can the choose operator look at when it's making its decision?

[Jason Rute]

Thanks! Are you by chance talking about this at Lean Together?

[Jason Rute]

Actually, I should have just looked at the schedule. I think the answer is no.

[Daniel Selsam]

Kevin Lacker said:

it looks pretty neat... what data can the choose operator look at when it's making its decision?

This is discussed in sections 2 and 3 for the prototype language in the paper. For Lean it would be the same information but would probably be represented as bytecode.

[Daniel Selsam]

Jason Rute said:

Thanks! Are you by chance talking about this at Lean Together?

I was not planning to. The preprint does not even mention Lean -- there is still a long way to go to manifest the idea in a practical way in Lean.

[Jason Rute]

@Daniel Selsam I assume this a continuation of the project you talked about at AITP2020 and that @Jesse Michael Han blogged about?

[Daniel Selsam]

Yes, this paper presents a crystallization of the search transformer + universal oracle idea, stripped to its essence.

[Johan Commelin]

@Daniel Selsam Congrats! This looks cool!

[Johan Commelin]

The main function is step, which dispatches to helper functions step-atom, step-if, step-quote, step-lambda, step-app

Is step-choicepoint missing from that list?

[Daniel Selsam]

Johan Commelin said:

The main function is step, which dispatches to helper functions step-atom, step-if, step-quote, step-lambda, step-app

Is step-choicepoint missing from that list?

Good catch, thank you. I just fixed it locally but will buffer revisions before posting to arXiv.

[Johan Commelin]

so rather than belabor the low-level details we highlight a few decision decisions and then summarize the process.

decision decisions -- doesn't seem what you want, right?

[Daniel Selsam]

Johan Commelin said:

so rather than belabor the low-level details we highlight a few decision decisions and then summarize the process.

decision decisions -- doesn't seem what you want, right?

thanks, fixed (should be 'design decisions')

[Johan Commelin]

Ultimately we envision an OGDP framework embedded in a general-purpose

/me is ignorant... what does "OGDP" stand for?

[Daniel Selsam]

ah whoops, never introduced it -- oracle-guided decision programming

[Johan Commelin]

ok, makes sense :smiley:

[Jason Rute]

I wrote a summary of this paper. I'm going to try something different and put it in a Github Gist. Let's keep the discussion here on Zulip.

[Daniel Selsam]

@Jason Rute Thank you very much for sharing.

[Daniel Selsam]

one still needs to design the network underlying Dodona’s universal policy, which the paper suggests is not at all fleshed out.

I wouldn't quite say that the network is not fleshed out, but rather that the details of the network are independent of the main ideas of the paper. Basically, you should use whatever model seems to work best at whatever time you are living in. Right now that means transformers. Since we weren't co-training on anything and the Dodona data has natural graph structure, we also chose to augment the standard transformer with the ability to attend to the edges of the graph, but this part is not necessary.

[Daniel Selsam]

I don’t think one should just work on building Dodona’s policy from scratch ... but instead work on gathering data for a large dataset of formal mathematics, which can include natural language, formal math, and other sources, in addition to Dodona MDP continuation data when that becomes available.

I agree completely. The key problem Dodona solves (at least in principle) is that it lets you build precise, neurally-embeddable specifications for any computable goal. A network may gain 99.99% of its knowledge from arbitrarily unstructured data, and yet it could still serve as a universal oracle for Dodona as long as it sees enough Dodona problems to infer how to interpret these specifications precisely.

[Daniel Selsam]

The rewriting tactics in Lean probably have a lot of code. Would all that code get passed to the Neural network as part of the continuation?

Dodona supports tagging functions as @[opaque], which means that the function should be embedded as its name rather than as its code. This feature could easily be made available in any Dodona descendent as well. However, big datastructures (as opposed to big programs) pose a serious problem. The Dodona embedder has access to runtime type information, and so a type may be marked as opaque and embedded by its name rather than as its data. But this may not be possible in other languages. For example, in the Lean4 runtime, every object is represented by a lean_object and there is no additional typing information. I prototyped a universal oracle for Lean4 and tried it on the tactic framework. The embeddings were astronomical, since the backtracking part of the tactic state includes the entire environment. Even after removing the environment from the backtracking tactic state, there was still quite a lot of waste, since the metavariable context was still getting embedded (which includes information about past goals that are not relevant to the current ones) and the embedding of every expression included all of its implicit arguments. Worse, there is no obvious recourse.

[Daniel Selsam]

Ultimately I view Dodona as a "Plato Pole"---a timeless extreme of the Platonic design space---that clarifies and inspires but that is likely to remain impractical in its extreme form. I think it is still very much an open problem how best to leverage ML for hard (IMO-level) mathematical problem solving. I wrote up a taxonomy of possibilities in a short idea paper for an upcoming ICLR workshop. My current thinking is to pre/co-train on everything, then rank choices in SearchT tactics based on a mix of explicit tactic-state snapshots and a (Dodona-style) view of the downstream code (but not the data). This is messy though and not worth speculating about until it comes time to try it.

[Johan Commelin]

@Jason Rute Thanks for writing the summary. :thumbs_up: Minor point: you wrote Dodana (both in title and main text), whereas it's Dodona...

[David Renshaw]

Dodona seems to have a lot of parallels with what I've previously heard called "symbolic execution", e.g. https://arxiv.org/pdf/2002.06311.pdf

[David Renshaw]

I suppose that a big difference is that symbolic execution algorithms typically try to defer actually making decisions at choice points, and instead try to maintain a set of symbolic constraints describing previous choices.

[David Renshaw]

If I understand correctly, Dodona proposes, in contrast, that we should just learn how to make really good choices.

[David Renshaw]

The supplementary material includes code for all tasks in the suite

Where can I find this supplementary material?

[Daniel Selsam]

David Renshaw said:

The supplementary material includes code for all tasks in the suite

Where can I find this supplementary material?

Click "Other Formats" on the arXiv page.

[Daniel Selsam]

David Renshaw said:

Dodona seems to have a lot of parallels with what I've previously heard called "symbolic execution", e.g. https://arxiv.org/pdf/2002.06311.pdf

Patrice Godefroid is a co-author on the universal oracle paper :)