Neuro-symbolic AI, as its name indicates, is an AI approach that combines the neural AI methods and symbolic AI methods. Nevertheless, how to combine these 2 methods is still under exploration. Henry Kautz in his AAAI 2020 Robert S. Engelmore Memorial Award Lecture pointed out that there are at least 5 categories.
Personally, I am particularly advocating one of it, the Neuro[Symbolic] one, meaning "the embedding of symbolic reasoning inside a neural engine, where symbolic reasoning is understood as 'deliberative, type 2 reasoning' as common." An example would be using ChatGPT uas a neural engine to understand the problem, decompose the problem into sub-tasks, call the symbolic tools to solve these sub-tasks, and finally ChatGPT synthesise the results.
The reason why I am fond of this approach is that it directly mimics how human brains work. Our biological brains are naturally neural engines, and we use our brains to understand the problem, decompose the problem into sub-tasks, call the symbolic tools to solve these sub-tasks, and finally synthesise the results. In fact, we are encouraged to adhere to this workflow as much as possible, rather than solving the problem end-to-end, as we believe that this can not only increase accuracy but also transparency (and thus explainability plus debuggability).
Today, the state-of-the-art neural engines are Large Language Models (LLMs), or its generalised, multimodal version, Fundation Models (FMs). Hence, I am keen to explore the idea of LLM[Sy] which understands and processes the problem using LLMs, and calls external symbolic tools when necessary.
The study of Tool-augmented LLMs is to address the hallucination problem of LLMs, by equipping them with versatile tools such as calculators, theorem provers, code interpreters, search engines, or even physical robots. This is exactly the foxus of LLMSy, which is to understand the problem and extract sub-problems that can be solved by symbolic tools.
- ChatGPT-plugins
- Toolformer: Language Models Can Teach Themselves to Use Tools
- TALM: Tool Augmented Language Models
- PAL: Program-aided Language Models
- Augmented Language Models: a Survey
In science, the process of putting the blur ideas down on paper in formal language is sometimes called formalisation, or more specifically, logic translatioin which translate a problem from natural language (as well as image or other information) into formal language, that is, logic and math. The branch of AI research targetting on this process is auto-formalisation. Here are some selected papers on this topic:
- A Promising Path Towards Autoformalization and General Artificial Intelligence
- Autoformalization with Large Language Models
- Draft, Sketch, and Prove
- Formal Specifications from Natural Language
- Baldur: Whole-Proof Generation and Repair with Large Language Models
- Don't Trust: Verify--Grounding LLM Quantitative Reasoning with Autoformalization
The above papers focus on a particular domain: converting informal math into formal math, and thus proving theorems automatically. More related resources are in Tutorial on Machine Learning for Theorem Proving @ NeurIPS 2023. A natural generalisation of formalise math/proofs is to formalise scientific theories apart from abstract math, but also organic chemistry, genetics, behavoural modelling, etc. Math and proofs can be Represented by math formulas or theorem proving language, such as Lean, Coq, and Isabelle.
Similarly, scientific theories can be represented by modelling languages (PDDL for planning) or even general-purpose programming languages (Python or Javascript). The studies on how to do this is called program synthesis, or more fashinably, (AI) code generation.
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent