このケーススタディは、形式的なソフトウェア仕様の広く認められた利点 — 設計上の欠陥の早期発見、前提の明示化、組み込まれた不変条件 — と、その限られた産業界での採用との間にある長年のギャップを扱う。著者らはこのギャップの原因を、形式仕様を書いて保守することの負担と、従来の仕様言語が要求する専門知識にあるとしている。著者らの提案は、非形式的な自然言語の要件と完全に形式的な言語との間に位置する中間表現である。すなわち、軽量な数学的記法で豊かにした自然言語を LaTeX で記述するもので、仕様のレベルで推論・証明できるアサーションを支えるのに十分な精密さを持ちながら、形式手法の深い訓練がなくても読めるものである。
この研究は、自然言語の仕様から同じプログラムを開発する 2 つの方法を比較する。1 つ目では、シミュレーションを実行結果から反復的に修正する。2 つ目では、コードを生成・実行する前に AI が仕様をレビューし洗練させる。著者らは、2 つ目の方法にかかった時間は 1 つ目のおよそ 6 分の 1 であり、最初のコード生成の試みで正しいシミュレーションが得られたと報告している。ケーススタディの題材は組織内での知識の成長のシミュレーションであり、解釈可能性を保ちながらも、自明でない構造、不変条件、パラメーター化を必要とするほど十分に豊かなドメインとして選ばれた。仕様は数回のラウンドを通じて練り上げられ、各ラウンドで著者らはモデルに曖昧さや矛盾を特定させ、説明を補い、実装を依頼する前に仕様を再生成させている。
締めくくりの実験では、曖昧さがもたらすコストを調べるためにこのプロセスを逆向きに実行する。洗練された数学的記述の豊富な仕様から出発し、著者らはモデルに数学記号を使わない平易な言葉で言い直させ、次にそれを 3 段落に要約させ、さらに — 新しいコンテキストで — 要約版から厳密な仕様を再構築するよう求めた。再構築では内容が失われた。著者らの報告によれば、組織という概念はほぼ消え、グラフ構造には有向辺と無向辺の混同やクリークの定義の誤りといった間違いが含まれ、ファシリテーターと組織との関連づけは手つかずのままであり、一時的な辺が導入される前にクリークが選ばれていたため出来事の順序が誤っており、ファシリテーターの予算が欠落していたために予算が無制限であるかのようになり、シナリオの具体性が失われていた。
要点
- 軽量な数学的記法で補強した自然言語を LaTeX で記述することを中間的な仕様言語として提案し、これは形式仕様の利点 — 早期の検証、明示的な不変条件、設計による正しさ — を保ちつつ、重量級の形式手法の記法上の負担を軽減すると論じている。
- コードを生成する前に AI で仕様をレビューし洗練させる方法は、実装を実行結果から反復的に修正する方法の約 6 分の 1 の時間で済み、最初の生成の試みで正しいシミュレーションが得られたと報告している。これは著者らによる 1 つのケーススタディに基づくものであり、プロジェクトやチームをまたいだ統制された比較ではない。
- システムアナリストが制御したい側面と、制御する必要のない側面とを明示的に区別すべきだと論じている。著者らは、GUI のような周辺的な要素はアナリストに相談せずにモデルが変更・拡張してよい一方、ビジネスロジックに関わるものは、特に意図が曖昧な場合には、洗練または確認のためにアナリストに戻すべきだとしている。
- 不変条件に関する役割分担を報告している。人間の設計者が高レベルの不変条件を提示し、モデルは著者らが正しく有用だと判断した低レベルの不変条件を提案した。著者らはまた、自分たちで定義した正しさの不変条件はモデルが提案したものの中には含まれていなかったこと、そしてモデルが提案した不変条件の一部は対応する論理式を伴わない散文で記述されていたことも指摘している。
- 注意の限界を報告している。仕様が数ページを超えて大きくなると、モデルは生成中にときどきその一部を省略した。著者らはこれを、長い仕様を扱う際には抽象化、モジュール化、分解が必要であることの論拠と解釈している。
- モデルが依頼されていない拡張を提案したことを報告している — 挙げられている例は、結果を統計的に安定させるためのモンテカルロシミュレーションである。著者らは、仕様のレベルで検証できることを条件にそれを受け入れた。
- 精密な仕様を緩い散文に要約すると、生成されるプログラムを変えてしまう形で曖昧さが再び持ち込まれると報告し、これを著者らが精密さの優位性と呼ぶものの証拠として提示している。人間が最初に書くビジネスロジックの記述は通常不精密であり、それが残す曖昧な境界によって、モデルは意図されていたよりも多くの部分で創造性を発揮する余地を得てしまう。
補足
著者らはこの研究を、仕様駆動開発と形式仕様言語に対して位置づけている。仕様駆動開発については、数学的記法で補強した自然言語を中間表現として用いることでその上に構築していると述べ、形式仕様言語に対しては、厳密さの一部を読みやすさと使いやすさと引き換えにしている。曖昧さの実験では、モデルが仕様駆動開発のやり方 — 実装する前に中間ファイルで問題を形式化する — で作業することを許可したと述べ、これによってビジネスロジックを取り巻く要素についてモデルが下した判断の透明性が得られたと報告している。この実践そのものについては 仕様駆動開発 を参照。
著者らは自ら限界も述べている。ケーススタディとして用いたシミュレーションは、論理的には複雑だが小規模なソフトウェアであり、開発中には注意の限界、仕様の分解、反復的な洗練といった課題に直面した。生成されたコードはどの時点でも手作業でレビューされておらず、著者らは仕様レベルの推論と不変条件のチェックで十分と判断していた。結果として得られたプログラムは Python で、リンクされたノートブックとして配布されている。また、モデルに実験の結論を明示的に述べさせるには繰り返しプロンプトを与える必要があったと報告しており、これはエージェント型ワークフローをさらに洗練させるべき領域だと示唆している。