search

brando90 / coq-serapi-python

API for Coq using SerAPI
Other
0 stars 0 forks source link

AI agent/mathematician design discussion #7

Open brando90 opened 5 years ago

brando90 commented 5 years ago

Discussion for design decisions for the AI agent.

The 1st agent will be a simple RL agent (conv net) acting on embeddings of Coq Terms.

brando90 commented 5 years ago

@ejgallego is there any point in having the tactic simpl. be an action choice for the RL agent?

brando90 commented 5 years ago

@ejgallego I remember in some previous discussion you suggested some tactic(s) that could have the RL agent potentially loop a proof forever. Was it symmetry.? I forget which one it was but I thought it would be a good idea to try to give the agent some tactics it should learn to avoid repeating that cause this sort of problems.

ejgallego commented 5 years ago

@ejgallego is there any point in having the tactic simpl. be an action choice for the RL agent?

Oh indeed simpl is quite complicated and can make a later rewrite step for example succeed.

hat could have the RL agent potentially loop a proof forever. Was it symmetry.?

Yup, symmetry, and in general many rewrites, for example addnC n m : n + m = m + n, rewriting with this will loop forever.

I guess the most reasonable choice will be to limit the depth at first; the agent will quickly learn that rewriting twice with a tactic is not a good thing to do :D