実験ノート：COBOLのモダナイゼーション with Opus4.6(その4):Leanによる形式的な変換を試す→失敗するもSMTソルバ版で論文化までやった

前記事では、COBOLプログラムのモダナイゼーション（TypeScript等への変換）において、 元のプログラムが持つ性質（プロパティ）が変換後も保存されることを検証可能にする仕組みを構築した。

経緯としては、型安全なシステム、ここではstatic modeのTypeScript、に変換する仕組みに、後から、事前にプログラムの性質（プロパティ）を定義して、これが変換後にも保たれるというのを検証手段としてつけたという流れで、自分で言うのも何だが、積み上げ式で理解できる範囲の作業であるともいえる。

なんか、形式化という点では、物足らない。Opus4.6のその力を出し切れてないのではないか。。

定理証明系(Lean)を仲介した形式的な手法を探索 Opus4.6

そこで、Claude Code on the webを使い、既存のリポジトリに対して以下の依頼を、Opus4.6をモデルとして行った

本当に、think ultra deppしてくれるだろうか？

おお、”thorough understanding of the codebase"ということで理解してくれて、さらに、" Let me design and implement the Lean-based formal verification system."ということだ。中身は、COBOLをleanの依存型理論として形式化、プロパティはproof obligationに変換、変換の正しさの証明、そして、ランタイム検証と形式証明の統合？？最後は判らんな。。

以下のような手順をふんで、これを実行する。。。できるのか。。

いや、快調にすすんでいるわけですが、本当か？

この辺りで、利用料が43%消費してまったい。

テストに入って、はまっている模様。。そう簡単にいくはずない。

なんだって、Buildが成功し、テストが通った？そんな馬鹿な。

完成！

そしてなんと、勝利宣言。

新たに作ったのは、３つのモジュール

そして、サンプル事例の評価結果は。。

本当にやったのか？聞いてみる

本当なのだろうか？いつものとおり、怪しすぎだな。。

すると、するっと正直な回答が。。

Leanへの変換が正しいということをチェックしただけか。

そうだよね、サンプルをLeanに変換して、確認しないと「できた」とは言えないとおもう。しかし過去の経験上、Claude Codeで leanをインストールさせて実行するというのはうまくいかなかったな。あきらめるか。。。

ここまえ利用量が66%かあ、

Lean4による検証をお願いする

まあ、ダメもとで、Sonnet4.6に切り替えて実行だ！

やっぱり、Leanはインストールできない、しかし代わりにSMTソルバ―をインストールするとな？

なんか、壮大なる、いやな予感、、今まで作ったLeanの仕組みのほかの検証の仕組みを作る勢い。。

なんとSMTに切り替えて再試行

どうも、SMTへの変換と証明が動いている模様、テスト中。

やっぱり、こなれたSMTソルバーに切り替えたといっても、一筋縄ではいかない、

どんどんバグを修正し、テスト再開して、通った？？

といっても、全部のプロパティが証明(sat)になるわけではなく、引き続きデバグ中。

なんか、いい感じなのか？

"INV-03"が、まだ残件になっている。それ以外は"PROVEN"なんだね。

深いデバグを行っている

なんか問題がとても深いところにある模様、、

なんとなく、Root Causeを見つけたような、感じだな。

やっぱりうまくいかない、unsatだ。SMTソルバのオプションを変えて再実行？

いや、どんどんはまっていくような感じなんですけど。。利用量はすでに100%、追い銭をつかって継続中。。。

最後のテストをやっているようだが、なんかはまっている not scientific notationというのは何だ？

おお、テストが進んだ、

やっと完成

そして、勝利宣言！

SMTによる検証を論文化

もう、利用料が100%超えているからやけくそだ。

どうやら完成、

出来た論文をPrismに突っ込んで、、、

成果物をここに供養する。中身はあとで見返そう。。