Catala - 法律テキストから忠実なアルゴリズムを導出するDSL
(github.com/CatalaLang)- Catalaは、立法テキストから faithful-by-construction アルゴリズム を導出するためのドメイン特化言語であり、社会・財政立法のリテラテイトプログラミングに合わせて設計されたプログラミング言語
- 法律、施行令、判例など、実装対象となる社会・財政メカニズムに関する資料を集めたうえで、条項ごとに各行の意味をコードとして注釈化する形で実装を記述する
- Catalaコンパイラは、完成してテスト済みのコードから、弁護士が読める PDF版 の実装を生成できる。また、法律専門家がレビューし、正確性を認証できるよう、法律専門家との協業を前提に設計された言語でもある
- 中核概念は、Sarah Lawsky教授の A Logic for Statutes に基づく definition-under-conditions と default logic であり、法の論理構造を言語の論理構造が模倣している
- 開発ツールとして、各種テキストエディタ向けのシンタックスハイライト、VSCode拡張、専用LSPサーバー、コードナビゲーション、自動補完、テストスイートUX、
catala-formatフォーマッタを提供している - 学習およびリファレンスには、Catala book、Catala tutorial、フランス語・英語文法の cheat sheet、最新
masterバージョンの コンパイラ文書 を利用できる - コンパイラおよびリポジトリ内のコードは、サブディレクトリに別途ライセンス表記がない限り、Apache license version 2 で配布される
- CatalaはInriaの研究プロジェクトであり、コンパイラはまだ不安定で、一部機能が不足している
1件のコメント
Hacker News のコメント
このプロジェクトは、法律の条文を形式的に仕様化し、法令をおおむね機械的に解釈できる体系が望ましいものだと暗黙に仮定しているように見える。
さらに言えば、裁量や誤差の余地を持つ既存の人間による解釈者の体系は克服すべき問題だと見ていることになるが、その仮定に全面的に反対するわけではないものの、それが正しいかも明確ではなく、著者らがそれを裏づける論拠を示しているようにも見えない。
法令をコードに変える過程を知っている立場からすると、価値がソフトウェア開発者に明確さを提供することに限られるとしても、このプロジェクトがやろうとしていることは理解できる。
これは法の支配とも密接に関係していると思う。https://www.britannica.com/topic/rule-of-law によれば、法律は公開され、明確で、一般的な形式と普遍的な適用可能性を持ち、人々が行動する前に参照できる確定的な要件を含むべきであり、法的義務が遡及的に作られてはならない。曖昧な法律にどんな利点があるのか気になる。
法学の学位を取っていたとき、プログラマーとしてこの分野にかなり関心があり、フランス語圏でこうした法律主義的な取り組みを行う大きなコミュニティを見つけた。私の大学でこの方面に関心を持っていた教授も、その影響圏の側に傾いているように見えた。
何年もの間、弁護士の友人にまさにこういうものがあればいいと説得してきたが、実はおそらくずっと存在していたようだ。
本当にすばらしいと思う。すべての法律はこのような言語で書かれ、シンタックスハイライトと一貫した書式ルールで公開されるべきだ。そのうえで、学校のカリキュラムにこの法律言語を学ぶ内容を含めるべきだ。そうすれば、人々が法律を読み、自分の理解に自信を持つ能力は大きく向上し、社会的にも大きな利益になるだろう。
現実の法律はすでに比較的平易な言葉で書かれており、単語もほとんど常に一般英語での意味そのままだ。問題は、その単語が説明している法概念そのものが複雑であり、他の法律・規則・判例などへの参照が絡み合うことが多い点にある。
同時に、Uniform Commercial Code のように法律が成文化されている場合もある。つまり判例法を一貫した形で書き直し、パッチをマージして整理した事例である。
テストケースも一緒に「織り込む」と面白そうだ。論理文が接する作業面こそ、バグが入り込む場所である。
特に時間的な出来事の周辺ではそうで、それは形式モデルにつながり、バグもさらに増える。通常、キーに関するルールがあるなら少なくとも3つのテストが必要だ¹：より大きい場合、同じ場合、より小さい場合。型などがなければ、負数、null、最大値/最小値の境界入力も必要になる。
たとえば「規則が3か月後に成立し、当事者が B を行使できなくなったが、それでも『17トン』の廃棄物が投棄されたとき……」のようなタイムラインベースのテストを置ける。モデル検査器が統合されれば大いに役立つだろう。形式検証された立法、少なくとも言語をコードにエンコードする過程に DevOps のようなパイプラインを置くこともできそうだ。
¹ https://en.m.wikipedia.org/wiki/Equivalence_partitioning
多くの法律には多義的な表現が多く含まれている。ロシア車両を認めるかどうかに関する最近の EU 規則がよい例だ。ただし、法律をプログラミング言語へ「デジタル化」しようとするとき、あり得る多義性や曖昧な定義をすべて見つけ出すにはよいアイデアかもしれない。
レビュアーにコードが動くと納得してもらうために、ユニット/統合/エンドツーエンドテストで証明しようとするのに似ている。法体系にもエンドツーエンドテストを置くということだ。
さらに一歩進めてテスト群を作成し、そのテストを満たす可能な法律の範囲を自動生成することもできる。
法の意図を明示する標準テストスイート形式をもっと見てみたい
以前住んでいた州で、善意から非常に単純な児童ポルノ禁止法が提案されたのだが、単純すぎた。大まかには「携帯電話で未成年者の露骨な写真を送る者は、児童ポルノ頒布罪に問われる」というようなもので、法律用語では書かれていたが、それ以上に詳しい内容ではなかった。法案提出者に電話して、仮に自分の娘が自分の裸の写真を彼氏に送ったら、新法の下では重罪犯になるのではないかと尋ねたところ、「ああ、しまった、そういう意味ではなかった！」という反応で、結局書き直すために法案を取り下げた
これをプログラムコードのように扱い、「この法律は、未成年者が自分自身の写真を送る場合には適用されない」といったテストを付けることを想像できる。立法者に意図を明確にさせ、「オンライン児童安全法をトランスジェンダー支持コンテンツの禁止には使わない」と言うなら、「よし、それをテストケースに入れよう」と言える。政治家がそのように明文化されるのを嫌がる点が決定的な障害だ
また、意図を反映した法律を書きやすくなり、将来の裁判所が法の意図を評価するのにも使える。文言上は15歳がセルフィーを送る場合に適用されるとしても、テストがそれは意図していないと明示していれば、無罪になり得る。何百もの理由で不可能だろうが、夢見ることはできる
つまり、広く引っかかるようにわざと曖昧に法律を作り、人々に裁判所で争わせるようなやり方であってはならない
法律はコンピュータ上で実行可能である必要はない。意図とその解釈に関するものなので、テストスイート自体も事実上法律の一部であり、単に法律の中に含めればよい
個人的には、どの国であれ法律そのものに立法趣旨を付けてくれれば満足だ。可能なら、機能しているかを見るための重要業績評価指標も付けるとよい。後になって、その法律が実際に機能しているのか、逆効果になっているのか、主な適用例がそもそもの導入理由と違っているのかを再評価できる
[1] https://www.aclu.org/news/juvenile-justice/minnesota-prosecu...
Greg Bear の本 Moving Mars（1993）には、Legal Logic という名前でこれに似たものが少し登場する。人間の火星人たちが新たに独立した社会の法律を作る際に、AI の助けを借りて使うものだ
Greg Bear は1年足らず前に亡くなった有名なSF作家で、当時ここでも彼の訃報が議論されていた。私の十代に大きな影響を与えた作家の一人なので、特に Moving Mars のこの要素が想像力を刺激した記憶があり、Catala が何を提供するのか読んでみたい
[1] https://en.wikipedia.org/wiki/Greg_Bear
[2] https://en.wikipedia.org/wiki/Moving_Mars
[3] https://news.ycombinator.com/item?id=33679668
[4] https://news.ycombinator.com/item?id=33675708
この言語を説明した論文がある: https://hal.inria.fr/hal-03159939。短い動画要約もある: https://youtu.be/OiaFTFSAa1I
プログラマーは、法律に「プログラミング言語」のようなものを使おうと提案するのが好きだ
しかしこれは、曖昧さがある意味では法律の根本的に重要な部分であることを見落としている。世界そのものが、ある面では根本的に曖昧であり、別の面では明確に分かれているからだ。もちろん、あらゆる種類の曖昧さが望ましいわけではない
しかし「コードがすなわち法」になると、抜け穴を悪用するやり方はさらに悪化すると思う。実際、多くの法律は細かな実装方法よりも守るべき価値に注力すべきであり、それは本質的に、より明確でなく、より曖昧にならざるを得ない
これが法律の問題なのか執行の問題なのかは議論しないが、いずれにせよ私たちの社会は曖昧さと不均等な執行の上に成り立っている
value.fair_marketを見ればよい [0]。弁護士たちはその意味をめぐって争えるが、競合する定義もプログラムとして定義できる法律への関心は実装の細部よりも結果に向けられるべきだという点には同意する。そのためには新しい法律の結果を測定する評価関数を作る方法が必要であり、Catala のようなシステムは期待される結果をモデル化し、競合する法案の間で選択する助けになり得る。たとえば結果が「汚染を減らしたい」なら、政策は「汚染産業の禁止」かもしれないし、「汚染の外部性への課税」かもしれないが、どちらも複雑な結果を生むので、自動分析と実証的測定のほうがよいだろう
[0] https://github.com/CatalaLang/catala#concepts
コンピューターが法律文言について実際に推論するうえで、大きく解決してくれる問題があるのかはよく分からない。複雑なのは衡平性の比較衡量であり、そこには依然として人間と弁護士が必要だ
立法者、弁護士、裁判官の中にこれを期待している人がいるのか、それともプログラマーだけが期待しているのか気になる
私たちの法体系をあまり信用していない。なぜ聞くのか分からない
カタルーニャ語を話す立場からすると、記事で述べられている言語との名前の衝突は非常に残念に感じる
名前の選び方が本当に残念だ。プログラミング言語に「français」「Deutsch」、あるいは「English」と名付けるようなものだ
readme の下のほうには「この言語は Pierre Catala にちなんで名付けられた」とある。むしろ PierreLang に変えることを提案する
カタルーニャ語のネイティブとして、名前を見てかなり驚いたが、よくある姓なら納得できる