FormalEvolve: 多様で証明器に有効な自動形式化のためのニューラル-シンボリック進化探索

要約: 自然言語の数学をコンパイル可能で機械検証可能な命題へ翻訳することを自動公式化は目指します。しかし、意味的一貫性が証明器の有効性を意味するわけではありません。意味的に一貫した形式化であっても、証明探索コストと成功率には大きな差が生じることがあります。本研究では、意味的一貫したレパートリを予算付きの推論時探索として定式化し、コンパイル制御型ニューローシンボリック進化フレームワークである FormalEvolve を提案します。FormalEvolve は、境界付きパッチ修復を伴うLLM駆動の変異と交叉により多様な候補を生成します。一方、記号的抽象構文木（AST）書換操作は、構造的多様性をさらに付与します。CombiBench と ProofNet において、厳密なジェネレーター呼び出し予算を T = 100 と設定すると、FormalEvolve は意味的ヒット率（SH@100）をそれぞれ 58.0% および 84.9% に達し、意味的成功の問題間集中を低減させる（ジニ係数が低下する）。固定された証明器予算の下でも、FormalEvolve は CombiBench における下流の証明性能を改善します。コードは公開されます。