Spaces:
Runtime error
Runtime error
feat: benchmark
Browse files- benchmarks/run-formal-eval.ts +153 -0
- benchmarks/samples.jsonl +45 -0
- package.json +1 -0
benchmarks/run-formal-eval.ts
ADDED
|
@@ -0,0 +1,153 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
import "dotenv/config";
|
| 2 |
+
import { readFileSync, writeFileSync, existsSync } from "node:fs";
|
| 3 |
+
import { resolve } from "node:path";
|
| 4 |
+
import { coderAgent } from "../src/agents/coder/agent.ts";
|
| 5 |
+
|
| 6 |
+
// βββ Config ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 7 |
+
const FORMAL_EVAL_PATH =
|
| 8 |
+
process.env.FORMAL_EVAL_PATH ??
|
| 9 |
+
resolve("..", "formal-eval", "data", "FormalEval.jsonl");
|
| 10 |
+
|
| 11 |
+
const OUTPUT_PATH = process.env.BENCHMARK_OUTPUT ?? resolve("benchmarks", "samples.jsonl");
|
| 12 |
+
const SAMPLES_PER_TASK = Number(process.env.SAMPLES_PER_TASK ?? "1");
|
| 13 |
+
const SKIP_REVIEW = process.env.SKIP_REVIEW !== "false"; // skip review by default for speed
|
| 14 |
+
|
| 15 |
+
// βββ Types βββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 16 |
+
interface FormalEvalProblem {
|
| 17 |
+
task_id: string;
|
| 18 |
+
complexity: string;
|
| 19 |
+
description: string;
|
| 20 |
+
prompt: string;
|
| 21 |
+
canonical_solution: string;
|
| 22 |
+
test: string;
|
| 23 |
+
entry_point: string;
|
| 24 |
+
}
|
| 25 |
+
|
| 26 |
+
interface SampleOutput {
|
| 27 |
+
task_id: string;
|
| 28 |
+
completion: string;
|
| 29 |
+
}
|
| 30 |
+
|
| 31 |
+
// βββ Helpers βββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 32 |
+
|
| 33 |
+
function readProblems(path: string): FormalEvalProblem[] {
|
| 34 |
+
const content = readFileSync(path, "utf-8");
|
| 35 |
+
return content
|
| 36 |
+
.split("\n")
|
| 37 |
+
.filter((line) => line.trim())
|
| 38 |
+
.map((line) => JSON.parse(line));
|
| 39 |
+
}
|
| 40 |
+
|
| 41 |
+
/**
|
| 42 |
+
* Extrai a "completion" (body do contrato) a partir do contrato completo gerado.
|
| 43 |
+
* O FormalEval espera: prompt + completion = contrato completo.
|
| 44 |
+
* EntΓ£o precisamos remover tudo que jΓ‘ estΓ‘ no prompt.
|
| 45 |
+
*/
|
| 46 |
+
function extractCompletion(generatedContract: string, prompt: string): string {
|
| 47 |
+
// EstratΓ©gia 1: Se o contrato gerado contΓ©m o prompt exato, pegar o que vem depois
|
| 48 |
+
const promptTrimmed = prompt.trimEnd();
|
| 49 |
+
const idx = generatedContract.indexOf(promptTrimmed);
|
| 50 |
+
if (idx !== -1) {
|
| 51 |
+
return generatedContract.slice(idx + promptTrimmed.length);
|
| 52 |
+
}
|
| 53 |
+
|
| 54 |
+
// EstratΓ©gia 2: Encontrar a declaraΓ§Γ£o "contract <Name> {" e pegar o body
|
| 55 |
+
// O prompt sempre termina com "contract <Name> {\n"
|
| 56 |
+
const contractDeclMatch = prompt.match(/contract\s+(\w+)\s*\{?\s*$/m);
|
| 57 |
+
if (contractDeclMatch) {
|
| 58 |
+
const contractName = contractDeclMatch[1];
|
| 59 |
+
const pattern = new RegExp(`contract\\s+${contractName}\\s*\\{`);
|
| 60 |
+
const match = generatedContract.match(pattern);
|
| 61 |
+
if (match?.index !== undefined) {
|
| 62 |
+
const afterDecl = generatedContract.slice(match.index + match[0].length);
|
| 63 |
+
return afterDecl;
|
| 64 |
+
}
|
| 65 |
+
}
|
| 66 |
+
|
| 67 |
+
// EstratΓ©gia 3: Fallback β Tenta remover pragma + imports + declaraΓ§Γ£o atΓ© "{"
|
| 68 |
+
const lines = generatedContract.split("\n");
|
| 69 |
+
let bodyStart = 0;
|
| 70 |
+
for (let i = 0; i < lines.length; i++) {
|
| 71 |
+
if (lines[i].match(/contract\s+\w+.*\{/)) {
|
| 72 |
+
bodyStart = i + 1;
|
| 73 |
+
break;
|
| 74 |
+
}
|
| 75 |
+
}
|
| 76 |
+
return lines.slice(bodyStart).join("\n");
|
| 77 |
+
}
|
| 78 |
+
|
| 79 |
+
/**
|
| 80 |
+
* Adapta o prompt do FormalEval para ser interpretado pelo Coder Agent.
|
| 81 |
+
* Inclui instruΓ§Γ£o explΓcita para gerar apenas o body.
|
| 82 |
+
*/
|
| 83 |
+
function buildRequirements(problem: FormalEvalProblem): string {
|
| 84 |
+
return `Complete the following Solidity contract. Generate ONLY the contract body (state variables, functions, and closing brace "}").
|
| 85 |
+
Do NOT include the SPDX license, pragma, or contract declaration β they are already provided.
|
| 86 |
+
The code must compile with solc ^0.8.19.
|
| 87 |
+
|
| 88 |
+
Here is the contract declaration with its specification:
|
| 89 |
+
|
| 90 |
+
${problem.prompt}
|
| 91 |
+
|
| 92 |
+
IMPORTANT: Return ONLY the code that goes INSIDE the contract (after the opening brace). Include the closing "}" at the end.`;
|
| 93 |
+
}
|
| 94 |
+
|
| 95 |
+
// βββ Main ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 96 |
+
|
| 97 |
+
async function main() {
|
| 98 |
+
if (!existsSync(FORMAL_EVAL_PATH)) {
|
| 99 |
+
console.error(`FormalEval dataset not found at: ${FORMAL_EVAL_PATH}`);
|
| 100 |
+
console.error("Set FORMAL_EVAL_PATH env variable to the correct path.");
|
| 101 |
+
process.exit(1);
|
| 102 |
+
}
|
| 103 |
+
|
| 104 |
+
const problems = readProblems(FORMAL_EVAL_PATH);
|
| 105 |
+
console.log(`Loaded ${problems.length} problems from FormalEval`);
|
| 106 |
+
console.log(`Generating ${SAMPLES_PER_TASK} sample(s) per task...`);
|
| 107 |
+
console.log(`Output: ${OUTPUT_PATH}\n`);
|
| 108 |
+
|
| 109 |
+
const samples: SampleOutput[] = [];
|
| 110 |
+
let completed = 0;
|
| 111 |
+
|
| 112 |
+
for (const problem of problems) {
|
| 113 |
+
for (let s = 0; s < SAMPLES_PER_TASK; s++) {
|
| 114 |
+
const label = `[${problem.task_id}] (${problem.complexity}) sample ${s + 1}/${SAMPLES_PER_TASK}`;
|
| 115 |
+
console.log(`β ${label}: ${problem.description}`);
|
| 116 |
+
|
| 117 |
+
try {
|
| 118 |
+
const requirements = buildRequirements(problem);
|
| 119 |
+
const result = await coderAgent.invoke({ requirements: [requirements] });
|
| 120 |
+
|
| 121 |
+
const generated = result.contract;
|
| 122 |
+
const completion = extractCompletion(generated, problem.prompt);
|
| 123 |
+
|
| 124 |
+
samples.push({ task_id: problem.task_id, completion });
|
| 125 |
+
|
| 126 |
+
const hasErrors = result.compilationErrors.length > 0;
|
| 127 |
+
console.log(` β Done${hasErrors ? ` (with ${result.compilationErrors.length} compile errors)` : ""}`);
|
| 128 |
+
} catch (error) {
|
| 129 |
+
const msg = error instanceof Error ? error.message : String(error);
|
| 130 |
+
console.error(` β Failed: ${msg}`);
|
| 131 |
+
// Still emit an empty completion so FormalEval doesn't complain about missing tasks
|
| 132 |
+
samples.push({ task_id: problem.task_id, completion: "// generation failed\n}\n" });
|
| 133 |
+
}
|
| 134 |
+
|
| 135 |
+
completed++;
|
| 136 |
+
}
|
| 137 |
+
}
|
| 138 |
+
|
| 139 |
+
// Write JSONL output
|
| 140 |
+
const jsonl = samples.map((s) => JSON.stringify(s)).join("\n") + "\n";
|
| 141 |
+
writeFileSync(OUTPUT_PATH, jsonl, "utf-8");
|
| 142 |
+
|
| 143 |
+
console.log(`\n${"β".repeat(60)}`);
|
| 144 |
+
console.log(`Benchmark complete: ${completed} completions generated`);
|
| 145 |
+
console.log(`Output saved to: ${OUTPUT_PATH}`);
|
| 146 |
+
console.log(`\nTo evaluate, run:`);
|
| 147 |
+
console.log(` cd ../formal-eval && evaluate_formal_correctness ${resolve(OUTPUT_PATH)}`);
|
| 148 |
+
}
|
| 149 |
+
|
| 150 |
+
main().catch((err) => {
|
| 151 |
+
console.error("Fatal error:", err);
|
| 152 |
+
process.exit(1);
|
| 153 |
+
});
|
benchmarks/samples.jsonl
ADDED
|
@@ -0,0 +1,45 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
{"task_id":"FormalEval/0","completion":"// generation failed\n}\n"}
|
| 2 |
+
{"task_id":"FormalEval/0","completion":"// generation failed\n}\n"}
|
| 3 |
+
{"task_id":"FormalEval/0","completion":"// generation failed\n}\n"}
|
| 4 |
+
{"task_id":"FormalEval/1","completion":"// generation failed\n}\n"}
|
| 5 |
+
{"task_id":"FormalEval/1","completion":"// generation failed\n}\n"}
|
| 6 |
+
{"task_id":"FormalEval/1","completion":"// generation failed\n}\n"}
|
| 7 |
+
{"task_id":"FormalEval/2","completion":"// generation failed\n}\n"}
|
| 8 |
+
{"task_id":"FormalEval/2","completion":"// generation failed\n}\n"}
|
| 9 |
+
{"task_id":"FormalEval/2","completion":"// generation failed\n}\n"}
|
| 10 |
+
{"task_id":"FormalEval/3","completion":"// generation failed\n}\n"}
|
| 11 |
+
{"task_id":"FormalEval/3","completion":"// generation failed\n}\n"}
|
| 12 |
+
{"task_id":"FormalEval/3","completion":"// generation failed\n}\n"}
|
| 13 |
+
{"task_id":"FormalEval/4","completion":"// generation failed\n}\n"}
|
| 14 |
+
{"task_id":"FormalEval/4","completion":"// generation failed\n}\n"}
|
| 15 |
+
{"task_id":"FormalEval/4","completion":"// generation failed\n}\n"}
|
| 16 |
+
{"task_id":"FormalEval/5","completion":"// generation failed\n}\n"}
|
| 17 |
+
{"task_id":"FormalEval/5","completion":"// generation failed\n}\n"}
|
| 18 |
+
{"task_id":"FormalEval/5","completion":"// generation failed\n}\n"}
|
| 19 |
+
{"task_id":"FormalEval/6","completion":"// generation failed\n}\n"}
|
| 20 |
+
{"task_id":"FormalEval/6","completion":"// generation failed\n}\n"}
|
| 21 |
+
{"task_id":"FormalEval/6","completion":"// generation failed\n}\n"}
|
| 22 |
+
{"task_id":"FormalEval/7","completion":"// generation failed\n}\n"}
|
| 23 |
+
{"task_id":"FormalEval/7","completion":"// generation failed\n}\n"}
|
| 24 |
+
{"task_id":"FormalEval/7","completion":"// generation failed\n}\n"}
|
| 25 |
+
{"task_id":"FormalEval/8","completion":"// generation failed\n}\n"}
|
| 26 |
+
{"task_id":"FormalEval/8","completion":"// generation failed\n}\n"}
|
| 27 |
+
{"task_id":"FormalEval/8","completion":"// generation failed\n}\n"}
|
| 28 |
+
{"task_id":"FormalEval/9","completion":"// generation failed\n}\n"}
|
| 29 |
+
{"task_id":"FormalEval/9","completion":"// generation failed\n}\n"}
|
| 30 |
+
{"task_id":"FormalEval/9","completion":"// generation failed\n}\n"}
|
| 31 |
+
{"task_id":"FormalEval/10","completion":"// generation failed\n}\n"}
|
| 32 |
+
{"task_id":"FormalEval/10","completion":"// generation failed\n}\n"}
|
| 33 |
+
{"task_id":"FormalEval/10","completion":"// generation failed\n}\n"}
|
| 34 |
+
{"task_id":"FormalEval/11","completion":"// generation failed\n}\n"}
|
| 35 |
+
{"task_id":"FormalEval/11","completion":"// generation failed\n}\n"}
|
| 36 |
+
{"task_id":"FormalEval/11","completion":"// generation failed\n}\n"}
|
| 37 |
+
{"task_id":"FormalEval/12","completion":"// generation failed\n}\n"}
|
| 38 |
+
{"task_id":"FormalEval/12","completion":"// generation failed\n}\n"}
|
| 39 |
+
{"task_id":"FormalEval/12","completion":"// generation failed\n}\n"}
|
| 40 |
+
{"task_id":"FormalEval/13","completion":"// generation failed\n}\n"}
|
| 41 |
+
{"task_id":"FormalEval/13","completion":"// generation failed\n}\n"}
|
| 42 |
+
{"task_id":"FormalEval/13","completion":"// generation failed\n}\n"}
|
| 43 |
+
{"task_id":"FormalEval/14","completion":"// generation failed\n}\n"}
|
| 44 |
+
{"task_id":"FormalEval/14","completion":"// generation failed\n}\n"}
|
| 45 |
+
{"task_id":"FormalEval/14","completion":"// generation failed\n}\n"}
|
package.json
CHANGED
|
@@ -11,6 +11,7 @@
|
|
| 11 |
"start": "npm run build && node dist/index.js",
|
| 12 |
"server": "npm run build && node dist/server.js",
|
| 13 |
"dev:server": "npx tsx src/server.ts",
|
|
|
|
| 14 |
"postinstall": "patch-package"
|
| 15 |
},
|
| 16 |
"repository": {
|
|
|
|
| 11 |
"start": "npm run build && node dist/index.js",
|
| 12 |
"server": "npm run build && node dist/server.js",
|
| 13 |
"dev:server": "npx tsx src/server.ts",
|
| 14 |
+
"benchmark": "npx tsx benchmarks/run-formal-eval.ts",
|
| 15 |
"postinstall": "patch-package"
|
| 16 |
},
|
| 17 |
"repository": {
|