Pythagoras-Prover: Augmented Lean Formalisationによる効率的な形式証明の進展
Pythagoras-Proverは、4Bおよび32Bの自己回帰モデルと4Bの拡散モデルからなる、計算効率の高いLean定理証明器ファミリーです。段階的なカリキュラムSFTと動的証明フィルタリングにより訓練効率を向上させ、Augmented Lean Formalisation（ALF）を導入して検証コーパスを拡張します。実験では、4BモデルがMiniF2F-TestでDeepSeek-Prover-V2-671Bを上回り（86.1% vs 82.4%）、32Bモデルが93.0%でオープンソースの最高記録を達成し、PutnamBenchで93問を解決しました。
現代のLean定理証明器は、高い性能を達成するために大規模な訓練および推論計算を必要とします。その理由の一つは、検証済み証明データの不足と形式証明探索における長い推論トレースにあり、これにより教師あり微調整（SFT）とサンプリングのコストが高くなっています。この課題に対処するため、研究チームはPythagoras-Proverを提案しました。これは、実用的な計算予算に合わせて設計された、計算効率の高いオープンソースのLean定理証明器ファミリーです。このファミリーは、2つの生成パラダイムをカバーしています：4Bおよび32Bパラメータの自己回帰モデルと、推論時にLean証明を反復的に洗練する概念実証の拡散ベース証明器（4B）です。
訓練効率を向上させるために、研究チームはLean検証済みコーパスを構築し、それを簡単、中程度、難しい問題に層別してカリキュラムSFTに使用しました。これにより、モデルは短く単純な証明から長く複雑な証明へと徐々に証明スキルを習得します。SFT中には、動的な証明推論フィルタリングスキームが、情報量の多い証明トレースを保持しつつ、各インスタンスを8kトークンのコンテキスト予算内に収めます。また、研究チームはAugmented Lean Formalisation（ALF）を導入しました。これは、希少な検証コーパスを形式文の変種に拡張し、自己蒸留によって変種を生成することで、すべての変種を正式に検証することなく追加の訓練信号を提供します。既知の問題を摂動させて形式特性を維持することで、ALFは文の表面形式への依存を低減します。
実験結果では、Pythagoras-Prover-4BはMiniF2F-Testのpass@32でDeepSeek-Prover-V2-671Bを上回り（86.1% vs 82.4%）、パラメータ数は約167分の1でした。一方、Pythagoras-Prover-32BはMiniF2F-Testで93.0%を達成し、オープンソースの最先端記録を更新し、PutnamBenchの672問中93問を解決しました。研究チームはまた、ALF変異による汚染感受性ベンチマークであるMiniF2F-ALFを公開しており、評価されたすべてのモデルがこのベンチマークで精度を低下させました。このベンチマークでは、32Bモデルが最も強力であり、4Bモデルは以前の最先端モデルであるGoedel-Prover-V2-32Bと同等の性能を示しました。