プログラム自動改良のための定理証明器