生成式AI的功劳

解几何题经常需要引入辅助线、辅助点。这就是大语言模型所擅长的。

For example, if you want to prove something about a triangle, it is sometimes necessary to introduce new points and lines that were not mentioned in the problem. It is precisely this introduction of new auxiliary objects (the points and lines) needed to approach a proof that an LLM similar to GPT-4 is well suited to take on.

回溯法演绎不动了，AI引入新的点和线

But the LLM does not learn the deductive steps to finding a solution, which is work that is still done by specialized deductive algorithms. The AI model instead concentrates on finding points, lines and other useful auxiliary objects.

过程描述

If AlphaGeometry is given a problem, a deductive algorithm first derives various properties from what is described. If the statement to be proven is not included, the LLM auxiliary objects. Through intensive training, the AI can decide to add a fourth point X to a triangle ABC, for example, so that ABCX represents a parallelogram, something that the program has learned from previous training. This gives the deductive algorithm new information that it can use to derive further properties of the geometric object. This can be repeated until the AI and the deductive program reach the desired conclusion.

训练数据是人工生成的

Trinh and his colleagues generated a dataset with more than 100 million problems and corresponding proofs.

参考

SciAm