Hello,
This is related to my previous posts: Business models motivating active development in OCaml and OCaml projects utilizing Category theory.
A recently curated list, Deep Learning for Theorem Proving, surveys works for using learning-driven models for theorem proving. Notably Coq, based on OCaml, was used. Formal modeling with provable guarantees for Reinforcement Learning is witnessed as in RL: Foundations introductory course.
Unlike Julia and Python, OCaml has a competitive edge by design, when it comes to provable guarantees and theorem proving.
Is there any industrial OCaml project, which well-utilizes OCaml’s strengths, in the recent progress of machine learning with provable guarantees?
1 Like
This is not directly related to Coq, but related to automatic proving. Imandra is doing the kind of thing you’re asking for. Maybe @c-cube (who is working at Imandra) can give you some answers on how they articulate the two techniques (stochastic IA and formal reasoning).
2 Likes
Yes please. “AI reasoners powered by mathematical logic” sounds like an oxymoron to me .
(Although, I hereby nominate “neurosymbolic AI” for the silliness Oscars. Maybe “Stupidest Marketing Slogan”?
Why is it an oxymoron? For sure, the principles behind stochastic IA are not grounded in deductive logic. Maybe they can (by this I mean perhaps) be useful to find proves (so in the context of automatic proving). Consider the question : give me me argumentative P and a theorem T, then is P a proof of T ? This question can be answered finitely with a computer, a program that answers this question is called a type checker. If we only have a theorem T, the question to find Pthat proves T leads to the halting problem. But if we restrict the kind of questions, and we don’t mind the argumentation (we are only interested in the the truth of T and not why it is true), LLM may be of interest to explore the solution space. I will not claim it is the case, but I won"t claim the opposite either without strong evidences. 
I like that idea. At least, Imandra could participate in Type Theory forall podcast. I recommend the OCaml Foundation to sponser and support, if Imandra has any aspired open-source contribution.
This area deserves more attention by our community.