Lean4向けザンジバルベース関連言語ZIL、AI向けプロジェクト管理ツール公開

ZILは小規模な関連言語で、名前付きオブジェクト、それらの間の関係、およびその関係から追加の関係を導出するルールを記述します。基本構造は三部構造の関係「主語 ── 関係 ──▶ 対象」であり、例えば「lean.Parser.parse ── implements ──▶ requirement.parseInput」のように、宣言が要件を実装することを表します。

ZIL LeanはこのモデルをLean 4の内部に実装し、Leanが定義、実行可能プログラム、定理ステートメント、証明を検証する一方で、ZILはそれらの検証済み宣言がプロジェクト内の要件、ドキュメント、テスト、タスク、依存関係、およびその他の要素とどう関連するかを記録します。同じプロジェクトマップは「この要件を実装している宣言は何か」「このコンポーネントを検証している定理は何か」「この宣言に依存しているモジュールは何か」「この結果を待っているタスクは何か」「この変更後にレビューすべき宣言は何か」といった問い合わせに答えることができます。

ZILの関連モデルはGoogleのZanzibar（2019年USENIX ATC発表）の論文のセクション2.1に記載されたタプル指向モデルに影響を受けています。Zanzibarは認可タプル、例えば「doc:readme#owner@10」（ユーザー10はdoc:readmeの所有者）や「doc:readme#viewer@group:eng#member」（group:engのメンバーはdoc:readmeの閲覧者）といった形式を使用し、ZILは同じコンパクトな関連構造を認可モデルと広範なプロジェクト関係（宣言が要件を実装する、定理がコンポーネントを検証する、モジュールが別のモジュールに依存する、タスクが課題によってブロックされるなど）の両方に適用します。

ZILはDatalogシステムで一般的に使用されるホーン規則を採用しており、既存の関係から新しい関係を導出するルールを記述できます。例えば「グループがドキュメントを閲覧でき、かつユーザーがそのグループに属する場合、ユーザーはそのドキュメントを閲覧できる」というルールがあれば、このルールは繰り返し評価されて推移的な関係を自動生成します。プロジェクト例では、パーサー、正規化パス、正規化出力に関する定理から、パーサーへの依存関係を記録し、別のルールで変更の波及影響（例えば「lean.Parser.parseが変更されると、それに依存するlean.Normalize.normalizeもレビューが必要」）を導出できます。

LeanとZILの統合により、開発者、レビュー担当者、ビルドツール、ドキュメント生成ツール、課題トラッカー、AIアシスタントが同じプロジェクトマップを使用して、「宣言がどの要件を実装しているか」「変更がどの下流コンポーネントに影響するか」「どの作業がブロックされているか」などを追跡できます。ZILはノード（宣言、要件、クレーム、テスト、ファイル、タスク、ユーザー、グループなど）、関係、ルール、クエリという4つの基本構造を使用し、Lean環境拡張によって事実、ルール、スキーマ、契約、チェックポイント、宣言リンク、証明に支えられたルールを永続化します。また、ZILは「asserted」（直接登録されたプロジェクト事実）、「graphDerived」（推論された関係）、「certified」（Lean命題と証明項に関連付けられたルール）という3つの信頼レベルを記録し、推論された関係がどのように導出されたかを説明できます。

ZILは形式検証と実用的なプロジェクト管理を結びつける試みです。Lean 4は数学的厳密性で知られていますが、大規模プロジェクトではコード、要件、テスト、ドキュメント間の関係を追跡することが、実装の正当性と同じくらい重要になります。ZILはGoogleのZanzibar認可システムの設計パターン（タプル形式、ルール、推移的推論）をプロジェクト管理に応用し、開発者、レビューツール、CI、AI支援など複数のアクターが同じメタデータを共有・問い合わせできる仕組みを提供します。ホーン規則による推論エンジンにより、明示的に記述されていない関係（例えば変更の波及影響）も自動的に導出でき、これはコード検証と並行して、プロジェクト全体の整合性を保つための基盤となります。

まだコメントがありません。最初のコメントを投稿しましょう！