解説ねえ智也くん、この論文のタ…
TL;DR
AdvancedMathBenchは、LLMの高度な数学証明能力を評価するベンチマークスイートです。証明生成用のProverBench（245問、学部・博士資格試験レベル）と、証明検証用のVerifierBench（888件のモデル生成証明＋専門家正解）から構成。自動検証パイプラインで証明の正誤・誤り箇所を詳細評価します。最良モデルでも学部64.5点、博士資格試験48.9点、検証F1は65.1と低く、高度な証明の生成・検証は依然困難です。
解説
ねえ智也くん、このブログの「AdvancedMathBench」って何？数学の証明を評価するベンチマークなんだって？
うん、そう。LLMがどれだけ高度な数学の証明を生成したり、検証したりできるかを測るためのベンチマークスイートだよ。
へー、でもなんでそんなの必要なん？普通の数学の問題を解くのとは違うの？
違うんだ。普通の問題は答えが数値だったりするけど、証明は論理の連鎖で正しさを示す必要がある。LLMはまだそこが苦手で、ちゃんと評価する仕組みが不足してたんだよね。
なるほどね。で、このベンチマークはどうやってできてるの？
二つに分かれてて、一つはProverBenchっていう証明生成用で245問。学部レベルと博士資格試験レベルがある。もう一つはVerifierBenchで、モデルが生成した証明888件と専門家の正解をセットにして、証明の検証能力を評価するんだ。
888件も！それって全部人間がチェックしたの？大変そう…
いや、自動検証パイプラインを使ってる。証明の正誤だけでなく、どこが間違ってるかまで詳細に評価できるように設計されてるんだ。
自動でそこまでできるんだ！すごいね。で、実際にLLMはどれくらいできたの？
最良のモデルでも学部レベルで64.5点、博士資格試験で48.9点、検証のF1スコアは65.1だった。かなり低い。高度な証明の生成と検証はまだ難しいってことだね。
えー、そんなに低いんだ。でもそれって逆に言うと、これから伸びしろがあるってこと？
そうだね。このベンチマークが標準化されれば、今後のモデルの改善を定量的に追えるようになる。研究の進展に役立つと思う。
でもさ、証明の検証って人間でも難しいよね。このベンチマークの限界とかはあるの？
ああ、問題は数学の全分野をカバーしてるわけじゃないし、自動検証の精度にも限界がある。あと、証明のスタイルや表現の多様性までは評価しきれてない。
ふーん、まだまだ課題はあるんだね。でも、これでLLMが数学の証明をちゃんとできるようになったら、将来は私の宿題もやってくれるかな？
その前に、まずは自分で証明を書けるようになったほうがいいと思うよ。