AITP invited talk

Stream: IMO-grand-challenge

[Daniel Selsam]

@channel FYI I will be giving an invited talk tomorrow at AITP 2020 on the IMO Grand Challenge. Among other things, I will be presenting a very preliminary but perhaps plausible technical roadmap. It will be live on Zoom at 3:00pm GMT (5:00pm Paris time) and there will be time for questions. They asked us not to post the Zoom link publicly, but if you are interested, message me and I can share it with you.

[Oliver Nash]

Cool! Will it be recorded and subsequently publicly available?

[Jason Rute]

In the past the slides and/or videos have been posted on the AITP website. Here is where they would be: http://aitp-conference.org/2020/

[Jason Rute]

Jesse Michael Han said:

For those of you who saw Dan's talk on the IMO Grand Challenge yesterday and would like to learn more, I have a blog post where I discuss the SearchT monad transformer, ARC, and our work on building an IMO geometry solver: https://jesse-michael-han.github.io/blog/imo-gc-geo/

Cross posting so this doesn't get lost.

[Daniel Selsam]

The talk is now available here: https://youtu.be/GtAo8wqWHHg

[Kevin Lacker]

you mention ~ 32 minutes in, if we can solve the IMO we could also have, start with some inefficient code, and do lots of optimizations to have code that does the same thing but with better performance. that's kind of what a modern compiler does, right? unrolling loops and so on. but this hopefully could be a lot more advanced, using weird data structures etc. very interesting talk...

[Miroslav Olšák]

This is all on the "dream level" but how I understand it, especially IMO combinatorics requires some algorithmic thinking. So if we could solve IMO, we are not so far away from solving analogous programming competitions as IOI, or ACM ICPC (by the way, I have attended both IMO and ACM ICPC).
So computer could just find the right efficient (verified) code given a mathematical problem description.
And one of such descriptions could simply be an unefficient code.

[Kevin Lacker]

it might be similar and more economically useful to say, here's some running code, is there any input it would crash on. or, here's a stack trace from a crash, please autowrite a pull request that fixes it. but yeah kind of "dream level"\

[Daniel Selsam]

@Kevin Lacker To clarify, I don't foresee a push-button makeReal :: HighLevelCode -> RealSystem function that takes some high-level code and produces a competitive web-scale production system automatically. I foresee an (extensible, programmable) interactive assistant---basically just an improved Lean---that can automate many subproblems arising in this process but that is nonetheless still driven by humans.

Here is a high-level sketch:

• In addition to factoring out choice points as in nondeterministic programming, also factor out every step that has a simple declarative representation, producing a program that is not only nondeterministic but also noncomputable. For example, instead of hardcoding a specific search algorithm, write in math that you want to sort the array. Instead of designing a fancy custom datastructure, write the API (with specs) you want the datastructure to satisfy. Instead of devising a clever algorithm that computes X in one pass, write a naive one that does it in three, or better yet, describe declaratively the thing you want to compute. In general, write the most abstract, declarative, simple version of the program you can that precisely captures your intent.

• Expose a high-level tactic language for refining the noncomputable program into the desired implementation. The tactics can encompass many kinds of tasks. Subproblems might be immediately formal ("synthesize a datastructure for this API" or "search for a concrete way to compute this value"). Or, they could be formalizable with respect to a mathematical cost model ("...with all operations quasilinear" or "...only visiting each element of some array once"). They could also involve optimization over learned cost models ("select a sorting algorithm here based on this learned cost model and this historical input data") or even define ongoing policies ("for this ADT, search for 3 candidate implementations with good asymptotics and train a classifier online to map inputs to the most appropriate candidate").

• Have standard tactics/strategies that can do pretty well in push-button mode.

Most of this could be done in current Lean with enough effort, it is just nowhere near cost effective yet for most use-cases.