法令⼯学の可能性と課題

⽚⼭卓也，寺町康昌
Seagaia Meeting, 2023/5/19

法令⼯学の可能性と課題- 法令⼯学による千年⾏政ITシステム-

⽚⼭卓也，寺町康昌
Seagaia Meeting, 2023/5/19

法令は社会を動かすソフトウェア
社会を⽀える制度やサービスは法令により決められている．
規定
国⺠年⾦法
政令
厚⽣年⾦法
政令
所得税法
政令

履修規則

規定
規定

規定

国⺠年⾦制
度・サービス

具現

厚⽣年⾦制度・
サービス

具現

徴税制度・
サービス

具現

国⺠年⾦情報システム

厚⽣年⾦情報システム

規定
規定

税情報システム

規定
規定

教育制度・
サービス

具現

履修情報システム• 法令を正しく作り，進化させることが，社会の安⼼の源• 法律の数２０００本，複雑に絡み合ったスパゲティ状態• 法令の作り⽅は変わっていない：基本的には職⼈的⼿作業，莫⼤な作成・保守コスト

労働者派遣法改正法案の条⽂の誤り• 職業安定局（平成 26 年５⽉ 26 ⽇）
http://www.mhlw.go.jp/file/05-Shingikai-10201000-Daijinkanbousoumuka-Soumuka/0000046988.pdf• 国会に提出した労働者派遣事業の適正な運営の確保及び派遣労働者の保護等に関する法律等の⼀部を改正する法律案（閣法第 56号）において、「⼀年以下の懲役」とすべきところ「⼀年以上の懲役」としてしまったもの。
「附則第６条６ 前⼆項の規定による処分に違反した者は、⼀年以上の懲役⼜は百万円以下の罰⾦に処する。」• 6⽉20⽇廃案、厚労省事務次官以下6名訓告• 最近では，コロナに関連した多くの法案で誤り
4

⽴法爆発• 榎並博利＠富⼠通総研経済研究所• “近年の「⽴法爆発」で法律は「スパゲティ状態」の限界に”• 法と経済のジャーナル

２０１５/９/１８• 法律の数１９５０本、８０００本（省政令を含める）• 内容的にも、複雑に絡み合ったスパゲティ状態• 新聞に報道された幾つかの誤り• ⽴法制度の⼤きな⾒直しが必要• IT利⽤、ソフトウェア開発技術の利⽤• ⼈間によるチェックの限界社会保険オンラインシステムの巨額保守
コスト• 初期構築後４０〜５０年以上を経たシステム• メインフレーム上のCOBOLプログラムの塊• 度重なる法令改正による改修の結果，内部がスパゲティ化• 年間運⽤費⽤• 785億円/年「厚⽣労働省のIT投資状況について」 ，厚⽣労働省 H25/11/21• 変更・機能追加等による費⽤ ソフトウェア 337億円/年「衆議院議員内⼭晃君質問に対する答弁書」，衆議院答弁本⽂情報 H16/4/27• ⼩⿊ ⼀正 : IT予算の8割が維持管理費…「デジタル政府」が延々と進まない …
Business Journal（2020/10/21）• フェーズ1､フェーズ2に分けたシステム改⾰実施中 R1〜R8• データベースの統合とRDB化，計算機システム=>オープン系• COBOLによる計算ロジックは不変

⾏政ITシステムの巨額運⽤経費• ⾏政ITシステム（年⾦，税，⼾籍，．．．）• 根拠法令に従って構築され，社会基盤として⻑期間に亘る安定動作が要求される．

• 制度改正 ⇒ 法令改正 ⇒ システムの改修 ⇒ 内部構造の劣化• 過⼤な保守コスト• 保守開発業者がいなくなる危惧• 保守作業が困難，保守作業の失敗による訴訟• 社会の停滞２種類の法令• 法令Ⅰ：六法全書に載っている法令など• 憲法、⺠法、商法、刑法など• 条⽂の解釈の幅が⾮常に⼤きい．
• 判例や社会的コンセンサスにより条⽂を解釈，裁判で決着⇨ 法推論研究(AI)• 法令Ⅱ：年⾦法などの⾏政サービスに関する法令• 法令という形をしたソフトウェア• 基本的には解釈の幅はない．必要に応じて，補完法令で詳細を規定• 最終的には，⾏政組織や法令施⾏ITシステムにより法令を解釈実⾏⇨ 法令⼯学研究 (SE)

法令⼯学研究の経緯• ⽂科省21世紀COEプログラム「検証進化可能電⼦社会」(2004-2008、北陸先端科学技術⼤学院⼤学(JAIST))で提案• 名⼤法情報研究センターで法制執務システムの研究• 例規データベース(⾃治体条例や規規のテキストレベルの再利⽤）• 多くの⾃治体で利⽤• 中央⼤学研究開発機構法令⼯学研究ユニット(2016ー2020)• セコム研究助成，⽂科省CREST• 例規データベースの⾼度化• 法令⼯学セミナー（阪⼤，中央⼤，東⼯⼤，ＪＡＩＳＴ，筑波⼤）• 興味を持ついくつかの企業（特に，Atrris社）

法令⼯学（１）正しさの保障された法令作成の⽅法論• 現在の法令は， ⽬と⼿だけで作られ，テストをせずに運⽤されている．
• 正しさの確保に多くの汗と時間• 新しい社会制度の実現に必要な法令作成に迅速に対応出来ない．

• ⼿法：法令の論理式記述＋定理証明技術によるテスト･検証（２）正しい法令から法令施⾏ITシステムを作成する⽅法論• 現在の開発⽅法論は，法令の構造を無視している．
• 法令の改正により内部が劣化する可能性• ⼿法：法令指向開発⽅法論
10法令⼯学（１）
条⽂の論理式化による正しい法令の作成

Z3Pyによる国⺠年⾦法の論理式化• 国⺠年⾦法の主要部分約40条の論理式記述実験• 被保険者• 給付：⽼齢基礎年⾦，障害基礎年⾦，遺族基礎年⾦• 述語論理体系Z3Pyにより論理式化･検証• Z3Py : マイクロソフト社製，⾼速定理⾃動証明システムZ3のPython版(Coq ：遺族基礎年⾦のみ)• 結論• 条⽂の論理式による記述は可能である．
• 定理証明システムによる解釈実⾏により，条⽂の正しさを確認• 条⽂は，⽂章上は複雑であるが、論理的深度は浅く定理証明システムは⾼速で動く．

⽼齢基礎年⾦の概略
保険料納付
保険料半額納付免除

資被格保成険立者

免保
除険
要料件半成額立納付Or・日本国内に住む20才以上60才未満・厚生年金の被保険者
・第2号非保険者の配偶者

資格
消滅

受 支
支給 給
給権 開停
発 始 Or
止生・併給の調整

受給権
消滅Or
・被保険者資格の不成立・受給権者の申し出
・死亡・受給権者の死亡AndAnd
・保険料納付期間＋保険料免除期間 10年
・本人配偶者世帯主が困窮・65才に達する･ 残りの半額の納付・被保険者による申請・他の納付免除なし

論理式化の⽅法と記述体系• 条⽂単位で論理式化• 各条⽂で定義される概念を，Z3Py論理式として記述• Python lambda式による述語定義• 殆どの述語は，⽇付(⽇または⽉) ⇒ {True,False}• Z3Py論理式• ⼀階論理• And, Or, Not, Implies, ForAll, Exists, ==• Int, Real, Array, bit列などのドメイン＋それ上の解釈された演算⼦• 抽象データ型

法令⽂の論理式化の例（被保険者の資格）
第七条

次の各号のいずれかに該当する者は、国⺠年⾦の被保険者とする。

⼀ ⽇本国内に住所を有する⼆⼗歳以上六⼗歳未満の者であつて次号及び第三号のいずれにも該当しないもの（厚⽣年⾦保険法 （昭和⼆⼗九年法律第百⼗五号）に基づく⽼齢を⽀給事由とする年⾦たる保険給付その他の⽼齢⼜は退職を⽀給事由とする給付であつて政令で定めるもの（以下「厚⽣年⾦保険法 に基づく⽼齢給付等」という。）を受けることができる者を除く。以下「第⼀号被保険者」という。）
⼆

厚⽣年⾦保険の被保険者（以下「第⼆号被保険者」という。）

三 第⼆号被保険者の配偶者であつて主として第⼆号被保険者の収⼊により⽣計を維持するもの（第⼆号被保険者である者を除く。以下「被扶養配偶者」という。）のうち⼆⼗歳以上六⼗歳未満のもの（以下「第三号被保険者」という。）
2 前項第三号の規定の適⽤上、主として第⼆号被保険者の収⼊により⽣計を維持することの認定に関し必要な事項は、政令で定める。
3 前項の認定については、⾏政⼿続法（平成五年法律第⼋⼗⼋号）第三章（第⼗⼆条及び第⼗四条を除く。）の規定は、適⽤しない。

# f7.py 第７条被保険者の資格, d : ⽇を表す変数
被保険者=(lambda d :Or(第⼀号被保険者(d), 第⼆号被保険者(d), 第三号被保険者(d)))
第⼀号被保険者=(lambda d :And(⽇本国内に住所を有する(d),⼆⼗歳以上六⼗歳未満(d),Not(第⼆号被保険者(d)),
Not(第三号被保険者(d)),
Not(厚⽣年⾦保険法⽼齢等受給可能(d))))
第⼆号被保険者=(lambda d :厚⽣年⾦保険の被保険者(d))
第三号被保険者=(lambda d :And(被扶養配偶者(d),⼆⼗歳以上六⼗歳未満(d)))
被扶養配偶者=(lambda d :And(第⼆号被保険者の配偶者(d),
主に第⼆号被保険者の収⼊により⽣計維持(d),Not(第⼆号被保険者(d))))論理式の検証：充⾜性判定• Z3Pyシステムによる推論：充⾜性判定
論理式P(x,y,z,…)に含まれる変数のx,y,z,…の値の⾃動決定• P(x,y,z,…)＝True になるようなx,y,z,…の値を求める．
存在する ⇒ sat (satisfiable) 解x,y,..,zを出⼒存在しない ⇒ unsat
分からない ⇒ unknown または 停⽌せず
• 命題論理式の充⾜性判定(DPLL)＋解法理論(線形⽅程式・不等式など)
SMT(Satisfiability Modulo Theory)• ネットワーク，OS 等の検証で実⽤化

検証⽅法# v7_ladyA_date.py# 同じ⽇には異なる種別の被保険者にはなれないことの確認
import dummy
dummy.honnin=ʻhonnin_ladyAʼ # 年⾦原簿の設定
dummy.definitions=ʻdefinitionsʼ # ⽤語定義の設定
from essentials import *from f7 import * # 第7条論理式
d=Int('d')
s=Solver()p=Or(And(第⼀号被保険者(d),第⼆号被保険者(d)),
And(第⼀号被保険者(d),第三号被保険者(d)),
And(第⼆号被保険者(d),第三号被保険者(d)))
s.add(p)print(s.check()) # unsat

年⾦原簿
被保険者・受給権者の年⾦関連個⼈記録を論理式で記述したもの# honnin_ladyA_date.py

Ａ⼥史の年⾦原簿

誕⽣⽇=通⽇(1955,5,10)
⼆⼗歳以上六⼗歳未満=区間(年齢到達⽇(20,誕⽣⽇),年齢到達⽇(60,誕⽣⽇)-1)
⽇本国内に住所を有する=DD((1955,5,10),(2020,12,31))
厚⽣年⾦保険法⽼齢等受給可能=FALSE
厚⽣年⾦保険の被保険者=OR(DD((1977,4,1),(1998,9,30)),DD((2008,2,1),(2013,1,31)))第⼆号被保険者の配偶者=OR(DD((1985,6,1),(1998,11,20)),DD((2013,2,1),(2020,12,31)))
主に第⼆号被保険者の収⼊により⽣計維持=AND(第⼆号被保険者の配偶者,NOT(厚⽣年⾦保険の被保険者))…
# dfinitions.py 基本⽤語定義
DD=(lambda x1,x2:lambda d: And(通⽇(x1[0],x1[1],x1[2])<=d,d<=通⽇(x2[0],x2[1],x2[2])))

基本⽤語定義式• 条⽂や年⾦原簿論理式で使われる⽤語の定義• ⽇付関係• ⽇付は1858年11⽉17⽇を原点とした⽇数で計る：修正ユリウス通⽇• 修正ユリウス通⽇と⻄暦年⽉⽇との相互変換，属⽉：通⽇⇒通⽉，• ⽇区間 DD((2020,5,2),(2030,10,1))，⽉区間 MM• ⽉の集合• 期間(f,g)：fが成⽴する⽇の属する⽉の次の⽉からgが成⽴する⽉までの⽉の集合• ⽉数(f)：fが成⽴する⽉数• 年齢の計算 年齢は誕⽣⽇の前⽇に加算される．
• イベントの成⽴の時間的前後関係• 成⽴に⾄る(f)(d)，前に成⽴(d)(g)，間で成⽴(d1,d2)(h)，⽉内で最後に成⽴(f,g,h),…

• ⽇付軸上に拡張された論理演算⼦• OR, AND, NOT, …

検証例

A⼥史の年⾦額の計算• 関連条⽂
27条(年⾦額)
5条(⽤語の定義)
11条(被保険験者期間の計算)
7条(被保険験者の資格))
89条(法定免除), 90条(全額免除), 90条の2(⼀部免除),90条の3(学⽣特例免除)• 年⾦原簿 honnin_ladyA, haiguusaha_ladyA, setainushi_ladyA• 基本⽤語定義集 definitions• 検証スクリプト v27（第27条論理式f27を起動）

条⽂の実⾏
検証スクリプトv_27
第２７条（年⾦額）の実⾏

条⽂論理式
Z3Pyソルバー

年⾦額(a)
a=716000年⾦原簿論理式

基本⽤語定義集

論理式化＋検証により発⾒された条⽂の誤りや不備• 基本的に条⽂は正しく作られているが，• アルゴリズム的側⾯は，⽬視だけによる正しい条⽂の作成には限界がある．
• 第20条の誤りは，事務⼿続きにより運⽤上回避されている．
第２０条(併給の調整) : 誤りの発⾒とその検証
第８条(資格取得の時期)：不備の発⾒とその検証
第９条(資格喪失の時期) : 不備の発⾒とその検証
第２８条(⽀給の繰下) : 不備の発⾒

条⽂の論理式化• ⾏政サービスのための法令は，原理的には論理式化可能• 年⾦法論理式化のこれまでの経験• サービスが実際に実施され，計算機化されている．
（政策，財政などは除く）• 論理式化の⽅法• しばらくは⼈間の⼿作業• 法務実務家，ITエンジニア• ⾃動論理式化• 条⽂は⽤語や表現のぶれが少く，内容的にも幅の狭い⽂章なので，ツールの整備を⾏えば可能か？
• とりあえずは，⽂章構造解析システムがほしい．

施⾏令，施⾏規則，附則• 実⽤システムの構築には，「法律」部分のみでなく，施⾏令（政令），施⾏規則（省令）の論理式化が必要• 法律：原理的側⾯の記述• 施⾏令：法律の条⽂の詳細化･具体化• 施⾏規則：法律，施⾏令の条⽂の詳細化･具体化• これら論理式化が法律部分に⽐べて困難ということはない．

• 附則中での条⽂のバージョン管理記述• 施⾏⽇の指定• 経過措置（「なお従前の例による」，「なおその効⼒を有する」）• 条⽂中の語句の読み替え

⾏政全体の形式記述と検証• 今回の論理式化は，年⾦額の計算に直結する部分のみ• 基本的には述語論理で⼗分• ⾏政組織によるサービスや業務の分担や委譲，被保険者による届出などの側⾯の形式的記述するには，別のメカニズムが必要• 多くの論理体系が既に型式⼿法の分野で提案，研究され，仕様記述などの分野で使われている．

法令⼯学（２）
法令施⾏ITシステムの法令指向開発

法令と⾏政サービス
法令＝条⽂の集合
条⽂の解釈・実⾏・原簿の参照
・計算
年⾦原簿
⾏政組織

税DB

⼾籍DB

福祉DB

…

被保険者受給権者

法令施⾏ITシステムの法令指向開発
条⽂論理式
論理式解釈実⾏システム（定理証明システム）

年⾦原簿論理式

税DB

⼾籍DB

福祉DB

…

被保険者受給権者

法令改正に対応するITシステムの変更➡ 改正条⽂論理式のみを変更
新第n条 yyyyyyyy

改正は条⽂単位条⽂論理式
旧第n条 xxxxxx

論理式解釈実⾏システム（定理証明システム）

年⾦原簿
論理式

千年システムとしての法令• 法令＝条⽂の集合として⾏政サービスを表現• 法令作成の⻑い伝統から適切な条⽂の設定• ⾏政サービスの変更 ⇒ 少数の条⽂の改正
条⽂１

⾏政サービス１
⾏政サービス２

⾏政サービスｋ

条⽂２

条⽂３

条⽂４

条⽂ｎ

千年システムとして⾏政ITシステム
⾏政ITシステム

条⽂１
論理式

条⽂２
論理式

条⽂３
論理式

条⽂４
論理式

条⽂ｎ
論理式

⾏政サービス１
⾏政サービス２

⾏政サービスｋ･ 条⽂を論理式としてコーディング
・⾏政サービス：定理証明器内の条⽂論理式の相互関連により動的に実現

現⾏の⾏政ITシステムの構成法=ユースケース指向
条⽂１

⾏政

⾏政サービスプログラム１

IT

⾏政サービスプログラム２

シス
テム

条⽂２

条⽂３

条⽂４

条⽂ｎ

⾏政サービスプログラムｋ・⾏政サービスを直接コーディング，条⽂との関連は明確に意識されない．
・１つの条⽂の変更により複数のプログラムの変更が必要

法令施⾏ITシステムの「法令指向」開発• 法令指向開発
法令施⾏ITシステム：法令⾃⾝を動かす．
法令施⾏ITシステム＝法令論理式＋定理⾃動証明エンジン＋UI＋DB• 技術的には可能• 論理式記述体系，証明エンジン，ハードウェア• 法令改正への対応• 基本的には，改正条⽂の論理式の変更のみ• 法令の改正を重ねても，システムの構造が劣化することはない．

法令⼯学の社会実装の可能性☓ 法令⼯学１：条⽂の論理式化による正しい法令の作成• 法曹界の現状を考えると困難と思われる．
• 法学部では法律の作り⽅を教えていない．
• 伝統や安定性を重要視する業界• 暫くは新しい技術の導⼊をしなくても，法令の質は守られる．

⚬ 法令⼯学2：法令指向⽅法論• 政府ITシステムの保守困難性の解決は緊急課題• 正しい法令の存在を仮定すれば，論理式化は技術的には可能• 基盤技術は既に存在• 技術以外の問題

出版物
1. 国⺠年⾦法の述語論理による記述と検証：SMTソルバーZ3Pyを⽤いた
ケーススタディ• ⽇本ソフトウェア科学会誌Vol.36, No.3 (2019)

2. 法令⼯学の実践：国⺠年⾦法の述語論理による記述と検証• JAIST学術研究成果リポジトリ(JAIST図書館)• 第１版 2019/9, 第２版 2019/11, 第３版 2020/11，第4版 2021/12• ダウンロード数 約40/⽉• COE Research Monograph Series, Vol. 2 : 法令⼯学の提案• 2007/9 出版• 2019/9〜2020/11 ダウンロード数 1852(⽉平均 154)

法令⼯学（３）Atrris社の取り組み