diff --git a/docs/leaderboard.html b/docs/leaderboard.html index 3a74b1e..ae82c77 100644 --- a/docs/leaderboard.html +++ b/docs/leaderboard.html @@ -1,329 +1,365 @@ - - - - - - CLEVER Leaderboard - - - - -
-
-

🏆 CLEVER Leaderboard

-

Curated Lean Verified Code Generation Benchmark

- -
- - GitHub Repository - - - 📄 Paper - - - 📦 PyPI Package - -
-
- -
-
Legend
-
💚 Fully open-sourced method
-
💙 Partially open-sourced method
-
FS: Few-shot prompting with 1-2 examples
-
COPRA: Symbolic proof search agent [arXiv]
-
Compiled: Code is syntactically valid and type-checks
-
Proved: Proofs accepted by Lean's kernel
-
Pass@k-sec: Success rate within 600-second time budget (k=600)
-
# Proofs Generated: # Proofs generated while Spec and Impl Certification
-
- - -
- 🏆 End-to-End Performance Rankings -
-
- Complete pipeline success: specification certification + implementation certification (Pass@600-sec)
- Sorted based on first "End-to-End Code Generation" column, then "# Proofs Generated" -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
#ModelApproachEnd-to-End Code GenerationNote# Proofs Generated
1💙 Claude-3.7COPRA-enhanced1/161Problem 532/161 (spec) + 14/161 (impl) = 16/282
1💚 DeepSeek-R1Few-Shot1/161Problem 531/161 (spec) + 9/161 (impl) = 10/282
1💚 GPT OSS 20bCOPRA-enhanced1/161Problem 532/161 (spec) + 8/161 (impl) = 10/282
1💙 GPT-4oCOPRA-enhanced1/161Problem 533/161 (spec) + 6/161 (impl) = 9/282
1💙 GPT-4o miniFew-Shot1/161Problem 532/161 (spec) + 3 / 161 (impl) = 5/282
1💙 Claude-3.7Few-Shot1/161Problem 531/161 (spec) + 3/161 (impl) = 4/282
6💙 GPT-4oFew-Shot0/161-1/161 (spec) + 1/161 (impl) = 2/282
6💙 GPT-5 mini (For Code Generation) + Kimina Prover (For proofs)Few-Shot0/161-0/161 (spec) + 1/161 (impl) = 1/282
-
- - -
- 📊 Detailed Performance Breakdown -
-
- Pass@600-sec rates for specification certification and implementation certification
- (Compiled: syntactically valid and type-checks; Proved: proofs accepted by Lean's kernel)
- Sorted based on average compilation rates across both stages -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
ModelApproachSpec CertificationImpl CertificationEnd-to-End
CompiledProvedCompiledProved
Few-Shot Baseline
💙 GPT-4o miniFew-Shot82.609%1.242%83.230%1.863%0.621%
💙 Claude-3.7Few-Shot86.957%0.621%65.217%1.863%0.621%
💙 GPT-4oFew-Shot84.472%0.621%68.323%0.621%0%
💚 DeepSeek-R1Few-Shot71.42%0.621%60.870%5.559%0.621%
COPRA Baseline
💙 Claude-3.7COPRA-enhanced81.366%1.242%65.217%8.696%0.621%
💚 GPT OSS 20bCOPRA-enhanced78.261%1.242%65.839%4.969%0.621%
💙 GPT-4oCOPRA-enhanced76.398%1.863%68.323%3.727%0.621%
-
- - -
-
📝 Submission Guidelines
-

To add your results to this leaderboard:

-
    -
  1. Evaluate your approach using the CLEVER Python API
    2. -
  2. Document your methodology with a preprint or publication
    3. -
  3. Submit your results by contacting us with evaluation metrics and methodology details
    4. -
-

Contact: amitayush@utexas.edu

-
- - -
- - - + + + + + + CLEVER Leaderboard + + + + +
+
+

🏆 CLEVER Leaderboard

+

Curated Lean Verified Code Generation Benchmark

+ +
+ + GitHub Repository + + + 📄 Paper + + + 📦 PyPI Package + +
+
+ +
+
Legend
+
💚 Fully open-sourced method
+
💙 Partially open-sourced method
+
FS: Few-shot prompting with 1-2 examples
+
COPRA: Symbolic proof search agent [arXiv]
+
Compiled: Code is syntactically valid and type-checks
+
Proved: Proofs accepted by Lean's kernel
+
Pass@k-sec: Success rate within 600-second time budget (k=600)
+
# Proofs Generated: # Proofs generated while Spec and Impl Certification
+
+ + +
+ 🏆 End-to-End Performance Rankings +
+
+ Complete pipeline success: specification certification + implementation certification (Pass@600-sec)
+ Sorted based on first "End-to-End Code Generation" column, then "# Proofs Generated" +
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
#ModelApproachEnd-to-End Code GenerationNote# Proofs Generated
1💙 Claude CodeAgentic Proving (compiler-in-the-loop)59/161alt-spec-pipeline67/161 (spec) + 104/161 (impl) = 171/282
2💙 Claude-3.7COPRA-enhanced1/161Problem 532/161 (spec) + 14/161 (impl) = 16/282
2💚 DeepSeek-R1Few-Shot1/161Problem 531/161 (spec) + 9/161 (impl) = 10/282
2💚 GPT OSS 20bCOPRA-enhanced1/161Problem 532/161 (spec) + 8/161 (impl) = 10/282
2💙 GPT-4oCOPRA-enhanced1/161Problem 533/161 (spec) + 6/161 (impl) = 9/282
2💙 GPT-4o miniFew-Shot1/161Problem 532/161 (spec) + 3 / 161 (impl) = 5/282
2💙 Claude-3.7Few-Shot1/161Problem 531/161 (spec) + 3/161 (impl) = 4/282
7💙 GPT-4oFew-Shot0/161-1/161 (spec) + 1/161 (impl) = 2/282
7💙 GPT-5 mini (For Code Generation) + Kimina Prover (For proofs)Few-Shot0/161-0/161 (spec) + 1/161 (impl) = 1/282
+
+ + +
+ 📊 Detailed Performance Breakdown +
+
+ Pass@600-sec rates for specification certification and implementation certification
+ (Compiled: syntactically valid and type-checks; Proved: proofs accepted by Lean's kernel)
+ Sorted based on average compilation rates across both stages +
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
ModelApproachSpec CertificationImpl CertificationEnd-to-End
CompiledProvedCompiledProved
Agentic Proving Baseline
💙 Claude CodeAgentic Proving (compiler-in-the-loop)100.00%41.615%94.410%64.596%36.646%
Few-Shot Baseline
💙 GPT-4o miniFew-Shot82.609%1.242%83.230%1.863%0.621%
💙 Claude-3.7Few-Shot86.957%0.621%65.217%1.863%0.621%
💙 GPT-4oFew-Shot84.472%0.621%68.323%0.621%0%
💚 DeepSeek-R1Few-Shot71.42%0.621%60.870%5.559%0.621%
COPRA Baseline
💙 Claude-3.7COPRA-enhanced81.366%1.242%65.217%8.696%0.621%
💚 GPT OSS 20bCOPRA-enhanced78.261%1.242%65.839%4.969%0.621%
💙 GPT-4oCOPRA-enhanced76.398%1.863%68.323%3.727%0.621%
+
+

+ *See author remarks below for additional context on Claude Code's results, including an alternative generated-specification pipeline. +

+ + +
+
💬 Remarks
+ +
+ + +
+
📝 Submission Guidelines
+

To add your results to this leaderboard:

+
    +
  1. Evaluate your approach using the CLEVER Python API
    2. +
  2. Document your methodology with a preprint or publication
    3. +
  3. Submit your results by contacting us with evaluation metrics and methodology details
    4. +
+

Contact: amitayush@utexas.edu

+
+ + +
+ + + \ No newline at end of file