AIがCPythonをLeanで形式化、418件のバグを発見
Formalizing CPython
Opus 5.5を使ってCPythonの関数をLeanに書き直し、実Pythonとの突き合わせテストと機械検証を重ねたプロジェクト。4,071関数がレビューを通過し、61万行超のLeanコードと18,898の定理が生成された。証明の過程で見つかった418件のバグ報告のうち、約55件は通常のPythonコードからインタプリタをクラッシュさせたりメモリを破壊したりできる深刻なものだという。
証明チェッカーが受け入れる以上、曖昧なままにはできない。だからこそ証明は、コードが誰もが前提にしている通りに動いていない箇所を見つけるのに向いている。
HNでの議論
54- debugnik
そのトークンを、Frama-CでCPythonを検証するためにACSLアノテーションを追加する方に使った方が生産的ではないでしょうか？AIによる翻訳物ではなく、実際のランタイムを検証できますし、修正は直接upstreamに貢献できます。
- anewhnaccount2
Juliaのstdlibでも同じアプローチが取られています: https://discourse.julialang.org/t/formalizing-julia-in-lean-...
- jakobnissen
このバグ探索のアプローチは非常に有望だと思います（明らかに、大量のバグを見つけていますから）。長期的な課題は、この種のバグ探索をテストスイートの一部として日常的に行えるようにする方法です。これらの人々が取ったアプローチは、Juliaの人々がやったときと同じアプローチですが、人間とAIエージェントの両方の作業を大量に必要とするため、実際には自動化できません。
長期的には、コードとLeanの証明が乖離しないように、言語に組み込む必要があると思います。つまり、コードと一緒に書かれるオプトインのプロパティとして、テストスイートでチェックされる形です。通常のコンパイラチェックと非常に似ていますが、より表現力が高くコストが高く、テスト時のみ実行される点が異なります。
- tomtom1337
いくつか点で混乱しているので、誰か明確にしてもらえると嬉しいです！
- Leanへの書き換えが行ごとに行われるなら、なぜ2つの実装で結果が異なり得るのでしょうか（ステップ2）？
- このアプローチはステップ3で「常に真であるべきこと」をどうやって知るのでしょうか（LLMの「推測」する知能によるものですか？）。
- erfgh
AIが書いた記事を読む人はいるのでしょうか。これは真面目な質問です。