反証を学ぶ：大規模言語モデルによる形式的反例生成

概要:
数学的推論には、真の命題に対して厳密な証明を構築する能力と、偽りの命題を反証する反例を見つけ出す能力という、二つの重要で相補的なスキルが求められます。
しかし、現在の数学分野のAI研究はほぼ唯一、証明の構築に焦点を当てており、反例を見つけるという同等に重要な課題をしばしば見過ごしています。
本論文では、反例を推論し生成するために大規模言語モデル（LLM）を微調整することで、このギャップに対処します。
これには、LLMが候補となる反例を提案するだけでなく、Lean 4定理証明機で自動検証可能な形式的証明を作成することが求められます。
効果的な学習を実現するために、定理を体系的に抽出し、選択された仮説を破棄することで多様な訓練データを合成する象徴的変異戦略を導入し、さまざまな反例のインスタンスを生み出します。
厳選されたデータセットとともに、この戦略は、反例生成と定理証明のためのLLMの訓練の有効性と効率を大幅に高める、複数報酬のエキスパート反復フレームワークを可能にします。
新たに収集された3つのベンチマークにおける実験は、我々のアプローチの利点を検証し、変異戦略と訓練フレームワークが顕著な性能向上をもたらすことを示しています。