cmu-l3/reuf2f の ReuF2F は、学部研究プログラムの論文や報告書にある猜想および明示された未解決問題を Lean に形式化し、コーディングエージェントを評価するベンチマークである。このリポジトリにはそのような問題が 244 件収録されている。個別のバージョンやリリース情報は示されていない。
モデルは、未解決問題が記載された Lean ファイルを基に、theorem を証明するか、その完全な否定を証明する patch を生成する。回答は形式化された証明を検査して判定されるため、評価は自然言語の回答との類似度ではなく、問題が証明されたかどうかに基づく。実行ハーネスは Docker、固定の elan ツールチェーン、Python 3.11 以上を使用する。結果は run_id・モデル名・instance_id ごとにキャッシュされ、同じ run_id で再実行すると保存済みのレポートが再利用される。
評価では信頼できない Lean コードを実行するため、認証情報を置かない使い捨てホストを使用するよう警告がある。共有イメージは約 15GB、実行環境には少なくとも 60GB の空き容量が必要で、イメージは linux/amd64 向けのため M シリーズ Mac ではエミュレーションで実行される。ライセンスは NOASSERTION と記載されており、リポジトリ自体にも性能比較の結果は示されていないため、エージェント間の性能差はこの資料だけでは判断しにくい。