OpenAIの数学原稿はどこまで確かめられた？ 719原稿と「形式化」の意味

OpenAIが10月6日に公開した数学研究の原稿について、The Vergeが研究者の反応を報じました。AIの可能性への期待とともに、大量の出力を人が検証する負担が論点になっています。新しい数学モデルの一般提供が始まったというニュースではありません。

「原稿が公開された」「一部の結果に計算機で確認できる証明がある」「数学的な意味まで人が理解した」は、それぞれ異なる段階です。

719原稿は、719の独立した新発見という意味ではない

OpenAIの公式一覧では、719の原稿を372のグループに整理しています。関連する主な結果、補足の議論、そこから導かれる結果、別の証明などが、同じグループに含まれます。

原稿数だけで、解決した問題や独立した発見の数を数えることはできません。公開物には検証の段階が異なるものがあり、OpenAI自身も、形式化されていない結果に問題が残る可能性を認めています。

Leanでの形式化は、何を確かめるのか

OpenAIは、証明を計算機で確認できる言語Leanによる形式化も公開しています。公式一覧の説明では、主要な結果の約42％が形式化されています。原稿全体の42％を人が精読済み、という数字ではありません。

形式化は、数学の主張や証明を厳密な形で書き、計算機で確認できるようにするものです。ただし、そこで書かれた主張が原稿で意図した内容に対応しているかは、別に確かめる必要があります。機械で確認できることと、説明を理解して研究に役立てられることは、つながりながらも同じではありません。

結果を共有し、理解を深めるために

OpenAIは、引用や説明の質を改善し、修正を履歴として残す方針を示しています。また、AIが生み出した結果を理解するための研究会などを支援するとしています。

AIによって研究の候補が増えたとき、その価値を数学の知識へつなぐには、証明を確認できること、他の研究者が意味を理解できること、誤りを直せることが必要です。今回の公開を読む際も、原稿の本数と、それぞれがどこまで確かめられたかを分けて見ることが大切です。