Seeker's research tasks & brainstorming

[brando90]

here we will write tasks, brainstorming, discussions, questions, etc. for projects

---

Meeting 👍 Mondays 6-7 and Thursdays 5-6

---

Brando's availability

Monday 4-6pm (or even 7pm) Thursdays 5-6:30pm Fridays 4-5pm (or even 7pm) weekends by appointment.

---

Useful links:

https://sites.google.com/view/holist/home

[brando90]

task

• for Brando do make a summary of the meeting notes and start a discussion for how to solve the environment issues and identify the issues
• implement our first NN on the HOList data set. Goal: understand the data and use it appropriately. without bugs.
• Explore how to improve embeddings for theorems/formulas/terms/goals.

[brando90]

Brando Meeting notes with Sanmi 30/Oct/2019:

• number of classes for classification

  • structure in classification

• number examples

• number characters

• number tactics

• read about transformer, BERT

• try de bruij representation

• https://arxiv.org/abs/1901.00596

• start the discussion about extending to any TP

• start discussion on allow HOList be more usable for any researcher

• start discussion on extending HOList to handle terms

• HOList env working with RL, progress in that

[Seeker-YML]

10/30/2019 - Updated Plan after the meeting:

1. Report the problem complexity of Automated Theorem Proving on HOList Dataset (at least include the tactic number and sample number and also some other useful data like the proving node number);
2. (First Priority) Work on the HOL Light (TP) working environment (build the research iteration env for Supervised Learning and Reinforcement Learning);
3. Meet twice on Monday and Thursday for reporting and collaboration (Seeker and Brando);
4. Consider the Embedding Methods and appropriate Neural Nets Architecture for Theorem Proving task ... --- (why work well and whether others could be better)

"Add to your deliverables the above task on articulating about finding out why google things graph NNs are good for this problem in the gitissue please."

5. Consider de bruij representation;

For Seeker (before Friday evening):

1. Report the problem complexity (statistics) and more experiment settings and results;
2. Work on building the interaction with HOL Light and report the difficulty or anything important;
3. Try to find out the problems of previous experiments (refer the codes from Google);

[brando90]

meeting 4/nov/2019:

https://docs.google.com/document/d/1aPMiE7uZfs2ww_ZhubhZl9z_O21IukJcoWc73ygHxJI/edit

• env:
  • having docker HOList work on vision cluster
  • TODO: run some ML model to do proofs
• Goal: NN embeddings
  • measuring improvement: testing the embeddings is by checking its accuracy on the tactic prediction (TacPred)
  • baseline: RNN = 10%
  • Suggests:
    • run their any version of their best model and check its performance on TacPred
      • 1) TF and check their performance on (TacPred)
      • 2) our own implement in Pytroch
      • Q: why can’t we run their TF pretrained models? <- ask them or look around
  • Question: what token/char level should we use to create embeddings?
    • experiments:
      • 1) char based
      • 2) word based
    • summary: of what Google’s best model does
      • figure out what they do
  • Questions: Network arch?
    • GNN
    • bert/transformer

[brando90]

@Seeker-YML

Notes from Sanmi Meeting 7/Nov/2019:

• understanding the problem first

• to solve the problem

• multi-output

  • ranking
  • multi-output

• https://github.com/brando90/ML4TP/blob/master/review_data.pbtxt

• stats

  • check if there are multiple tactics for the same goal
  • data preprocessing -> instead of goal to tactic, predict all the tactic used at that goal
  • Q: figure out the why there is variation in goal->tactic

• Clarify Sanmi’s question

  • goal: get an intuition on how many tactics are
  • S_N = (X_i=Goal_i,Y_i=Set(Tactics)i)^N{i=1}
    • average size 1/N \sum_i Set(Tactics)_i
    • how many tactics can be applied to a goal
    • histogram of |Set(Tactics)_i|
  • Solution:
    • ranking
    • google multi-out ML, distribution prediction

• Seeker Deliverable

  • Wavenet + multi-output

[brando90]

• DeepSeeker10 10% = char level input + 2 layer GRU + 2 FC layers

Objective

• a) implement our own model for HOList

• i) Env has to work

  • Brando

• ii) the model has to be good on the proving Task

  • proving task ~ tactic prediction
  • Seeker

Deliverables

• 1) apply wavenet (for a ii) ) so that we can compare DeepSeeker10 with SeekerWavenet and their checkpoints

• 2) try to run their checkpoints on the tactic prediction

  • this is to have a good reference

• 3) clarify

  • the wavenet training procedure
    • clarify what the loss is
    • where ranking fits in

• 4) |Set(Tactics)_i|

  • to understand problem better

• Later (for improving model)

  • basic experiment about how to use the data

[Seeker-YML]

Notes of Brando on Jan 22/2020

• Goal - submit to NeurIPS 2020

  • deadline is 23 may
  • deadline is 16 may

• Brando

  • send DARTs paper for getting a feel of how ppl in AutoML are moving away from RL & evolutionary/genetic algs but more to end-to-end differentiable

• Seeker

  • keep going on reproducing HOList
  • try to use tf 2.x
  • think about loss function at the end of the system