世界

コンピューターが主要な物理学の論文の欠陥を初めて発見

機械は数学的エラーを発見するのに役立ちますアラミーストックフォト 数学の定理の誤りを見つけるために作成されたコンピュータ言語が、広く引用されている物理学の論文の根本的な誤りを初めて発見した。この発見に関わった研究者は、この方法で分析した物理学論文はこれが初めてだと述べたが、懸念すべき疑問が生じた。「あと何本に間違いが含まれているのだろうか?」 数学者が証明が正しく、矛盾や論理的穴がないかを確認するために、形式化として知られるプロセスを使用して、専用のソフトウェアがますます使用されています。このアプローチは、望月新一によるABC予想の500ページにわたる膨大な証明など、専門家が何年も議論してきた数学の最も厄介な問題のいくつかに対する潜在的な解決策として提案されている。 現在、英国バース大学のジョセフ・トゥービー・スミスは、リーンと呼ばれる形式化言語を物理学の分野に向けました。彼は、2006 年に発表された 2 ヒッグス ダブレット モデル (2HDM) ポテンシャルの安定性に関する研究を形式化しようとしました。この研究は、それ以来、広く引用されてきましたが、定理を損なう誤りを誤って明らかにしてしまいました。 形式化された定理は、より複雑な定理を形式化するための構成要素として使用できます。トゥービースミス氏は、自分の仕事は、MathsLib と呼ばれる確立された数学用データベースをモデルとする、PhysLib と呼ばれる形式化された物理学研究のより大きなプロジェクトに論文を追加するための「チェックボックスの練習」であるはずだったと述べています。 「私たちは論文を反証するために現場に出ているのではありません。誰もが利用できる結果を構築するために現場に出ているのです」とトゥービースミス氏は言います。 このエラーは、元の作成者が、問題を安定的に解決するには特定の条件 C があれば十分であると述べているステートメントに関連しています。しかし、トゥービー・スミスは定式化の際に、安定した解を提供しない条件 C が存在することを示しました。 トゥービー・スミス氏は、誤りの発見は論文に劇的な影響を与えるが、それを基にしてそれを引用した下流の研究で問題が生じる可能性は低いと述べている。しかし現在、同氏は多くの物理学の論文に同様の間違いがあるのではないかと懸念しているが、問題がどれほど広範囲に及ぶかは定かではない。これは、新しい研究を発表する際に形式化が標準的な部分となる強力な根拠になると彼は考えています。 トゥービー・スミスによれば、物理学者は数学者ほど定理の明確な詳細を与えない傾向があるという。 「多くの物理学者はこれらの核心的な詳細に興味がないため、時々それらを見逃してしまい、そこでエラーが発生します」と彼は言います。 インペリアル・カレッジ・ロンドンのケビン・バザード氏は、形式化は数学に大きな影響を与えており、少なくとも理論物理学を同様に扱えない理由はない、と述べている。 「私たちはこのような数学を試みましたが、非常に興味深いことが分かりました」と彼は言います。 しかし、数学における形式化の本当の利点は、既存の形式化された定理の大規模なコーパスによってもたらされており、これにより人間の数学者がそれらの上に容易に構築できるようになり、新しい定理をより迅速に形式化するのに役立つ AI モデルをトレーニングできるようになりました。これらの AI モデルをトレーニングして数学を形式化するには時間がかかり、トレーニング データとして使用するには多くの具体例が必要でしたが、物理学ではまだ利用できない可能性があります。 「理想的には、100 万行の物理演算が必要ですが、それを実現するのは大変な作業かもしれません。最初は機械が物理演算をあまり得意としていない場合、最初は手作業が必要になりますが、最終的には機械が引き継いでくれると思います」とバザード氏は言います。 元の物理学論文の著者らは、米国からのコメント要請に応じなかった。 新しい科学者しかし、トゥービー・スミスは、自分の発見を彼らに伝え、彼らが同意するという確認を受け、正誤表が出版されるだろうと告げられたと述べている。 トピック: #コンピューターが主要な物理学の論文の欠陥を初めて発見