AI Hilbert: From Data and Background Knowledge to Automated Scientific Discovery

要約

自然現象を控えめに説明し、既存の背景理論と一致する科学的公式を発見することは、科学における重要な目標です。
歴史的に、科学者は既存の知識に基づいて方程式を操作し、新しい方程式を作成し、実験的に検証することによって自然法則を導き出してきました。
近年、データ駆動型の科学的発見が、大量の実験データを扱う環境において有力な競争相手として浮上しています。
残念ながら、データにノイズが多い場合やデータが不足している場合、データ駆動型の手法では有効な法則を発見できないことがよくあります。
したがって、最近の研究では、回帰と推論を組み合わせて、背景理論と矛盾する式を排除しています。
しかし、背景理論と一致する式の空間を探索して、データに最もよく適合する式を見つけるという問題は、十分に解決されていません。
私たちは、すべての公理と科学法則が多項式の等式と不等式によって表現できる場合に、この問題の解決策を提案し、私たちのアプローチが広く適用できると主張します。
さらに、バイナリ変数と論理制約を使用して最小限の複雑さの概念をモデル化し、混合整数線形最適化または半定値最適化によって多項式最適化問題を解決し、Positivestellensatz 証明書によって科学的発見の妥当性を自動的に証明します。
注目すべきことに、この論文で活用した最適化手法により、完全に正しい背景理論を使用した多項式時間、または部分的に正しい背景理論を使用した非決定的多項式 (NP) 時間でアプローチを実行できるようになります。
私たちは、ケプラーの惑星運動の第 3 法則、ハーゲン・ポアズイユ方程式、放射重力波力方程式などのいくつかの有名な科学法則が、部分的に正しい背景公理のセットから自動的に導出できることを実験的に示します。

要約(オリジナル)

The discovery of scientific formulae that parsimoniously explain natural phenomena and align with existing background theory is a key goal in science. Historically, scientists have derived natural laws by manipulating equations based on existing knowledge, forming new equations, and verifying them experimentally. In recent years, data-driven scientific discovery has emerged as a viable competitor in settings with large amounts of experimental data. Unfortunately, data-driven methods often fail to discover valid laws when data is noisy or scarce. Accordingly, recent works combine regression and reasoning to eliminate formulae inconsistent with background theory. However, the problem of searching over the space of formulae consistent with background theory to find one that fits the data best is not well solved. We propose a solution to this problem when all axioms and scientific laws are expressible via polynomial equalities and inequalities and argue that our approach is widely applicable. We further model notions of minimal complexity using binary variables and logical constraints, solve polynomial optimization problems via mixed-integer linear or semidefinite optimization, and automatically prove the validity of our scientific discoveries via Positivestellensatz certificates. Remarkably, the optimization techniques leveraged in this paper allow our approach to run in polynomial time with fully correct background theory, or non-deterministic polynomial (NP) time with partially correct background theory. We experimentally demonstrate that some famous scientific laws, including Kepler’s Third Law of Planetary Motion, the Hagen-Poiseuille Equation, and the Radiated Gravitational Wave Power equation, can be automatically derived from sets of partially correct background axioms.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google