InfoQ - Language Workbench - ニュース https://www.infoq.com/jp InfoQ Language Workbench ニュース フィード DeepSeek社、数学定理証明向けLLM「Prover-V2」をオープンソースで公開 https://www.infoq.com/jp/news/2025/06/deepseek-prover-v2-formal-proof/?utm_campaign=infoq_content&utm_source=infoq&utm_medium=feed&utm_term=Language+Workbench-news <img src="https://www.infoq.com/styles/static/images/logo/logo_bigger.jpg"/><p>DeepSeek社は、Lean 4における数学定理証明に特化した新しいオープンソースの大規模言語モデルDeepSeek-Prover-V2を公開した。このモデルは、同社の基盤モデルであるDeepSeek-V3を活用した再帰的定理証明パイプラインを基盤として構築されている。Lean 4は、Microsoft Researchが開発した最新バージョンのLean定理証明ツールであり、機械による検証が可能な形式的証明を数学者やコンピュータ科学者が記述できる対話型証明支援システムである。</p> <i>By Vinod Goje</i> <i> Translated by Takashi Kawase</i> Language Workbench AIと機械学習、データエンジニアリング ニュース Thu, 12 Jun 2025 08:30:00 GMT https://www.infoq.com/jp/news/2025/06/deepseek-prover-v2-formal-proof/?utm_campaign=infoq_content&utm_source=infoq&utm_medium=feed&utm_term=Language+Workbench-news Vinod Goje 2025-06-12T08:30:00Z /news/2025/06/deepseek-prover-v2-formal-proof/ja