gohan

The Gohan Project for AI mathematics

The project is about

• given a proof sketch of a math problem, fill the gaps to be acceptable by a formal theorem prover

• develop theory and practice of dedicated learning methods for these problems, built upon existing methods like large language models

• demonstrate the Husky programming language's superiority by showing the algorithms can be developed much faster in Husky

The project is not about

• solving IMO or research level mathematics

• using soley large language model for doing mathematics

• the foundations of mathematics

What is the importance of the problem for AI

Besides being a utility for mathematics, we would like to stress upon its important for AI.

Currently, the logical inference paradigm of nowadays AI is using large language models, as against rule-based expert systems, which is considered archaic nowadays.

However, we believe that the view is highly biased and reflects how narrow people understand AI.

The possible futures of logical inference are

• solely general-purpose LLM.

In this case, OpenAI would be the winner, open-source companies and Husky will lose.

• solely general-purpose LLM combined with special-purpose LLM

In this case, open-source companies will thrive, and OpenAI would likely find it hard to profit, and Husky will lose.

• solely general-purpose LLM combined with special-purpose LLM, but only as a bridge to domain specific solver, which will be augmented by learning as compared with traditional solver.

In this case, Husky wins by providing a much stronger learning framework than existing ones.

We believe in the last case will happen, for the following reasons:

• sole LLM, general-purpose or domain specific, is hardly efficient. The model is originally designed for handling natural language, which contains inherent difficulties like ambiguity, imprecise meaning, temporal logic that not necessarily trouble specific domains. And natural language handles daily common communication, is not good enough for professional stuffs.

• deep learning in general is not sample efficient. Deep learning is basically about function approximation. For any problem, the general pattern is to see the problem as a function, collect data for it, and then train. The simplicity is a feature, not a bug, and explains much of its current success. However, the simpility comes at the cost of training time. Costly training time is fine for many tasks, because a model typically needs to be trained once in scenarios like translation, easy daily text manipulation, simple code generation. However, for things like AI mathematics, it's believed by us that online learning is important for efficient exploration (another story to be explained somewhere else). By the very definition of online learning, training and inference happens at the same time. In other words, deep learning in its current form is not the best for such tasks.

So the project's true objective is to showcase the advantage of a next-generation AI methodology and influence the AI community.

Advantage of Husky

Husky is a complicated project, I've never explained it fully to anyone because it's complicated. However, let's focus on what advantages Husky can bring to the table.

The main advantages are

• efficient training. Husky have a super form of mixture of experts by design. Each expert is only trained on a small portion of relevant data. There might be thousands, even millions of them.
• efficient inference.
• debugging.

The above will be particularly useful for AI maths.

Nature of the Problems

Review of Status Quo

LLM

LLM currently suffers greatly from hallucinations and we believe it's not going to be trusted in any near future.

Lean

Lean is horrible to read.