この記事では、miniF2Fベンチマークにおける形式的および非形式的な記述を、数学オリンピックの問題に取り組むAIシステムの観点から詳細に分析しています。AIモデルは、自然言語で問題を読み取り、Lean言語に形式化し、証明を行いますが、従来の手法では36%の精度にとどまりました。特に、問題の過半数において形式的な表現と非形式的な表現の不一致が、精度低下の重要な要因とされています。この問題を解決するために、著者たちはminiF2F-v2として修正されたベンチマークを提案し、証明パイプラインの評価では70%の精度を達成しました。これにより、AIにおける形式的推論の評価や自動形式化モデルと定理証明者の関係性の理解がさらに深まることが期待されます。