LLM で数学オリンピックや競技プログラミングの問題が解けたというやつ、なんというか、どれくらい驚いていいのか分からないところがある。もはや重要なポイントではないかもしれないと思いつつも、やはり訓練データにどの程度の類似問題があったかは気になるし。
まあしかし、自然言語の文法が学習できている時点で形式論理の学習と演繹が行えるのは確実であり、また非常に複雑な確率分布を学習・生成するのも DNN の得意とするところである。つまり論理の通った、ありがちな式変形を出力できる能力がある。それに生成時の探索的な仕組みが入れば、圧倒的な物量で非自明な数学の定理も証明できるのでは、といわれると「たしかに…」と思う。それは凡人が小定理を証明するときに行っていることでもある (なお圧倒的な物量はない)。
旧来の定理自動証明器には「形式化が大変」と「探索空間が広すぎる」という問題があったわけだけれど、それを解決する要素を LLM はたしかに持っている。
そして最後に Transformer のアーキテクチャを思い返し、「こんなもので定理の証明ができてたまるか」という気持ちに戻る。