InfoQ ホームページ Theorem-Prover に関するすべてのコンテンツ
ニュース
RSSフィード-
DeepSeek社、数学定理証明向けLLM「Prover-V2」をオープンソースで公開
DeepSeek社は、Lean 4における数学定理証明に特化した新しいオープンソースの大規模言語モデルDeepSeek-Prover-V2を公開した。このモデルは、同社の基盤モデルであるDeepSeek-V3を活用した再帰的定理証明パイプラインを基盤として構築されている。Lean 4は、Microsoft Researchが開発した最新バージョンのLean定理証明ツールであり、機械による検証が可能な形式的証明を数学者やコンピュータ科学者が記述できる対話型証明支援システムである。
-
Idrisが間もなくバージョン1.0に
依存型(dependent type)ベース言語のIdrisが間もなくバージョン0.99に到達する。Idrisチームによると，1.00のアルファ版として見ることができるものだ。Idris 1.0のリリースは2017年2月頃と予想される。
-
LINQ to Z3、世界最速の定理証明器
マイクロソフトリサーチは、Z3は、世界最速の定理証明器であると宣言した。Z3は、ほかのアプリケーションへの低レベルツールとして設計されており、単独では動作しない。定理証明器のホストは、 Spec#/Boogie、Pex、Yogi、Vigilante、SLAM、F7、SAGE、VS3、FORMULA、HAVOCを含む数多のプロジェクトで使用されている。Bart De Smet氏のLINQ to Z3を使えば、驚くほど簡単に使えるようになる。