技術要約: BARReL - LeanにおけるAtelier Bのためのモダンなバックエンド

問題提起

Bメソッドとその産業用ツールセットであるAtelier Bは、強力な保証議論を必要とする安全性の高いシステムの開発において、長らく標準となってきました。しかし、そのエコシステムはAtelier Bの内部プルーバーに大きく依存しており、これらは信頼できる計算基盤（TCB）に関して「ブラックボックス」内で動作しています。これまでの取り組みでは、Isabelle、PVS、あるいはRocqのような現代的な対話型定理証明器（ITP）とBを接続する試みがなされてきましたが、それらの多くはBのセマンティクスを形式化することに焦点を当てており、既存の産業用ワークフローに統合された実用的なバックエンドを提供することには至っていません。さらに、既存のツールは、Bメソッドの中核でありながら注意深いウェルディファインドネス（WD：定義可能性）チェックを必要とする部分演算子（例：min、部分領域上の関数適用）の堅牢な処理に欠けていることがよくあります。Atelier Bの対話モードでは、ユーザーが誤って、定義されていない項（例：min(∅)）をインスタンス化してしまうことがあり、ツールが手動のルール適用中に型制約の強制に失敗すると、不当な証明につながる恐れがあります。

手法

本論文では、Atelier BとLean証明支援機を橋渡しするように設計されたLean 4ライブラリであるBARReL（B Automated tRanslation for Reasoning in Lean）を紹介します。その手法は、Bの証明義務（PO）をLeanの定理へと変換するモジュール式の翻訳パイプラインに基づいており、Leanの依存型システムを活用して、構成によるウェルディファインドネスの強制を実現しています。

コア・アーキテクチャ

図1に示されるワークフローは、以下の4つのパスで進行します。

1. パースおよびPO生成: BARReLは、Bマシン（.mch）、リファインメント、または既存のProof Obligation Generator（POG）ファイルを受け取ります。そして、Atelier Bのbxmlおよびpogツールを呼び出し、XML形式で証明義務を生成します。
2. AST正規化: XML形式のPOは抽象構文木（AST）にパースされ、後続のエンコーディングを簡素化するために正規化されます（例：P ∧ Q ⇒ R を P ⇒ Q ⇒ R に変換）。
3. エンコーディングとメタプログラミング: 正規化されたBの論理式は、Leanのメタプログラミングフレームワークを使用してLeanの項へと転写されます。決定的なのは、このレイヤーがBの集合論的構成をMathlibの型付き集合および関係のプリミティブへとマッピングすることです。
4. ウェルディファインドネス（WD）の取り扱い: これが中心的な技術的革新です。BARReLは、Atelier Bの暗黙的な部分演算子の取り扱いに頼るのではなく、すべての部分演算子の使用に対して明示的なWD条件を生成します。

部分演算子の取り扱い

Bにおいて、min(S)や関数適用f(x)のような演算子は部分的です。Atelier BはWDサイドゴールを生成しますが、これらが満たされればメインのゴールが成立すると仮定します。BARReLは、部分演算子を、ウェルディファインドネスの証明を明示的な引数として要求する全域的なLean関数としてエンコードすることで、これとは異なるアプローチを取ります。

• メカニズム: Classical.choose（ヒルベルトの$\epsilon$演算子）を使用することで、BARReLは部分演算子を、型シグネチャに証明パラメータ（例：min.WD S）を含む形で定義します。
• 強制: min(S)をLeanの項の中で使用するには、ユーザーはSがWD条件（例：Sが空ではなく、かつ下限を持つこと）を満たすという証明を提供しなければなりません。
• 自動化: BARReLは、これらのWD証明をサイド定理またはサブゴールとして生成します。wd_minやwd_appといったカテゴリが付与された軽量な自動化タクティクスのレイヤーが、Mathlibの書き換えルールや集合論的補題を用いて、これらの定型的なWDゴールを自動的に解消することを試みます。

信頼境界

本システムは証明生成バックエンドとして設計されています。ユーザーがLean内でゴールを解消すると、結果としての定理はLeanの小さく監査可能なカーネルによってチェックされます。信頼されるコンポーネントは以下に限定されます。

1. Leanのカーネルとメタ理論。
2. Atelier Bの外部PO生成（bxml/pogステップ）の正当性。
3. BのセマンティクスをLeanへエンコードする際のBARReLの忠実性。
   論文では、Atelier Bのインタラクティブ層（ユーザーが変数を手動でインスタンス化する箇所）は証明を生成するものではなく、不整合を引き起こす可能性があることが明記されています。BARReLは、型チェッカーを通じて型正当性とウェルディファインドネスを強制することで、このリスクを排除します。

主な貢献

1. BARReLライブラリ: Bの構文と表記を可能な限り維持しながら、Bの開発（マシン、リファインメント、実装）をLeanの定理へと変換する、オープンソースでモジュール式のLean 4バックエンド。
2. 明示的なウェルディファインドネス・ディシプリン: Bの部分性を、明示的で証明可能なウェルディファインドネス条件へと変換する翻訳パイプライン。これにより、不当な型付けや定義されていないインスタンスへの静かな依存を防ぎます。これは、Atelier Bの対話型プルーバーにおける既知の落とし穴です。
3. 評価とワークフロー: Lean内での「最小値探索」アルゴリズムを用いた、エンドツーエンドのリファインメント・チェーンのデモンストレーション。この研究は、BARReLがAtelier Bよりも多くのWDゴールを生成する一方で、その大部分が自動的に解消され、ユーザーがコアとなるリファインメント論理に集中できることを示しています。

結果

著者らは、「最小値探索」の仕様に関する3レベルのリファインメント・チェーンを用いてBARReLを評価しました。

• 規模: このケーススタディでは、3つのレベル（仕様、2つのリファインメント）全体で合計190個のゴールが生成されました。
• ウェルディファインドネスのオーバーヘッド: このうち、146個のゴールがWD条件でした。
• 自動化の成功率: BARReLの自動化は、生成されたWD条件の**100%**を自動的に解消することに成功しました。
• 比較:
  • Atelier B: サブゴール間で条件を共有するため、より少ないWDゴール（例：第2リファインメントで2個）を生成しました。しかし、その対話型プルーバーは、ユーザーが注意を払わない場合、不当なインスタンス化（例：min(∅)）を許容します。
  • BARReL: 条件を出現ごとに具現化するため、より多くのWDゴール（例：第2リファインメントで100個）を生成しました。しかし、それらはすべて自動的に解消され、残りの21個の標準的なPOはLean内で対話的に証明されました。
• 実装メトリクス: コアとなるツール群は1,331行のコード（LoC）で構成され、サポート用の補題ライブラリと自動化タクティクスにさらに1,282行のLoCが使用されています。

意義と主張

本論文は、BARReLを、Leanに根ざした強力に信頼できるAtelier Bツールチェーンへの踏み台として位置付けています。

• 信頼性: 証明をLean内に移動することで、すべての証明が小さな検証済みカーネルによってチェックされることを保証し、Atelier BのGUIに見られる不当な対話型証明のリスクを排除します。
• ユーザビリティ: 親しみやすいBの構文と構造を保持することで、産業用B開発者の学習コストを最小限に抑えます。
• 拡張性: モジュール式の設計により、新しいBの構成要素やエンコーディング規則を段階的に追加することが可能です。
• 今後の方向性: 著者らは、以下の3つの将来的な研究分野を挙げています。
  1. サポートされるB言語の断片（シーケンス、ツリー、高度な量化子など）の拡張。
  2. 包含関係（subsumption）によるWDゴールの冗長性の削減（Atelier Bと比較してゴール数が多い問題に対処するため）。
  3. Lean内での検証済みPOジェネレータの開発。これにより、最終的にはAtelier Bのpogを信頼できる計算基盤から除外し、Lean内で直接Bを記述するための組み込みDSLを可能にします。

結論として、BARReLは、元の仕様の構造的完全性を損なうことなく、産業用のB開発を現代的な型理論に基づくバックエンドへと移行できることを実証しました。同時に、検証プロセスの健全性の保証を大幅に向上させています。