OpenAIが数学リポジトリを更新、新たな形式化と撤回を実施

OpenAIはGitHub上の公開数学リポジトリを更新し、6件の新しいLean形式化と19件の修正を追加するとともに、3件の特定の数学原稿を撤回しました。OpenAIの科学者であるDan Roberts氏によると、リポジトリの主要な結果の約42%が現在形式化されています。

撤回された数学原稿

OpenAIはコレクションから3件の原稿を正式に撤回しました。撤回された作品は、複雑な代数幾何学とホッジ理論に焦点を当てています：

• 分裂アーベル八次元多様体上のWeil類の代数的性
• K3曲面に対するKuga–Satake対応の代数的性
• K3曲面の積に対する有理ホッジ予想

同社は、新しい形式化が完了し、正誤表が特定されるにつれて、リポジトリは引き続き更新されると述べています。

方法論とモデルの使用

リポジトリ内の結果は、主に未公開の内部OpenAIモデルを使用して生成されました。このプロセスでは、モデルに約4,000の問題を提示し、各結果には平均3時間の「ChatGPT Pro思考計算」が必要でした。

OpenAIは、これら4,000の問題のうち約700件の結果を公開しています。このプロジェクトの目標は、数学的証明の正確性を検証するように設計された定理証明器およびプログラミング言語であるLeanを使用して、数学的結果の完全な形式化を目指すことです。

コミュニティの議論と技術的批判

この更新は、AI生成の証明と従来のピアレビューの交差点に関して、技術コミュニティと数学コミュニティ内で大きな議論を引き起こしています。

ソフトウェアエンジニアリングと数学的証明

観察者たちは、OpenAIが数学的証明をソフトウェアリリースと同様に扱い、バージョン管理と反復的な更新にGitHubを利用していると指摘しています。

「これは、ソフトウェアエンジニアリングの実践が数学と出会うときの様子です。'openai/math リリース1.3.42：論文139と140を撤回、論文47の符号エラーを修正、以前撤回した論文85を復元、論文101の議論をリファクタリング'。」

検証と信頼

撤回された論文が最初の公開前にLeanでチェックされたかどうかについて、進行中の議論があります。Leanは形式検証ツールであるため、Leanチェッカーを通過した証明は、形式化に関して数学的に正しいことが保証されます。撤回や「符号エラー」の存在は、初期の結果がLeanで完全に形式化されていなかったか、形式化が意図した数学的問題を正確に反映していなかったことを示唆しています。

研究ワークフローへの影響

一部の批評家は、AI生成の数学的主張の多量が研究コミュニティに「ジャマー」効果を生み出し、専門家が根本的なエラーを含む可能性のある「スロップ」を検証しようとするため、数学者の時間を無駄にする可能性があると主張しています。

「大規模な認知オフローディングであり、これがどこまで進むかによって、数学者の時間と注意の点で深く純負になる可能性があります。」

逆に、一部のユーザーは、撤回を公に記録する透明性を賞賛し、そのような公開性は従来の学術出版では稀であり、AI生成の研究に対するより良い監査証跡を提供すると指摘しています。