Mistral AI、形式証明モデル「Leanstral 1.5」を発表

Mistral AIは、Lean言語を用いた形式証明の生成に特化したモデル「Leanstral 1.5」を発表した。詳細な技術仕様は公式ブログで公開されている。

Leanstral 1.5とは

Leanは数学の定理証明を厳密に記述・検証できる形式言語および証明支援システムで、近年AIによる自動証明生成の研究対象として注目を集めている。Leanstral 1.5は、この分野に向けてMistral AIが開発したモデルであり、名称が示す通り「Lean」と「Mistral」を組み合わせた製品と考えられる。

自然言語による推論とは異なり、形式証明は論理的な誤りを許さない厳密な検証が可能なため、AIモデルの推論能力を客観的に評価・向上させる手段として重要視されている。

数学的推論AIへの流れ

近年、大規模言語モデルの分野では、単に自然言語で説明を生成するだけでなく、Leanのような形式証明系を用いて数学的命題を厳密に証明する能力が注目されている。これは、国際数学オリンピック（IMO）レベルの問題を形式的に解く試みなど、AIの推論能力を測る新たな指標としても活用されている。

Mistral AIによる今回の発表は、同社が汎用的な対話モデルだけでなく、数学・論理推論に特化した専門モデルの開発にも力を入れていることを示すものといえる。今後、Leanstral 1.5が数学研究や教育、形式検証の分野でどのように活用されるか注目される。