Duper and Program Synthesis

Stream: general

[Jason Rute]

@Victor Maia posts a lot on X about program/proof synthesis. For a recent example: https://x.com/victortaelin/status/1872612589290790953?s=46

foo : Int -> [Int] -> [Int] -> [Int]
- foo 2 [1,0,1] [] == [0,1]
- foo 1 [1,0] [] == [1]
- foo 0 [1,0] [] == []
- foo 3 [0,1,1,0,1] [] == [1,1,0]

(Where there is no context besides definitions, so no functions like reverse or take in the context.)

Can Duper do this sort of thing (even if it can’t do this example)? I imagine stuff like this could be good for counter-example finding.

[Josh Clune]

No, Duper isn't a program synthesis tool, so this isn't the sort of problem it tries to solve.

[Jason Rute]

@Josh Clune Maybe it doesn’t work well, but in DTT, program synthesis and theorem proving are the same, right? You can just do it as an existence proof: exists f : Int -> (List Int) -> (List Int) -> (List Int), …, no? (And Victor seems to talk about this as “proof synthesis”, so I think he also has proofs in mind in his work too.)

[Frederick Pu]

but Duper is only supposed to do first order logic stuff and program synthesis is almost always monadic logic

[Josh Clune]

Jason Rute said:

Josh Clune Maybe it doesn’t work well, but in DTT, program synthesis and theorem proving are the same, right? You can just do it as an existence proof: exists f : Int -> (List Int) -> (List Int) -> (List Int), …, no? (And Victor seems to talk about this as “proof synthesis”, so I think he also has proofs in mind in his work too.)

Sort of. I agree that you could rephrase the problem in terms of an existential statement, and that the resulting problem would have an appropriate form for Duper. I suspect Duper wouldn't solve this problem in particular, but I could imagine Duper solving a simpler version of it.

More fundamentally, Duper's proofs are inherently classical, so even if you prove the existential statement, you wouldn't be able to extract a program out of the result (as you would theoretically be able to if the proof were constructive). So Duper just isn't really the right tool for program synthesis.

[Frederick Pu]

im pretty sure something like Plausible would be better for this if you phrase the problems as
\exists x : Int -> List Int -> List Int -> List Int, foo 2 [1, 0, 1] [] = [0, 1] \and foo 1 [1, 0] [] = 1 ... and then create some type class instances for showsing that if alpha, beta are testable then alpha -> beta is testable

[Henrik Böving]

feels rather unlikely that random exploration will find something like this

[Jeremy Avigad]

@Chase Norman Is this something that Canonical can do?

[Chase Norman]

@Jeremy Avigad This seems within scope, but to test I'd need a PBE mode where we can send definitional equality constraints to Canonical.

[Kim Morrison]

o1 solves this without any hints on the first try... :woman_shrugging:

[Jason Rute]

“First try” is a funny phrase for o1. The model probably tries lots of things in its hidden reasoning sequence but it only shows you the first thing that it could verify works. But yes, even Victor admits o1 can do this. I think his point is that his pure symbolic methods can also do it too.

[Jared green]

@Chase Norman how can i use Canonical?

[Notification Bot]

49 messages were moved from this topic to #general > Canonical by Patrick Massot.