0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

@etale_cohomology(Etale Cohomology)

【Dedukti入門 ④】Dedukti に、産業実績はあるのか

0
Posted at

thumbnail_picture.jpg

この連載について

本記事は、Dedukti という言語を扱う連載シリーズの 4本目の記事です。
全体で何回まで続くかは決めていません。

回 扱うこと
初回 定理証明支援系が出力した証明項を、翻訳器が .dk ファイルに翻訳し、Dedukti が検査する仕組み
2 回目 Dedukti の言語そのもの。識別子の宣言と書き換え規則の 2 種類で、論理体系と型理論を記述する
3 回目 Logical Framework という考え方。Edinburgh LF、Twelf、Isabelle/Pure との関係
4 回目（本記事） Dedukti の実績と限界。年表、翻訳器、利用者、産業実績

初回から前回までの記事は以下のとおりです。

初回記事
【Dedukti入門 ①】Lean 4・Rocq・Isabelle が検証した証明を、もう一度別の証明検査器で検査する ── 翻訳器と符号化ファイルの仕組み

2回目の記事
【Dedukti入門 ②】Lean 4 の型理論も HOL Light の高階論理も、なぜ同じ言語で書けるのか ── Dedukti の言語 λΠ計算 modulo rewriting を、実物のコードで読む

3回目の記事
【Dedukti入門 ③】Logical Framework とは何か ── 1967 年の Automath から Isabelle、1987 年の Edinburgh LF、そして Dedukti へ

本記事について

初回記事では 翻訳器 と 符号化ファイル の仕組みを、2 回目では Dedukti の言語 を、3 回目では Logical Framework という考え方 を扱いました。

本記事では、実績と限界 を扱います。

Dedukti の研究は 1998 年から続いています。それにもかかわらず、産業界での実績を、筆者は公開資料の範囲では確認できませんでした。

何ができていて、何ができていないのかに、光を当てます。

初回から 3 回目までをまだお読みでなくても、この記事単独でお読みいただけるように努めました

専門用語は、初出の箇所で解説を入れさせていただきました。
また、記事末尾にも用語のミニ解説を置きました。

本記事の流れ

金色の枠が対話篇です。

なお、本文は、対話篇をすべて飛ばしても、上から下へ通して読めるように書いてあります。

対話篇 ① ── 検証済みの証明を、なぜもう一度検証するのか

タロウくん：
先生、この連載で、Dedukti について 3 つのことを教わりました。

  • Lean 4 や Rocq が出力した 証明項 を、翻訳器が .dk ファイルに翻訳 し、Dedukti が型検査する こと。
     
  • その .dk ファイルは、識別子の宣言と書き換え規則という 2 種類の記述でできている こと。
     
  • 論理体系そのものを記述するための言語 を Logical Framework と呼び、Dedukti がその系譜にあること。

でも、率直に言って、動機が分かりません 。

Lean にも Rocq にも、それぞれ検証器が付いています。証明はもう検証済みです。

検証済みの証明を、わざわざ Dedukti に翻訳して、もう一度検証する。

これは、何のためにやるのですか？

専任講師：
良い質問です。開発者たち自身が、その問いに答える文書を残しています。
INRIA が毎年公表している活動報告 と、2023年のLogipedia の論文 です。

順に見ていきましょう。

まず、開発の場所と人から確認します。Dedukti は、フランスの国立研究機関 Inria の Deducteam というチームで開発されてきました。中心人物の一人が Gilles Dowek です。

タロウくん：
そのチームは、何を目指していたのですか？

専任講師：
Deducteam は、Inria のチームとして 2011 年 12 月 1 日に発足しました。2013 年 1 月に探索的アクション、2017 年 1 月にプロジェクトチームへと位置づけが変わっています。チームリーダーは Gilles Dowek です。

発足以来の研究主題は、証明の相互運用（proof interoperability）と、その土台となる logical framework です。

出典：Inria, Presentation of the Project-Team DEDUCTEAM. https://raweb.inria.fr/rapportsactivite/RA2019/deducteam/uid1.html

彼らの動機は、次の事実認識から始まります。

形式化された数学の証明は、定理証明支援系ごとに分断されている。

この点は連載 3 回目でも述べましたが、過去記事をお読みになられていない方のために、あらためて記します。

Rocq の証明は、そのままでは Isabelle で検査できません。Isabelle の証明も、そのままでは Rocq で検査できません。同じ「フェルマーの小定理」の証明が、定理証明支援系の数だけ、別々に、ゼロから書かれています。

この認識は、Deducteam の発足から 12 年を経た 2023 年に、Dowek と Thiré が公表した Logipedia の論文にも、はっきりと記されています。

同論文の要旨は、次の 3 点を述べています。

第1に、形式証明のライブラリは数学の遺産の一部でありながら、使い勝手も持続性も乏しい。

第2に、どのライブラリも特定の定理証明支援系に固有であり、ときにはその定理証明支援系の特定の版にすら固有である。

第3に、ある定理証明支援系で作られたライブラリは、一般に別の定理証明支援系では使えず、その定理証明支援系が保守されなくなればライブラリごと失われかねない。

原文では each library is specific to a proof system と記されています。

出典：

G. Dowek, F. Thiré, "Logipedia: a multi-system encyclopedia of formal proofs", arXiv:2305.00064, 2023 年 4 月 6 日投稿. https://arxiv.org/abs/2305.00064

タロウくん：
・・・たしかに、Mathlib の成果を Agda から使う、という話は聞いたことがありません。

専任講師：
その分断への解答として、Deducteam は「すべての証明を、一つの共通の枠組みの上に表現し直す」という道を選びました。その共通の体系が λΠ計算 modulo rewriting であり、それを読み込んで型検査するプログラムが Dedukti です。

タロウくん：
では、最初の質問に戻ります。検証済みの証明を再検証する意味は、どこにあるのですか？

専任講師：
意味は、少なくとも 3 つあります。

第 1 に、検査の独立性です。

Rocq の証明を Rocq が型検査で受け入れた、という事実は、「Rocq の実装にバグが無ければ正しい」ということを意味します。

この「実装」がどこまでを指すかは、数え方で変わります。

カーネルだけを数えるのか、パーサや仮想機械や OCaml のコンパイラまで数えるのか。数え方によって、行数の見積もりも大きく変わります。

Dedukti の証明検査器は、それよりはるかに小さいプログラムです。

小さく、独立した別の証明検査器が同じ証明の型検査を通せば、証明の信頼は、特定の定理証明支援系のソースコードへの信頼から切り離されます。

📌 厳密性を担保した説明をすると……「小さな証明検査器」だけで信頼は完結するのか

完結しません。

証明が別の定理証明支援系から Dedukti に移されるとき、経路はこうなります。

元の証明 → 翻訳器 → Dedukti の証明 → Dedukti の証明検査器

Dedukti の証明検査器が正しくても、翻訳器が元の証明の意味を写し間違えていれば、結果は信用できません。

したがって、次の3つは分けて考える必要 があります。

  • Dedukti に書かれた証明項を、正しく検査できるか
     
  • 元の定理証明支援系の証明を、意味を壊さずに Dedukti の証明へ翻訳できるか
     
  • 翻訳先の理論に、元の定理証明支援系には無かった強すぎる公理が入っていないか

本記事が「小さな証明検査器」と述べているのは、検査についてです。

証明項を検査するプログラムの核を、小さくできる、という意味です。
翻訳器や符号化の正しさが自動的に保証される、という意味ではありません。

翻訳 のほうは、保存性（conservativity）という定理 として研究されています。

翻訳器のバグが何を壊し、何を壊さないかは、次回以降の記事で扱います。

タロウくん：
・・・監査を、別の会社にもう一度やらせるようなものですか。

専任講師：
監査人が小さな会社である点まで含めて、その理解で合っています。

証明検査器が小さいほど、証明検査器のソースコードを人間が肉眼でコードリーディングして、証明検査器に誤りが潜んでいないかどうかを自分で確かめられるから です。

pic_add_b.jpg

第 2 に、証明の再利用です。

HOL Light で証明された定理を Dedukti* に翻訳し、そこからさらに 別の定理証明支援系の形式へ変換 する。

この経路が通れば、ある定理証明支援系の資産を、別の定理証明支援系から使う道が開きます。

Deducteam は この考え を Logipedia ── 定理証明支援系を横断する「証明の百科事典」 ── として掲げました。

Logipedia の構想は、Thiré が 2018 年に発表した翻訳の仕事を出発点 としています。

タロウくん：
翻訳は、実際に成功したのですか？

専任講師：
部分的には成功しました。

Matita で書かれたフェルマーの小定理の証明が Dedukti に翻訳され、複数の定理証明支援系の形式へ書き出されて います。Thiré が 2018 年に発表した仕事 です。

出典：

F. Thiré, "Sharing a Library between Proof Assistants: Reaching out to the HOL Family", Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2018), Oxford, 2018 年 7 月 7 日, EPTCS 274, pp. 57-71. DOI: 10.4204/EPTCS.274.5 ／ arXiv:1807.01873. https://arxiv.org/abs/1807.01873

HOL Light や Isabelle/HOL からの取り込みも研究されています。

ただし、どの定理証明支援系の証明でも自動で翻訳できるわけではありません。定理証明支援系ごとに符号化を用意する必要があり、その定理証明支援系に固有の機能を使った証明は翻訳できないことがあります。この限界は、記事の後半で扱います。

第 3 に、自動証明器の出力の検査です。

Zenon Modulo や iProver Modulo のような 自動証明器 は、証明の探索は得意ですが、その出力が本当に証明になっているかは別問題 です。

自動証明器に Dedukti 形式の証明を出力させ、Dedukti が独立に検査する。

この分業なら、自動証明器の探索アルゴリズムが正しいことを、そのまま信頼する必要はなくなります。

探索の結果が証明になっているかどうかを、証明検査器が独立に確かめるから です。

pic_add_a.jpg

フランスの BWare プロジェクトでは、産業向けの B メソッドの証明義務をこの分業で処理する研究が行われました。

同じ分業は、一階の自動証明器 Vampire についても試みられています。

2025 年の論文が、その事例を報告しています。

Vampire は、理論・帰納法・高階論理などを扱えるように拡張された自動証明器 で、信頼すべきコードの規模が大きく、バグが定期的に見つかっており、まだ隠れているものもあると考えられる、と論文は述べています。

Vampire が出力する証明は長く込み入っていることがあり、人手で確かめることは望ましくも現実的でもない。そこで、Dedukti に検査させる。そうした構図です。

タロウくん：
・・・整理させてください。開発者が考えたユースケースは、

第 1 に、小さな独立した証明検査器による、証明の再検証。

第 2 に、定理証明支援系をまたぐ証明の翻訳と再利用。

第 3 に、自動証明器の出力の独立検査。

この 3 つですか。

専任講師：
そう整理して差し支えありません。そして 3 つに共通する思想を一言で言えば、「証明の正しさを、特定の定理証明支援系から独立させる」です。

pic_1.jpg

タロウくん：
最初は「二度手間では」と思いましたが、二度目の手間にこそ意味がある、という設計なのですね。

専任講師：
そのとおりです。ただし、Logipedia がどこまで実現しているか ── Logipedia は今も更新されているのか、産業で使われた実績はあるのか ── は、期待と現状を分けて見る必要があります。次の節で、事実だけを数字とともに確かめます。

補足 ── Dedukti は、どれだけ使われているのか

対話篇 ① の末尾で述べたとおり、ここでは期待と現状を分けて、事実だけを確かめます。
数字は 2026 年 9 月時点です。

年表 ── Dedukti は、新しい言語ではない

Arend 連載の初回で、筆者は Arend の実績の少なさを「公開からまだ 7 年」という若さで説明しました。同じ説明が Dedukti に使えるかを、先に確かめます。

年 できごと
1998〜2003 deduction modulo（計算を推論に組み込む枠組み）。Dowek・Hardin・Kirchner の Theorem Proving Modulo（Journal of Automated Reasoning、2003）に結実。Dedukti の理論的な源流
2007 Cousineau・Dowek が λΠ-calculus modulo を提案し、全ての関数的 Pure Type System を埋め込めることを示す（TLCA 2007）
2011 Dedukti の最初の実装。Boespflug がエコール・ポリテクニークの博士論文として Haskell で開発
2011 年末 Inria に Deducteam 発足
2012 Dedukti を OCaml で作り直す
2012 Boespflug・Carbonneaux・Hermant が λΠ-calculus modulo を universal proof language として提示（PxTP 2012）。CoqInE（Coq → Dedukti）公開
2013 Zenon Modulo（Dedukti 出力を生成する自動証明器）。産業向け B メソッドを扱う BWare プロジェクト（2012〜2016）
2015 Dedukti v2（Saillard の博士論文による全面再実装）。Holide（HOL → Dedukti、Assaf・Burel）。Assaf の博士論文（Matita → Dedukti の Krajono を含む）
2016 年頃 システム記述論文 Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory（Assaf ほか。未刊行のまま広く引用される）
2017 Lambdapi の開発が始まる（GitHub リポジトリ作成年）。対話的な証明機能・タクティクを持つ後継系
2019 Logipedia 公開。（比較：同年、Arend が公開される）
2022〜2025 EuroProofNet（COST アクション）。相互運用研究の欧州ネットワーク。2025 年 9 月に最終シンポジウム
2023 Dedukti v2.7（連載 2 回目の実機検証で使用した版）
2024 hol2dk と Lambdapi により HOL Light の Multivariate ライブラリ（2 万定理超）を Rocq へ翻訳（LPAR 2024）
2026 lean2dk（Lean 4 → Dedukti）の開発が継続中（6 月更新を確認）。Lambdapi は活発に開発中

計算体系の提案が 2007 年、最初のプログラムが 2011 年です。

そこからすでに15年が経過しています。

Arend（2019 年公開）の 2 倍以上、Lean（初版 2013 年）よりも古い。

年表の中で λΠ-calculus modulo という表記を使っている箇所があります。これは当時の論文の表記です。本連載では、Dedukti の証明検査器が名乗っている λΠ計算 modulo rewriting に統一しています。表記のゆれについては、連載 2 回目で扱いました。

したがって、「若いから実績が少ない」という説明は、Dedukti には使えません。 実績の規模は、別の理由で説明する必要があります。その理由は、次回以降の記事で述べます。ここでは先に、実績そのものを並べます。

主要言語からの翻訳器

定理証明支援系から Dedukti または Lambdapi への 翻訳器 は、2026年9 月時点で、いくつかの主要な体系について公開されています。

完成度、対応する言語機能、保守の状況は、翻訳器ごとに違います。

EuroProofNet が公開している一覧（Tools） と、
Inria の Deducteam 年次報告 2024 で確認できたものを表にします。

言語・体系 翻訳器 方向・補足
Rocq（旧 Coq） CoqInE Rocq → Dedukti。Coq プラグインとして実装。Coq 標準ライブラリの一部を翻訳した実績
Isabelle isabelle_dedukti Isabelle → Dedukti・Lambdapi。生成した Dedukti ファイルは Lambdapi の Coq 書き出しで Rocq へ変換可能。Isabelle 本体側では Makarius Wenzel が証明項出力の改善に取り組んでいる
Agda Agda2Dedukti ／ Dk2agda ／ Predicativize Agda → Dedukti（往路）。Dk2agda と Predicativize は Dedukti → Agda（復路）
Lean 4 lean2dk Lean 4 → Dedukti。EuroProofNet Deliverable 5 に掲載。開発中（GitHub 上で 2026 年 6 月更新を確認）。Ranta の Informath（2026 年）は Lean → Dedukti の変換を利用できるものとして数え、実際に用いている。また STTfaXport の書き出し先に Lean が含まれる（Dedukti → Lean 方向）
HOL Light hol2dk ／ Holide ／ HOLLightToDk HOL Light → Dedukti・Lambdapi。hol2dk は coq-hol-lightの基盤
Matita Krajono Matita → Dedukti。Logipedia の源流
PVS Personoj PVS → Lambdapi
Idris 2 確認できず EuroProofNet の一覧、および Deducteam のリポジトリ群に見当たらない
Arend 確認できず 同上

確認できなかったのは、Idris 2 と Arend の 2 つです。

両言語の利用者には、翻訳器がまだないものと思われます。

pic_2.jpg

体系をまたいで、実際に翻訳された証明

翻訳器があることと、証明が実際に翻訳されたことは、別です。

翻訳された証明の実例を挙げます。

  • Matita の算術ライブラリ（フェルマーの小定理を含む）が、構成的単純型理論（STTfa）へ弱められ、Rocq・Lean・PVS・HOL Light・Isabelle/HOL へ書き出されました。 Thiré による 2018 年の仕事です。これが Logipedia の中身 です。
     
  • Euclid『原論』第 1 巻の形式化（Rocq の GeoCoq）が、述語論理へ翻訳され、複数の体系へ書き出されました。
    Géran が 2021 年に分析し、2022 年に Rocq のタクティク言語への翻訳まで進めています。
    書き出し先は HOL Light・Lean・Matita・OpenTheory（経由で Isabelle/HOL と HOL4）・PVS の 7 つ です。
     
  • Bertrand の定理（Matita で形式化）が、Predicativize で 可述的型理論へ翻訳され、Agda へ書き出されました。 Felicissimo による 2023 年の仕事です。
     
  • HOL Light の Multivariate ライブラリ ── 実解析・複素解析の 2 万定理超 ── が、hol2dk と Lambdapi を用いて Rocq へ翻訳されました（Blanqui、LPAR 2024）。定理証明支援系のあいだの翻訳における、大規模な具体成果の 1 つです。

出典：

  • Inria, Deducteam 2024 Activity Report.

  • EuroProofNet, Deliverables 1 and 13.

実際の利用者

Lambdapi（Dedukti と同じ体系の上に作られた、後発のプログラム。次回以降の記事で扱います） の公式 README には、利用者を列挙した一覧表 があります。

以下は 2026 年 9 月時点の記述です。

  • 自動証明器の出力の検査：高階の自動証明器 LEO-III の Lambdapi 出力拡張。SMT ソルバの証明検証器 Carcara の拡張（SMT 2024、FroCoS 2025）。TSTP 形式から Lambdapi への翻訳（FLAIRS 2025）。一階論理の自動証明器 ZenonModulo。
     
  • 産業向け手法の検証研究：Event-B の証明義務（Rodin が生成）の Lambdapi による検証（ABZ 2024、2025）。TLA+ の集合論の符号化（ABZ 2023）。
     
  • 他形式からの翻訳：MetaMath から Lambdapi（JFLA 2023）。K 言語から Lambdapi（TYPES 2022）。PVS から Lambdapi（Personoj）。Why3 の証明課題変換の検証（PxTP 2021）。
     
  • 理論研究の器として：立方体型理論の Lambdapi 内での形式化（CubicalDk）。

出典：
Deducteam, lambdapi README "Some users". https://github.com/Deducteam/lambdapi

最後の項目は、数珠つなぎ 4 本目（https://qiita.com/etale_cohomology/items/75aa5395b5f8c03e1bf2）の主題と交わります。立方体型理論を、Lambdapi の上で理論として書いた人がいる、ということです。

研究ネットワーク ── EuroProofNet

証明の相互運用を主題とする欧州の研究ネットワーク EuroProofNet が、2022 年から 2025 年まで、COST アクションとして活動しました。公式サイトの記述を引きます。

Initially funded by COST between 2022 and 2025

（筆者訳）当初、2022 年から 2025 年まで COST の資金で運営された

出典：
EuroProofNet. https://europroofnet.github.io/

47 か国から 600 名を超える研究者が参加し、議長は Deducteam の Frédéric Blanqui でした。

2025 年 9 月に最終シンポジウムが開かれ、Logical Framework と証明系の相互運用に関する国際スクール（LFPSI） が、併せて開催されました。

COST としての資金期間は 2025 年で終了しています。

ネットワークとしての Web サイトと議論の場は継続しています。この 2 つは、分けて読む必要があります。

数字 ── GitHub の指標

Arend 連載の初回と同じ物差しで、数字を並べます。

リポジトリ Star Fork コミット数 備考
Deducteam/Dedukti 237 28 2,280 Issues 28
Deducteam/lambdapi 398 44 4,053 Issues 92。開発版は活発に更新中
（参考）Lean 4 約 8,700 ─ ─ Arend 連載初回の物差し
（参考）Agda 約 2,900 ─ ─ 同上
（参考）Arend 753 ─ ─ 同上

Dedukti と Lambdapi は、Arend よりさらに小さなコミュニティです。同じ物差しで、その事実を示しておきます。

pic_3.jpg

産業実績

2026 年 9 月時点で筆者が調べた公開資料の範囲では、CompCert（Rocq）や seL4（Isabelle）に相当する、産業級の成果物は確認できませんでした。

ただし、産業の側との接点は複数あります。
順に挙げます。

第 1 に、BWare プロジェクトです。

フランスの研究プロジェクトで、2012 年から 2016 年にかけて行われました。

B メソッド ── 鉄道など安全性が問われる分野で使われてきた形式手法 ── の証明義務を、自動証明器で証明し、Dedukti で独立に検査する流れを研究 しました。

第 2 に、ICSPA プロジェクトです。

BWare の後継 にあたります。
ANR（フランス国立研究機構）が 2020 年の公募で採択 しました。
課題番号は ANR-21-CE25-0015 です。

ICSPA は Interoperable and Confident Set-based Proof Assistants の略です。

集合論にもとづく証明支援系を、相互運用できるものにし、その証明への信頼を高める、という意味 になります。

参加しているのは、Samovar Paris（主幹）、CLEARSY、Inria Nancy、Inria Saclay、IRIT Toulouse、LRIMM Montpellier です。

このうち CLEARSY は、研究機関ではなく企業です。

フランス南部のエクス＝アン＝プロヴァンスに拠点を置く中小企業で、鉄道の信号や制御など、安全性が問われるシステムを手がけてきました。

B メソッドの開発環境である Atelier B の開発元 でもあります。

ICSPA の目的について、CLEARSY 自身 が次のように述べています。

ICSPA focuses on the set-based specification formalisms B, Event-B, and TLA+ that have been adopted for industrial development projects, for applications where correctness is critical.

（筆者訳）ICSPA が対象とするのは、集合論にもとづく仕様記述の形式である B、Event-B、TLA+ である。これらは、正しさが決定的に重要な用途のために、産業の開発プロジェクトで採用されてきた。

出典：CLEARSY, ICSPA. https://www.clearsy.com/en/research-and-development/icspa/

Dedukti の位置づけについても、同じ資料に記述があります。

The strategy we adopt is to verify these proofs formally and independently with Dedukti, a proof checker simple enough to be audited manually or even re-implemented.

（筆者訳）私たちが採る戦略は、これらの証明を Dedukti で形式的かつ独立に検証することである。Dedukti は、人手で監査でき、作り直すことさえできるほど単純な証明検査器である。

Dedukti を共通の土台とすることで、安全性が問われるソフトウェアのプログラマが、Atelier B、Rodin、TLAPS という各々の開発環境の中で、B・Event-B・TLA+ の開発成果をやり取りできるようになる。これが ICSPA の狙いです。

pic_4.jpg

第 3 に、CLEARSY との協働で、実際にプラグインがリリースされています。

2025 年 6 月に開かれた Rodin User and Developer Workshop の報告に、CLEARSY との協働で、Rodin 向けの Atelier B プラグインの新版を 2 つリリースした、と記されています。

出典：
Proceedings of the 12th Rodin User and Developer Workshop, 2025. https://eprints.soton.ac.uk/503334/1/RodinWorkshop2025_proceedings.pdf

第 4 に、Atelier B の証明を Dedukti で扱う研究論文があります。

Stolze・Hermant・Guillaumé による「Towards Formalization and Sharing of Atelier B Proofs with Dedukti」（2024 年）です。

出典：

これらをどう評価するか。

ICSPA は 研究プロジェクト です。

CLEARSYという企業 が参加し、 Atelier B という産業ツール を対象にしていますが、Dedukti が鉄道の現場に組み込まれて動いている、という段階ではありません。

研究プロジェクトの中で、産業ツールとの接続が試みられている段階 です。

したがって、筆者は次のように整理します。

産業実績そのものは確認できなかった。

しかし、産業ツールを開発する企業が参加する研究プロジェクトが、2020 年代に入って動いている。

まとめます。

  • 産業実績は、筆者が調べた公開資料の範囲では確認できなかった。
  • しかし、学術研究での利用は、研究機関名とプロジェクト名を挙げられるだけ存在する。
  • 翻訳器は主要言語について揃い、2 万定理超の翻訳という具体成果がある。
  • コミュニティは小さい。
  • Dedukti の研究は 1998 年から続いており、実績の少なさを研究期間の短さでは説明できない。

pic_5.jpg

対話篇 ② ── 15 年経って実績が少ない言語に、将来性はあるか

タロウくん：
先生、年表を見て、気づいたことがあります。

Dedukti は、最初のプログラムが作られてから 15 年も経っています。
それなのに、実績は少ない。

2026 年のいまも、研究や普及の活動は活発なのですか？

専任講師：
活動の事実を、確認できた範囲で挙げます。

開発は続いています。

Lambdapi のリポジトリには 4,000 件を超えるコミットが積まれ、開発版は現在も更新されています。Lean 4 からの翻訳器 lean2dk は、2026 年 6 月にも更新されていました。

研究の組織も作られていました。
EuroProofNet という欧州の研究ネットワーク が 2022 年から 2025 年まで活動し、47 か国から 600 名を超える研究者が参加 しました。

Dedukti の講習会 も開かれています。

ただ、EuroProofNet の COST としての資金期間は 2025 年で終了しました。
ネットワークの継続と、資金の継続は、別の話です。

タロウくん：
・・・では、いちばん聞きたいことを聞きます。

Dedukti は、学ぶ価値がありますか？
将来、広く使われる言語になる可能性はありますか？

それとも、誰も使わない、埃を被った言語になりそうですか？

言語の将来性を知りたいです。

専任講師：
まず、確認できる事実だけで答えます。
そのあとで、私の見解を、見解だと断って述べます。

（1点目）。Dedukti の研究目標は、2011 年 12 月のチーム発足以来、利用者数を増やすことより先に、論理の記述と証明の相互運用と独立検査の基盤を整えることに置かれています。

Lean には Mathlib があり、数学者のコミュニティがあります。

Dedukti にそれはありません。

Dedukti が目指してきたのは、証明を定理証明支援系のあいだで翻訳するための、研究の基盤です。

ですから、2 つの問いを分けて考える必要があります。

「Lean のような大きな利用者集団を持つか」という問いと、
「相互運用の研究基盤として重要か」という問いです。

（2点目）。15 年のあいだ、途切れずに研究が続いてきました。

年表で見たとおりです。

  • 理論の提案
  • 2011 年の Haskell 版のリリース
  • 2012 年の OCaml 版のリリース
  • 2015 年の v2 という 3 度のプログラムの作り直し。
  • 翻訳器の整備。
  • 欧州規模の研究ネットワーク。

埃を被った言語は、2026 年に Lean 4 からの翻訳器を更新しません。

（3点目）。Dedukti の将来は、Dedukti だけでは決まらない。

Dedukti の価値は、証明の翻訳元と翻訳先がどれだけあるかで決まります。

AI が Lean で証明を量産する時代が本当に来るなら、その証明を独立に検査したい、別の体系でも使いたい、という需要が高まる可能性があります。

反対に、世界が Lean 一色に収束しきるなら、翻訳する必要そのものが薄れます。

タロウくん：
・・・つまり、Dedukti の将来性は、「証明の世界が多様なまま続くかどうか」に賭けている、ということですか？

専任講師：
そう整理して差し支えありません。

ここから先は、私の見解です。

あなたが学ぶべきかどうかは、あなたが何者かによります。

Lean や Rocq で 証明を書きたいだけ なら、Dedukti を学ぶ必要はありません。
それが大多数の読者にとっての答えです。

しかし、次のいずれかに当てはまるなら、学ぶ価値があります。

  • 定理証明支援系を 作る側に 回りたい人。
     
  • 証明検査器の信頼という問題 を、実際に動く証明検査器のソースコードや動作を見ながら 考えたい 人。
     
  • そして、論理を「使う」だけでなく 「記述する」対象として扱う視点 を手に入れたい人。

この視点は、Dedukti が仮に消えても、消えることはないでしょう。

Logical Framework の考え方は、1967 年の Automath に始まり、1987 年の Edinburgh LF で言語として定式化された、60 年続く系譜であり、Dedukti はその現在形の一つです。

タロウくん：
言語は消えるかもしれないが、視点は残る
── 本連載でずっと言われてきたことですね。

専任講師：
そのとおりです。

そしてこの記事が冒頭に掲げたの問い ── 定理証明器を誰が検査するのか ── は、AI が証明を書く限り消えない問いです。

その問いに正面から取り組んできた 15 年の蓄積として、Dedukti は学ぶに値します。

読者の皆様へのメッセージ

本記事を通じて、読者の皆様にお伝えしたいことは、次の 3 点です。

第 1 に、「定理証明器が受け入れた」は、信頼の終点ではなく、信頼の置き場所の選択だということです。

AI が証明を書く時代、私たちは証明の中身を読む代わりに、定理証明器を信じます。

その信頼がどのプログラムの、どれだけの行数の上に載っているのかを、一度は見ておく価値があります。

第 2 に、その信頼を小さくする研究がなされています。その研究の成果は、ソースコードが公開されており、手元で使うことができます。

論理そのものを記述する言語と、小さな独立した証明検査器。この 2 つは思想にとどまらず、連載 2 回目の実機検証で示したとおり、手元の計算機で動きます。

同時に、翻訳には定理証明支援系ごとの符号化が要り、産業実績を筆者が公開資料の範囲では確認できなかったという現状も、そのままお伝えします。

第 3 に、定理証明器の世界には、定理証明支援系の「上」の階層があるということです。

Lean か、Rocq か、Agda か。定理証明支援系の選択の話の一段上に、論理そのものを記述し、証明を定理証明支援系のあいだで翻訳するという研究領域があります。

この階層を知っておくと、個々の定理証明支援系のニュースが、地図の上のできごととして読めるようになります。

ここまでのまとめ

この記事では、次の 4 点 を述べてきました。

（1点目）
Dedukti の研究は 1998 年から続いています。実績の少なさを、研究期間の短さでは説明できません。

（2点目）
2026 年 9 月時点で、翻訳器は、Lean 4・Rocq・Agda・Isabelle・HOL Light・PVS など、主要な定理証明支援系について公開されています。

（3点目）
体系をまたいで実際に翻訳された証明の実例があります。ただし、規模と件数には限りがあります。

（4点目）
産業界での実績は、2026 年 9 月時点で筆者が調べた公開資料の範囲では確認できませんでした。
ただし、鉄道の安全が問われるシステムを扱う企業 CLEARSY が参加する研究プロジェクト ICSPA が動いており、産業ツール Atelier B との接続が試みられています。

次回記事へ

ここまでの 4 本で、Dedukti が何をするものかを扱いました。

次回以降では、翻訳が成立するための条件を扱います。

本連載では、翻訳が成立することを前提に話を進めてきました。

実際には、翻訳がいつでも成立するわけではありません。条件は 5 つあります。

あわせて、Lean・Rocq・Agda・Arend といった定理証明支援系と Dedukti が 競合しない理由
── 階層が違うこと ── に光を当てます。

📌 用語のミニ解説

📌 本文に登場した定理証明支援系・翻訳器・考え方の、初心者向けミニ解説

Logical Framework（ロジカル・フレームワーク）

論理そのものを記述するための言語です。ふつうの定理証明支援系は、1 つの論理を組み込んでいます。Logical Framework は、論理を定義の対象として扱います。1967 年の Automath に始まり、1987 年の Edinburgh LF（Harper・Honsell・Plotkin）で言語として定式化されました。本記事の Dedukti は、この系譜の現在形の 1 つです。

λProlog（ラムダ・プロローグ）

論理プログラミング言語 Prolog の拡張で、高階の項と束縛を扱えます（Miller・Nadathur）。論理を記述する用途にも使われるため、論理プログラミング型の Logical Framework と位置づけられます。Dedukti との違いは、計算機が何を実行するかです ── λProlog は導出の探索を実行し、Dedukti（dkcheck）は型検査だけをします。ELPI という処理系が、Rocq のタクティク開発にも使われています。

Matita（マティータ）

イタリアのボローニャ大学で開発された定理証明支援系です。Rocq と同じ CIC（帰納構成計算）の系統ですが、小さく作られており、証明項が取り出しやすい構造をしています。本記事に登場した「Dedukti 経由で複数の体系へ翻訳された算術ライブラリ」は、Matita で書かれたものです。

HOL Light（ホル・ライト）

高階論理（HOL）系の定理証明支援系です（John Harrison）。検査の核が数百行と極めて小さいことで知られます。実解析・複素解析のライブラリ Multivariate を持ち、ケプラー予想の形式証明（Flyspeck 計画）にも使われました。本記事の「2 万定理超を Rocq へ翻訳」の翻訳元です。

CoqInE（コック・イン・イー）

Rocq（旧 Coq）の証明を Dedukti へ翻訳する変換器です。2012 年に公開されました。Rocq のプラグインとして作られており、標準ライブラリの一部を翻訳した実績があります。

Zenon Modulo（ゼノン・モジュロ）

一階論理の自動証明器 Zenon の拡張です。deduction modulo を組み込み、見つけた証明を Dedukti 形式で出力できます。探索は自動証明器、検査は Dedukti、という分業の実例です。

BWare（ビーウェア）

フランスの研究プロジェクトです（2012〜2016 頃）。B メソッド ── 鉄道など安全性が問われる分野で使われてきた形式手法 ── の証明義務を、自動証明器で証明し、Dedukti で独立に検査する流れを研究しました。産業の題材に最も近づいた事例ですが、研究プロジェクトであって産業での実績そのものではありません。

ICSPA（イクスパ）

フランスの研究プロジェクトです。ANR が 2020 年の公募で採択しました。BWare の後継にあたります。B・Event-B・TLA+ という 3 つの形式手法の証明を、Dedukti で独立に検証し、3 者のあいだで証明をやり取りできるようにすることを目指しています。参加者に、鉄道の安全が問われるシステムを扱う企業 CLEARSY が含まれます。

predicate subtyping と PVS（述語による部分型）

PVS は米国 SRI で開発された定理証明支援系で、航空宇宙分野の検証で広く使われてきました。その特徴が predicate subtyping ── 「0 でない実数」のように、述語で絞り込んだ部分型を作れる仕組みです。強力な半面、型検査が決定不能になります。この珍しい機能をどう符号化するかが、Dedukti 研究の題材になっています。

matching logic と K（マッチング論理）

K は、プログラミング言語の意味論を定義するための枠組みです。C・Java・イーサリアムの EVM などの意味論が K で定義されてきました。その論理的基盤が matching logic です。これも Dedukti への符号化の研究対象になっています。

de Bruijn 因子（de Bruijn factor）

連載 3 回目の序章で扱った de Bruijn 基準（criterion）とは別の概念です。形式化した数学の長さを、元の非形式の文章の長さで割った比を指します。Wiedijk が名づけました。形式化すると文章が何倍に膨らむか、という量です。基準は「証明を独立に検査できるか」、因子は「どれだけ膨らむか」で、名前だけが同じです。出典：F. Wiedijk, "The De Bruijn Factor", 2000. https://www.cs.ru.nl/~freek/factor/

訂正一覧

公開後に訂正した箇所を、ここに追記していきます。現時点ではありません。

関連記事

本記事の接続先

  • 論理はひとつではない ── 圏論論理学がつなぐ量子論理・トポス・圏論的量子力学 https://qiita.com/etale_cohomology/items/24858c3bd7c7d6833eaa
  • if 文も SQL も、実は別々の「論理」だった ── 古典論理から量子論理まで、21 の論理体系を 5 人で議論【対話篇】 https://qiita.com/etale_cohomology/items/4fadbda1ebea7a63f68d
  • 依存型を使わない Isabelle/HOL とは何か ── AWS のクラウド基盤を検証した定理証明系は、なぜ証明を自動で探せるのか
    https://qiita.com/etale_cohomology/items/6987c76966a3513cd6e0
    Isabelle/Pure という枠組みの上に HOL・ZF・FOL を載せる構造、sledgehammer による自動化、Isar 記法、seL4 と AWS Nitro Isolation Engine の検証を扱っています。連載 3 回目の第 3 章の背景です。
  • トポスと論理の関係 ── ひとつのトポス（数学の宇宙）を選ぶと、なぜ古典論理か直観主義論理が決まるのか ── そして、トポス以外の「器」たち https://qiita.com/etale_cohomology/items/5206679c2fd02aea9512
  • λProlog とは何か ── AI が数学を証明する時代、定理証明系 Rocq の内側で働く知られざる言語
    https://qiita.com/etale_cohomology/items/98b416523f468dc64959
    Prolog を高階論理と単純型付きラムダ計算で拡張した言語、その実装 ELPI、Rocq の拡張言語 Coq-Elpi、高階抽象構文（HOAS）を扱っています。連載 3 回目で挙げた論理プログラミング型の枠組みの詳細です。

数珠つなぎ連載（型理論から立方体型理論へ）

📚 Arend 連載（全 8 本）

出典一覧

0
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?