Datasetpublic

ByteDance-Seed/EdgeBench

Overview EdgeBench is a benchmark of 134 real-world tasks for evaluating how autonomous AI agents learn from real-world environments. Instead of measuring one-shot performance, EdgeBench places agents in executable task environments with realistic, multi-level feedback and lets them iterate for 12+ hours per task — tracking the full trajectory of improvement, not just the final score. We publicly release 51 tasks… See the full description on the dataset page: https://huggingface.co/datasets/ByteDance-Seed/EdgeBench.

sourceHugging Facecc-by-4.0updated 2mo agoView on Hugging Face

84likes7.5kdownloads

rootpfr_formalization.json

pfr_formalization.json32 linesDownload Raw Back to root

1{2  "task_id": "pfr_formalization",3  "name": "Pfr Formalization",4  "category": "Formal Math & Theorem Proving",5  "base_image": "lean_4",6  "platform": "linux/amd64",7  "internet": false,8  "cwd": "/home/workspace/",9  "submit_paths": [10    "se-bmk-intern/pfr"11  ],12  "submit_exclude": [13    "se-bmk-intern/pfr/.lake"14  ],15  "work": {16    "image_tag": "508bdc207859",17    "specs_dir": null,18    "agent_query": "You are a lean4 expert, now your task is to finish **all** sorries in this folder. Pay no attention to anything outside this folder. There are many sorries but do not be afraid as we value minor progress and the time is abundant. Try to do some easy problems and accumulate scores each round. Before you submit, run a `lake build` to verify the changes locally - if the build failed, no score will be given. Also, do not modify the signature of existing lemma/theorem/def as these changes will not pass the judge evaluation. Finally, we check the axioms transitively, finishing a theorem without completeing precedent lemma will not count."19  },20  "judge": {21    "image_tag": "9ed39cf76869",22    "eval_cmd": "cd /home/workspace/se-bmk-intern/pfr && cp -r /home/workspace/judge/se-bmk-intern/pfr/.lake . && cp /home/workspace/judge/se-bmk-intern/pfr/lake-manifest.json . && lake build && cp /home/workspace/judge/se-bmk-intern/pfr/ListDeclAxiom.lean . && cd /home/workspace/judge/se-bmk-intern && python3 eval_lean.py --baseline-repo /home/workspace/judge/se-bmk-intern/pfr --current-repo /home/workspace/se-bmk-intern/pfr",23    "eval_timeout": 2400,24    "parser": "structured_json",25    "rescale": {26      "kind": "linear",27      "lower": 0.0,28      "upper": 1.029    }30  }31}32