Neuro-symbolic AI Ambition

[mostafatouny]

Hello,

The problem of alignment, safety, and trustworthy in machine learning had sparked the world, especially after the modern advancement of generative AI. Neuro-symbolic AI, which aims to combine the best of data-driven and symbolic proven models, started to gain recognition.

• For an accessible intro see Forbes article.
• NeSy research conference.
• Deepminds used Functional language Lean to train a RL model to solve mathematical problems to advance AI capabilities. See their blog post.
• Amazon started to adopt automated theorem provers. See their blog article.

Owl and OCaml are branded for pragmatic computing with safety. The Coq theorem prover is very matured. I believe the community here is more suited to tackle recent safety challenges in AI and neuro-symbolic hybrid systems.

Is anyone interested in that? Would you like to explore its potential with me as a subsidiary activity?

[jzstark]

@mostafatouny Thanks a lot for this very detailed introduction! This topic looks very exciting and fit well to the OCaml + Owl world. I myself has no background in formal theorem proving, but I have not doubt that there are many in the OCaml community. The only suggestion I can give for now is that, given the potential significant engineering effort required, you can start with some simple owl-based side project to demonstrate a proof of concept. I will then help to share it in the community, so that more talents can be attracted to have more discussion about how it can be improved.

[mostafatouny]

Thank you @jzstark for the generous support offering. I shall keep you updated.