誰でも手軽に形式検証！Leanstral 1.5で証明の自動化がもっと身近に

Leanstral 1.5がリリースされました。今回のアップデートにより、数学的な証明をより多くのユーザーが効率的に扱えるようになり、証明の自動化プロセスが劇的に強化されています。形式検証の世界をより身近にする、待望の進化です。

素晴らしい成果だけど、バグ発見の例はちょっと違和感があるな。

一つのバグはdatrs/varintegerライブラリのzigzagデコード用sign関数にあった。入力としてStd.U64.MAXを与えたとき、(value + 1)の式がオーバーフローを起こし、デバッグモードではクラッシュ、リリースモードではサイレントなデータ破損を招いていた。これはテストやファジングでは通常見落とされるエッジケースだ。

この境界条件のケースが、なぜ「テストでは通常見落とされる」と言えるんだろう？確かに質の低いテストなら見落とすだろうし思いつかないかもしれないけど、(a)慎重な人なら当然考えるし、(b)今のMLコーディングシステムも「お、極端な値をテストすべきだな」と判断するのがすごく得意だよね。ユーザー入力をパースするようなものなら尚更。

他にもっと面白いバグを見つけたけど、説明が難しいから省いたのか気になる。

自分もHuggingFaceのリンク自体をここに投稿したよ: https://news.ycombinator.com/item?id=48779902 (https://news.ycombinator.com/item?id=48779902)

特化型モデルが、期待通りのパフォーマンスを出すために必要な入力の具体例を、いろんな問題タイプで提示してくれると助かるんだけどな。LLMが読み込むことを想定した、プロンプト構築のアドバイス用ドキュメントなんかもあるといいかも。

こういうモデルって、プロンプトの構成がちょっと違うだけで結果の質が大きく変わることがよくある。RL（強化学習）のトランスクリプトが見られれば、モデルが何を求めているのか推測するのがずっと楽になるはず。だからこそ、モデルの開発者が初期アドバイスを提供してくれるとかなりありがたい。