LeanDojoは、言語モデルを用いて数学の定理を証明するためのオープンソースプラットフォームである。

自動定理証明（ATP）は、形式論理で定式化された定理の証明を生成するタスクである。これは形式数学に有用であり、リスクの高いアプリケーションの正しさと安全性を保証する形式検証をサポートする。

しかし、ATPは探索空間が広いため困難である。そのため、対話的定理証明（ITP）が代替手段として登場した。ITPでは、数学者が証明アシスタントと呼ばれるソフトウェア・ツールと対話しながら証明を生成する。

機械学習はこのプロセスを自動化し、定理証明の新しい道を開くことができる。

大規模言語モデルで定理証明を自動化できる

リーン（Lean）のような証明アシスタントと組み合わせた大規模な言語モデルは、このプロセスの候補である。

しかし、カリフォルニア工科大学、エヌヴィディア、マサチューセッツ工科大学、カリフォルニア大学サンタバーバラ校、カリフォルニア大学オースティン校の研究者チームによると、既存の手法は、独自のコードやデータ、高い計算要件のために、再現や進化が困難であるという。

これに対処するため、彼らは言語モデルを使用して数学的定理を証明するためのオープンソースプラットフォーム、LeanDojoを作成した。

LeanDojoとReProverがさらなる研究の扉を開く

LeanDojoは、学習ベースの定理証明のために、データ抽出と、広く使われている証明アシスタントのLeanとモデルとのプログラムによる相互作用という2つの主な機能を提供する。研究者らによると、LeanDojoはLeanと確実に相互作用できる最初のツールであり、これにより証明ミスが大幅に減少するはずである。

LeanDojoはまた、定理証明における重要なボトルネックである「前提の選択」にも対処している。研究チームはReProver（Retrieval-Augmented Prover）でこれを実証している。ReProverは言語モデルベースの証明ツールで、Leanの数学ライブラリから取得したいくつかの仮定に基づいて証明戦略を生成する。

同チームによると、ReProverは他のいくつかの手法を凌駕し、LeanDojoベンチマークと2つの既存のデータセット、MiniF2FとProofNetでかなりの割合の定理を証明したという。ReProverはLeanでまだ証明されていない定理を証明することもでき、Leanの既存の数学ライブラリを拡張する有用なツールとなっている。

2026年までに言語モデルが数学の共著者に？
チームはまた、LeanDojoで構築されたベンチマークをリリースしている。このベンチマークにはMathlibの97,000近くの定理が含まれており、ChatGPTのプラグインもある。

数学者のテレンス・タオは最近、外部ツールを使用した言語モデルが、2026年までに数学やその他の科学で信頼できる共同執筆者になると予測した。LeanDojoとReProverは、そのようなツールがどのようなものかを示し、現在、他の研究者に改善の基礎を提供している。

詳細はLeanDojoのウェブサイトをご覧ください。