OpenAIはアドバイザーの要請にもかかわらず、数学に関する独自モデルのテストを継続している

10月6日、OpenAIは未公開の内部モデルから719件の数学論文をGitHubにアップロードした。

その1週間前、同社の諮問グループは、プロプライエタリなモデルで高度な数学問題のテストを行うことを停止するよう各ラボに要請していた。

600件以上のアンケート回答が、IASパネルの9月29日付ガイダンス形成に寄与

数学と人工知能に関する諮問委員会は、ニュージャージー州プリンストンの高等研究所に本部を置いています。9月29日、同委員会は600件を超えるアンケート回答に基づいた提言を発表しました。

「最初から明確に述べておきます：私たちはこの慣行を支持するものではなく、独自モデルに対する高度な数学的問題のテストを中止するよう求めます」と同グループは記した。

同文書は、プライベートな内部モデルが、ラボが分野の他者を凌駕する二層構造を生み出すリスクがあると警告している。

OpenAIはリポジトリにおいて、モデル開発の一環としてオープンな研究課題で自社のモデルをテストしていると説明し、既存の数値ベンチマークが飽和した後にこれらのテストを拡大した。

OpenAIは同グループと協議し、リリースに際してその勧告を参考にした。10月6日に発表された声明で、同グループは助言者の役割は「OpenAIがそれらを入手したプロセスの承認ではない」と述べた。

同グループは適合性に関する判断を、より広範な数学コミュニティに委ねた。

Navier-StokesのLeanコードは、論文に記載されている主張よりも弱い主張しか証明していない

OpenAIは719本の論文を372の数学ファミリーにグループ分けしました。各ファミリーは主要な結果とその関連する証明を中心に構成されています。プロプライエタリモデルには約4,000の問題が与えられ、各結果の処理にはChatGPT Proの思考計算で平均約3時間かかりました。

グループは、AIラボに対し、各結果についてモデル名、プロンプト、要約された思考チェーン、所要時間、および計算コストを公開するよう求めました。

OpenAIは10件の推論サマリーを公開し、トップラインの結果の約42%にLeanによる形式化が含まれています。

Leanは、コンピュータによって証明を検証するために使用できるプログラミング言語です。コードがコンパイルされたからといって、コードと記述された議論が同一であるとは限りません。それは単に、形式化された命題が真であることを意味するだけです。

アレクサンダー・バストーニス、ファビアン・シルチェリ、アンダース・C・ハンセンは、10月6日に公開された論文においてこのギャップを検証しました。彼らは、OpenAIのNavier-Stokes方程式に関する論文が、そのLeanコードで証明されている内容よりも強い主張を行っていること、および入力微分の次数に関する推定値が変更されていることを発見しました。

著者らは、OpenAIのオイラーの証明でも同様の誤訳を検出しました。OpenAIの記述された証明や他の自動形式化されたLeanの証明は、「他の証明と同様のピアレビュープロセスと精査を経て初めて信頼に値する」と彼らは述べています。

Navier-Stokes方程式の結果は9月8日にOpenAIによって発表されました。Cryptopolitanによると、ニューヨーク大学の数学者トリスタン・バックマスターは、この研究に関与した最小限の人間の入力の記述に対して異議を唱えました。

同社は、主要なAI成果に関するワークショップ、カンファレンス、特別プログラムに対して資金を提供すると約束しました。

10月6日、テレンス・タオ氏は、AIのプロンプトエンジニアはしばしば問題を解決した後にその分野への関心を失うと指摘しました。多くの人は、その結果に関する質問に答えたり、講演を行ったりできないと彼は記しています。彼の投稿ではOpenAIの名前は明記されていませんでした。

同社は、アドバイザーが研究のペースについて決定権を持っていないと述べており、これは9月にCryptopolitanによって報じられました。