式を簡単にすると遅くなるSMTソルバーを調査
Metamorphic Testing for Floating-Point Performance Issues in SMT Solvers
この論文をやさしく読む
ひとことで言うと
浮動小数点の論理式を意味を変えず簡単にしたのに、SMTソルバーが遅くなる例を探すテスト法です。
何に役立つ？
プログラム検証などで使うソルバーの性能問題の発見に役立ちます。正解が変わるバグではなく、同値な入力間の不自然な性能差を調べます。
この研究の面白いところ
特殊な浮動小数点値や局所的な簡約規則を使い、実際の問い合わせから別の同値式を作ります。単純化は速くなるはずという直感に反する例を見つけます。
どこまで分かった？
最大の遅延倍率はZ3で33.4、MathSATで5.6、cvc5で4.5、Bitwuzlaで1.8です。これらは発見した例の最大値で平均ではなく、文法からランダム生成した入力では成功が少なかったと報告しています。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
SMTソルバーは、プログラムの検証や合成をはじめ、さまざまな分野で不可欠である。正しさと性能は広く研究されているが、浮動小数点理論についての性能テストは、特に実際の用途から得られる問い合わせでは依然として限られている。 本研究は、浮動小数点の特殊値とピープホール最適化に着目し、意味を保つ書き換え規則を用いたメタモルフィックテストを提案する。これによって、SMTソルバーが浮動小数点式を扱う際の重要な性能上の問題を見つける。 実際の用途から得たテスト入力を使うと、調べたすべてのソルバーについて、問い合わせを簡単化したにもかかわらず求解時間が増えるSMT問い合わせを特定できた。観測された遅延倍率の最大値は、Z3で33.4倍、MathSATで5.6倍、cvc5で4.5倍、Bitwuzlaで1.8倍だった。さらに、文法からランダムに生成した入力ファイルを使う場合は、この手法の成功度が低くなることも観測した。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-17（UTC）
- 最新改訂
- 2026-09-17 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-17 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
SMT solvers are essential in various domains, including program verification and synthesis. Although their correctness and performance have been extensively studied, performance testing for the floating-point theory remains limited, particularly for real-world queries. We propose a metamorphic testing approach that uses semantics-preserving rewrite rules, focusing on floating-point special values and peep-hole optimizations, to uncover meaningful performance issues in SMT solvers' handling of floating-point formulas. Using real-world test inputs, our approach is able to identify for every solver tested SMT queries for which solving time increases when the queries are simplified; we see slowdowns of up to 33.4x for Z3, 5.6x for MathSAT, 4.5x for cvc5, and 1.8x for Bitwuzla. We further observe that the approach is less successful when using input files that were randomly generated from a grammar.
著者のコメント
extended version with appendix of SEFM 2026 paper
arXiv ID: 2609.19735 ／ 要約の誤りについて