サイクル整合性によるファインチューニングでLean4の自動形式化を改善する

要旨: 自動形式化（Autoformalization）——Lean4のような形式的証明言語へ自然言語の数学テキストを自動的に翻訳すること——は、証明検証または証明探索のいずれを通じても、AI支援による数学研究の加速に役立ち得る。私はFineLeanCorpus上で、LoRAを用いてQwen3.5-2Bを自然言語からLean4形式化へファインチューニングし、3つの学習レジームを検討する。すなわち、カリキュラム学習（難易度1〜10）を伴う教師あり微調整（SFT）、カリキュラム順序なしのSFT、そして群相対方策最適化（GRPO）を用いた強化学習（cycle consistency rewardあり）である。サイクル整合性は、NLからLean4へ、そしてNL'へと戻るループを通じて命題の意味がどれだけ保持されているかを測る。これは、既製の文章埋め込みのコサイン類似度として計算される。FineLeanCorpus（FLC）の未見サブセットおよびPutnamBenchにおいて、RLはSFTの2つの変種を大きく上回る（FLCでの平均サイクル整合性が0.669 vs. 0.513、PutnamBenchで0.561 vs. 0.422）。一方で、交差エントロピー損失はわずか0.011 natsしか増加せず、形式化品質への影響は最小限にとどまる。カリキュラム順序は、シャッフルした学習に対して測定可能な利点を提供しない。