Pairwise interaction models appear in various applications in scientific computing and machine learning, and these applications often symmetrically call kernels that implement pairwise effects. In that situation, a pair of symmetric calls shares much part of calculations, i.e., has much redundancy. This redundancy is not captured in ordinary compiler optimizations and therefore is eliminated by the hands of experts. This is not productive at all both for experts and non-experts. To resolve this problem, we present an approach to eliminating the redundancy, based on symmetry verification with SMT solvers and data-flow analysis on static single assignment form. We have implemented our approach as a source-to-source compiler that generates C++ code from an embedded language in Python and achieved about 20–40% reduction in execution time for non-trivial kernels.