Guoxin Chen Jing Wu Xinjie Chen Wayne Xin Zhao Ruihua Song Chengxi Li Kai Fan Dayiheng Liu Minpeng Liao

要約

自動形式化（Autoformalization）とは、自然言語で記述された数学を機械検証可能な形式的命題に変換する技術であり、自然言語で提示された数学問題を形式的数学的推論によって解くために不可欠である。大規模言語モデル（LLM）は文法的に正しい形式的命題を生成することができるが、元の問題の意味的意図を適切に保持することができないことが多く、その原因はLLMアプローチが自動形式化を単純な翻訳タスクとして扱っているためであり、人間の専門家が自然に行う自己反省や反復的精緻化のメカニズムが欠如しているからである。この課題を解決するため、本研究では、意味的一貫性の評価を自動形式化プロセスに密接に統合する「ReForm（Reflective Autoformalization）」を提案する。このアプローチにより、モデルは形式的命題を反復的に生成し、その意味的忠実度を評価し、発見された誤りを段階的精緻化によって自己修正することができる。この自己反省型モデルを効果的に訓練するため、我々は「前向き限界シーケンス最適化（Prospective Bounded Sequence Optimization, PBSO）」を導入する。PBSOは、シーケンス内の異なる位置に異なる報酬を適用することで、モデルが正確な自動形式化と正しい意味的検証の両方を習得するよう促す。これにより、表面的な評価にとどまるような不適切な自己批判を防ぎ、反省の目的を損なうことを回避する。4つの自動形式化ベンチマークにおいて実施した広範な実験の結果、ReFormは最強の既存ベースラインに対して平均17.2パーセンテージポイントの性能向上を達成した。さらに評価の信頼性を確保するため、859件の専門家アノテーション付きデータを含む「ConsistencyCheck」というベンチマークを導入した。このベンチマークは、LLMを審査者として検証するだけでなく、自動形式化が本質的に困難であることを示している。実際、人間の専門家ですら、38.5％のケースで意味的誤りを生じていることが明らかになった。