RustとZ3でループなしプログラムを自動合成する
Synthesizing Loop-Free Programs with Rust and Z3 (2020)
プログラム合成とは、仕様を満たすプログラムを自動で見つける技術だ。本記事では、Gulwaniらの論文に基づく「反例誘導型反復合成（CEGIS）」を用い、コンポーネントベースでループのないプログラムをRustとZ3ソルバーで実装する方法を解説する。右端の0ビットを3命令で孤立させる例を通して、SMTソルバーへのクエリや検証の仕組みを具体例とともに紹介。著者は、文献で報告されている性能を再現できず、難しいベンチマークでは解が見つからない問題の診断を読者に呼びかけている。
私たちのプログラム合成器は、1秒未満で解を見つけ、1分程度でその最小長の解を見つけ出す。同じことを手作業でやるなら、それよりずっと長い時間がかかるだろう。