internship at Oracle Labs

Stream: general

[Jeremy Avigad]

I just posted this message on the Lean-user mailing list:

Dear all,

I am sharing the following information from Jean-Baptiste Tristan:

---

My name is Jean-Baptiste Tristan, I am a researcher in the machine
learning research group at Oracle Labs, located in the Boston area. I
am looking for an intern who would be interested in doing work at the
intersection of learning theory and formal verification.

More specifically, we would attempt to formalize one or more
fundamental results from learning theory using the Coq proof
assistant. This would require formalizing concepts from probably
approximately correct learning. We would then attempt to prove one of
the key theorems in learning theory such as the one that links finite
VC dimensions with PAC learnability or the one on boosting that shows
that weak learners can be boosted into strong learners. Such work
would build the foundations toward accountable machine learning
algorithms where we can offer strong formal guarantees that a machine
learning algorithm is behaving as advertised.

I would really appreciate if you could share this short proposal with
your students, and I would be happy to answer more questions.

---

This could be a summer internship for a PhD student, but the terms are flexible. Jean-Baptiste tells me that he has been considering Coq in part because of the existence of the MLCert project (http://ace.cs.ohio.edu/~gstewart/mlcert.html), but he is open to considering alternatives, like Lean.

If you are interested, you can e-mail him directly:

Jean-Baptiste Tristan <JEAN.BAPTISTE.TRISTAN@oracle.com>

Best wishes,

Jeremy