形式的仕様記述言語VDM++を用いたChatGPT開発
VDMという言語をご存知でしょうか？
形式仕様記述というマイナーな言語ですが、昨今のChatGPTの進化に従い、一気に主役の座に躍り出るのではないか？
と思いまとめました。
なぜVDMがこれから生きてくるか？
まずは超ざっくりとVDMというものを解説したいと思います。
ポイント１
VDMとはプログラミング言語ではなく、「仕様記述言語（厳密な）」です。
ポイント2
VDMはシステムの事前条件と事後条件を定義する。実装は書かなくても良い。
システム開発のざっくりした流れ
要求
|
課題->仕様ー＞設計ー＞コーディング
この仕様の部分を担うのがVDMです。
システムというのはつまるところ、
入力に対して出力を得るものです。
入力-> [箱] -> 出力
そして正しいシステムとは、事前条件を満たした時、事後条件が満たされるものが正しいシステムです。
逆に言うと、事前条件と事後条件がなければ正しいプログラムか正しくないプログラムかは評価できないということです。
どういうことかというと、全く同じ階乗のプログラムでも、
事前条件
入力は自然数
事後条件
戻り値は階乗の結果であること
という条件のもとであれば正しいプログラムになりますし、
事前条件
入力は自然数
事後条件
戻り値は偶数であれば真を、奇数であれば偽であること
という条件の元では間違ったプログラムになります。
ChatGPTは、「いい感じに作っておいて」みたいなざっくりとした指示はいまだに苦手です。（人間でも嫌ですよね）また、あいまいな自然言語での指示は正しい、正しくない基準自体があいまい ということを意味します。
当然出力結果もあいまいなものにならざるを得ないでしょう。これは原理的な課題ですのでいくらAIが進化しようがこの問題は解決するとは思えません。
しかし、ChatGPTは事前条件、事後条件さえ厳密に定義してあげれば驚くほど正しくプログラムを書いてくれます。
入力１、入力２-> [割り算] -> 出力
事前条件
- 入力１、入力２ともに自然数であること
- 0 < 入力２ であること
事後条件
- 出力 = 入力１/入力２ を満たすこと
具体例
10、2 -> [割り算] -> 5
VDMでは具体的にこうかけます。
functions
箱:入力1の型 * 入力2の型 -> 出力の型
箱(入力1,入力2)==is not yet specified
pre
自然数であること(入力1)
and
自然数であること(入力2)
and
0<入力2
post
RESULT = 入力1/入力2
VDMはあくまで仕様ですから、箱の中で具体的にどうするかは書かなくて良いのです。
このような割り算を求めるような単純なシステムであれば箱の中を書かなくて良いメリットはいまいちピンとこないかもしれませんが、以下の場合ではどうでしょう？
入力-> [ソート] -> 出力
事前条件
- 入力は自然数の列であること
事後条件
- 出力は昇順にソートされていること
ソートアルゴリズムはたくさんありますが、VDMでは具体的にアルゴリズムを記述することなく、事後条件を定義することができます。
仕様なしではシステムが正しいか間違っているかは定義できません。
何が正しく、何が間違っているかを定義する。
それを数学的に厳密に記述できるVDMは、システム界の聖書と言っても過言ではありません。
functions
ソート: seq of int -> seq of int
ソート(入力)==is not yet specified
pre
自然数の列であること(入力)
post
昇順にソートされていること(RESULT) -- RESULTとは出力（戻り値）のこと
VDMを本当にざっくりまとめると、
- システムの事前条件、事後条件を具体的に定義し、システムの正しさを厳密に示すもの
- 実装は書かなくても良い
となります。
この性質が実はChatGPTととても相性が良いのです。
以下にVDMを利用したChatGPTでのプログラミングの具体的な例を示します。
欲しい物
Pythonの関数
２つの同じshapeのnumpy.array型の引数をとり、それぞれの引数の値の中間のランダムな値が入ったnumpy.array型の値を返す。
例
ret1 = random_between_arrays(np.array([1,2]),np.array([5,10]))
ret2 = random_between_arrays(np.array([1,2]),np.array([5,10]))
ret3 = random_between_arrays(np.array([1,2]),np.array([5,10]))
print(ret1) # [3,5]
print(ret2) # [1,7]
print(ret3) # [4,9]
第１段階（厳密なVDM）
下記のVDM++の仕様に従ってrandom_between_arrays関数のプログラムを作ってください。
ただし、以下の設計に従ってください。
言語：python
引数の型：numpy.array
戻り値の型：numpy.array
types
RecursiveSeq = seq of RecursiveElement;
RecursiveElement = int | RecursiveSeq;
functions
flatten: RecursiveSeq ->seq of int
flatten(s) == (
if is_(hd s,int) then [s]^flatten(tl s)
else
flatten(hd s) ^ flatten(tl s)
);
getShape: RecursiveSeq -> seq of int
getShape(s)==(
if not is_(hd s,RecursiveSeq) then []
else
[len s] ^ getShape(hd s)
)
pre
isSquear(s)
;
isSquear: RecursiveSeq -> bool
isSquear(s)==(
if is_(hd s,int) then true
else
forall i in set inds s & isSquear(s[i]) and len(s[i])=len(s[j])
);
public random_between_arrays:RecursiveSeq * RecursiveSeq->RecursiveSeq
random_between_arrays(arg1,arg2) == is not yet specified
pre
isSquear(arg1) and isSquear(arg2)
and
getShape(arg1) = getShape(arg2)
post
seqDepth(arg1) = seqDepth(arg2) = RESULT
and
getShape(arg1) = getShape(arg2) = getShape(RESULT)
and
forall i in set inds flatten(RESULT)&
flatten(arg1)[i]<=flatten(arg2)[i] => flatten(arg1)[i]<=RESULT[i]<flatten(arg2)[i]
and
flatten(arg2)[i]<=flatten(arg1)[i] => flatten(arg2)[i]<=RESULT[i]<flatten(arg1)[i]
;
この場合、黒い画面がVDMで書かれた仕様です。
そして、
言語：python
引数の型：numpy.array
戻り値の型：numpy.array
と指示している部分が設計となります。
具体的な言語の指定、言語に対して具体的な引数の型などは設計ですのでこれはVDMの範疇ではありません。
VDMで書くのは、pythonのnumpy.arrayやJavaのArrayListではなく、列（sequence）か集合(set)か写像(map)かという極めて原理的な部分です。
システムを使う側からしてみれば実装がnumpy.arrayだろうがpython標準のlistかというものは関心の範囲外です。
しかし、このVDMの具体的な実装を見て、ぐぇっ、習得するの大変そう…と思った方もいるのではないでしょうか？
しかし粒度の細かい関数の具体的な実装、例えばpythonでいうところのshapeと同じ動作の関数を、そのまま「この関数は、sのshapeの列を返します」と入れてやればよいのです。
これでは結局自然言語で仕様書くのと変わらないんじゃないの？と思うかもしれませんが、あいまいな所を明示的にするというだけでAIにはとても解釈しやすいものになります。
以下がVDMのちょっと難しい部分を自然言語にしたChatGPTへの指示です。
第２段階（関数の実装はしないで処理の概要を自然言語を記述したVDM）
下記のVDM++の仕様に従ってrandom_between_arrays関数のプログラムを作ってください。
ただし、以下の設計に従ってください。
言語：python
引数の型：numpy.array
戻り値の型：numpy.array
戻り値には、ランダムなint型の値が入ります。
types
RecursiveSeq = seq of RecursiveElement;
RecursiveElement = int | RecursiveSeq;
functions
flatten: RecursiveSeq ->seq of int
flatten(s) == この関数は、入れ子の列をフラットにします;
getShape: RecursiveSeq -> seq of int
getShape(s)== この関数は、sのshapeの列を返します
pre
isSquear(s)
;
isSquear: RecursiveSeq -> bool
isSquear(s)==この関数は、sがスクエアな配列かどうか、つまりpythonでshapeで各深さの要素数が一定であるかどうかを返します;
--------基本的に読むのはここから下だけ--------
public random_between_arrays:RecursiveSeq * RecursiveSeq->RecursiveSeq
random_between_arrays(arg1,arg2) == is not yet specified
pre
isSquear(arg1) and isSquear(arg2)
and
getShape(arg1) = getShape(arg2)
post
seqDepth(arg1) = seqDepth(arg2) = RESULT
and
getShape(arg1) = getShape(arg2) = getShape(RESULT)
and
forall i in set inds flatten(RESULT)&
flatten(arg1)[i]<=flatten(arg2)[i] => flatten(arg1)[i]<=RESULT[i]<flatten(arg2)[i]
and
flatten(arg2)[i]<=flatten(arg1)[i] => flatten(arg2)[i]<=RESULT[i]<flatten(arg1)[i]
;
上記の方法でChatGPTに入力した所、何れも意図したプログラムが得られました。
VDMの学習コスト
VDMは言語仕様よりも背景となる数学の知識が必要になります。
数学の知識と言っても、理系大学学部レベルの数学の知識があれば問題ありません。２ヶ月程度の学習時間ですらすらと読めるようになると思います。
最低限意味が理解できる程度であればand or 集合や全称記号∀など分かれば問題ありません。
さあ、それでもやっぱりVDMはハードルが高いよと思われた方。
ご安心ください。
あなたにはChatGPTがついています。
↓
You
以下のVDM++で書かれた仕様の一部を非エンジニアにもわかるように解説してください
types
RecursiveSeq = seq of RecursiveElement;
RecursiveElement = int | RecursiveSeq;
functions
flatten: RecursiveSeq ->seq of int
flatten(s) == (
if is_(hd s,int) then [s]^flatten(tl s)
else
flatten(hd s) ^ flatten(tl s)
);
getShape: RecursiveSeq -> seq of int
getShape(s)==(
if not is_(hd s,RecursiveSeq) then []
else
[len s] ^ getShape(hd s)
)
pre
isSquear(s)
;
isSquear: RecursiveSeq -> bool
isSquear(s)==(
if is_(hd s,int) then true
else
forall i in set inds s & isSquear(s[i]) and len(s[i])=len(s[j])
);
public random_between_arrays:RecursiveSeq * RecursiveSeq->RecursiveSeq
random_between_arrays(arg1,arg2) == is not yet specified
pre
isSquear(arg1) and isSquear(arg2)
and
getShape(arg1) = getShape(arg2)
post
seqDepth(arg1) = seqDepth(arg2) = RESULT
and
getShape(arg1) = getShape(arg2) = getShape(RESULT)
and
forall i in set inds flatten(RESULT)&
flatten(arg1)[i]<=flatten(arg2)[i] => flatten(arg1)[i]<=RESULT[i]<flatten(arg2)[i]
and
flatten(arg2)[i]<=flatten(arg1)[i] => flatten(arg2)[i]<=RESULT[i]<flatten(arg1)[i]
;
これに対するChatGPTの回答
ChatGPT
このVDM++の仕様には、特定の種類のデータ構造（RecursiveSeq）を操作するための関数が定義されています。これを非エンジニアにも分かりやすく説明すると以下のようになります：
データ構造の定義
- RecursiveSeq: これは「再帰的なシーケンス」を表します。これは整数のリストか、またはこれらの再帰的なシーケンスのリストです。つまり、リストの中には整数または他のリストが含まれることがあり、その他のリストにも同様に整数またはリストが含まれます。
-
RecursiveElement: これは
RecursiveSeqの個々の要素で、整数（int）か再帰的なシーケンス（RecursiveSeq）のどちらかです。
関数の定義
- flatten: この関数は、再帰的なシーケンスを平坦化して、すべての整数を一つのリストにします。つまり、リストの中に入れ子になったリストがあった場合、それらのリストをすべて展開して一つのリストにします。
- getShape: この関数は再帰的なシーケンスの「形」を取得します。これは、各レベルのシーケンスの長さを示すリストを返します。
- isSquear: この関数は、与えられた再帰的なシーケンスが「正方形」かどうかをチェックします。これは、すべてのシーケンスが同じ長さであることを意味します。
random_between_arrays関数
- この関数はまだ具体的に定義されていませんが、2つの再帰的なシーケンスを入力として受け取り、新しい再帰的なシーケンスを生成することを意図しています。
- 前提条件: この関数を呼び出すためには、入力された2つのシーケンスが「正方形」であり、同じ「形」を持っている必要があります。
- 事後条件: この関数によって生成されるシーケンスは、入力されたシーケンスと同じ深さと形を持ち、それぞれの整数は入力されたシーケンスの対応する整数の間にランダムに選ばれることを保証します。
この仕様は、複雑なネストされたリスト構造を操作し、その構造内でランダムな整数を生成するためのものです。非エンジニアにとっては、これがリスト内のリストを操作し、その要素にランダムな値を割り当てるためのツールであると理解すると良いでしょう。
得られたプログラム
import numpy as np
def random_between_arrays(arr1, arr2):
"""
Generate a random array with the same shape as arr1 and arr2, where each element is
randomly chosen between the corresponding elements of arr1 and arr2.
Args:
- arr1 (np.array): First input array.
- arr2 (np.array): Second input array.
Returns:
- np.array: An array with random values between arr1 and arr2.
"""
# Ensure arr1 and arr2 have the same shape
if arr1.shape != arr2.shape:
raise ValueError("arr1 and arr2 must have the same shape")
# Initialize an array to store the random values
random_values = np.empty_like(arr1, dtype=arr1.dtype)
# Create a vectorized function to generate random values within the specified range
vectorized_random = np.vectorize(lambda x, y: np.random.randint(min(x, y), max(x, y) + 1))
# Apply the vectorized function to the arrays
random_values = vectorized_random(arr1, arr2)
return random_values
# Example usage
arr1 = np.array([[1, 2], [3, 4]])
arr2 = np.array([[5, 6], [7, 8]])
result = random_between_arrays(arr1, arr2)
print(result)
以下国立情報学研究所のVDM＋＋簡易リファレンスです。
https://research.nii.ac.jp/~f-ishikawa/vdm/files/VDM-LangReference.pdf
まとめ
仕様さえ厳密に定義すればシステム開発は楽になる。
それは大規模であるほど、複雑であるほど加速度的にメリットは大きくなる。