From 3885ca3b224e81d6016160f0ffe2a97156394de6 Mon Sep 17 00:00:00 2001 From: findalexli Date: Tue, 3 Nov 2026 21:58:04 -0800 Subject: [PATCH] smt_solver: report an evaluator crash as invalid --- edgebench/tasks/smt_solver/NOTES.md | 9 +++++++++ .../environment/workspace/scripts/evaluate.py | 2 +- edgebench/tasks/smt_solver/judge/parse_result.py | 11 +++++++++-- edgebench/tasks/smt_solver/judge/run.sh | 2 +- .../smt_solver/judge/smt_judge/scripts/evaluate.py | 2 +- edgebench/tasks/smt_solver/task.toml | 2 +- 6 files changed, 22 insertions(+), 6 deletions(-) diff --git a/edgebench/tasks/smt_solver/NOTES.md b/edgebench/tasks/smt_solver/NOTES.md index 6de487e4..3ecf74e7 100644 --- a/edgebench/tasks/smt_solver/NOTES.md +++ b/edgebench/tasks/smt_solver/NOTES.md @@ -53,6 +53,15 @@ shared host, two runs each. Raw score; 0..100 in brackets. Deterministic rows match exactly, including per-logic counts. The timed rows differ by a few cases near the 60 s limit; the old-new difference of means is smaller than either side's own spread. +## Changes + +### 1.1.0 + +If the evaluator exits with anything but 0 or 2 and leaves no score file, the result is now invalid, +not a valid 0. A build failure, a missing `solve` and a preflight rejection stay a valid 0 (the missing +`solve` exit changes from 1 to 2 to keep that). No score changes unless the evaluator crashed. Source, +Deviations and Regression summary describe 1.0.0. Issue: https://github.com/ByteDance-Seed/EdgeBench/issues/42 + ## Known issues Kept as in v1, so scores stay comparable. Fixing any of them changes scores and bumps `version`. diff --git a/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py b/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py index a43158c8..2c6d6667 100644 --- a/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py +++ b/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py @@ -898,7 +898,7 @@ def main(): solver = os.path.abspath(args.solver) if not os.path.isfile(solver) or not os.access(solver, os.X_OK): print(f"Error: solver is not executable: {args.solver}", file=sys.stderr) - sys.exit(1) + sys.exit(2) if not os.path.isdir(args.benchmarks): print(f"Error: benchmark directory does not exist: {args.benchmarks}", file=sys.stderr) sys.exit(1) diff --git a/edgebench/tasks/smt_solver/judge/parse_result.py b/edgebench/tasks/smt_solver/judge/parse_result.py index af176e94..a4f10075 100644 --- a/edgebench/tasks/smt_solver/judge/parse_result.py +++ b/edgebench/tasks/smt_solver/judge/parse_result.py @@ -1,7 +1,14 @@ -# v1's /tmp/sebench_parse_result.py (heredoc in judge.eval_cmd), verbatim except that the -# score file path comes from argv[1] instead of the fixed /tmp/smt_hidden_score.json. +# v1's /tmp/sebench_parse_result.py (heredoc in judge.eval_cmd), except that the score file path comes +# from argv[1] instead of the fixed /tmp/smt_hidden_score.json, and that an evaluator crash is invalid. +# argv[2] = evaluate.py's exit status, empty if it did not run. 2 = it rejected the submission. import json, pathlib, sys p = pathlib.Path(sys.argv[1]) +status = sys.argv[2] if len(sys.argv) > 2 else '' +if not p.exists() and status not in ('', '0', '2'): + print('>>>>> Start Structured Result') + print(json.dumps({'valid': False, 'score': None, 'summary': 'evaluator exited with status {} before writing a score file'.format(status), 'details': [], 'metrics': {}})) + print('>>>>> End Structured Result') + sys.exit(0) raw = json.loads(p.read_text()) if p.exists() else {'final_score': 0.0, 'logic_summary': {}} raw_score = float(raw.get('final_score', 0.0) or 0.0) score = raw_score / 100.0 if raw_score > 1.0 else raw_score diff --git a/edgebench/tasks/smt_solver/judge/run.sh b/edgebench/tasks/smt_solver/judge/run.sh index 7daec838..9df734fb 100644 --- a/edgebench/tasks/smt_solver/judge/run.sh +++ b/edgebench/tasks/smt_solver/judge/run.sh @@ -17,7 +17,7 @@ LOG=$(mktemp) T=$(mktemp -d) ( -cd /home/workspace/smt_solver && rm -rf benchmarks hidden_benchmarks scripts expected_answers.json selection_manifest.json hidden_score.json public_score.json; chmod +x build.sh solve; build_status=0; ./build.sh >"$T/smt_build.out" 2>"$T/smt_build.err" || build_status=$?; if [ "$build_status" -eq 0 ]; then python3 /home/workspace/smt_judge/scripts/evaluate.py --solver ./solve --benchmarks /home/workspace/smt_judge/hidden_benchmarks --expected /home/workspace/smt_judge/hidden_benchmarks/expected_answers.json --manifest /home/workspace/smt_judge/hidden_benchmarks/selection_manifest.json --timeout 60 --parallel 16 --perturb --perturb-salt hidden-sebench --submission-root /home/workspace/smt_solver --output "$T/smt_hidden_score.json" >"$T/smt_eval.out" 2>"$T/smt_eval.err"; eval_status=$?; else eval_status=$build_status; fi; if [ -f "$T/smt_build.out" ]; then cat "$T/smt_build.out"; fi; if [ -f "$T/smt_build.err" ]; then cat "$T/smt_build.err"; fi; if [ -f "$T/smt_eval.out" ]; then cat "$T/smt_eval.out"; fi; if [ -f "$T/smt_eval.err" ]; then cat "$T/smt_eval.err"; fi; python3 /judge/parse_result.py "$T/smt_hidden_score.json" +cd /home/workspace/smt_solver && rm -rf benchmarks hidden_benchmarks scripts expected_answers.json selection_manifest.json hidden_score.json public_score.json; chmod +x build.sh solve; build_status=0; ./build.sh >"$T/smt_build.out" 2>"$T/smt_build.err" || build_status=$?; if [ "$build_status" -eq 0 ]; then python3 /home/workspace/smt_judge/scripts/evaluate.py --solver ./solve --benchmarks /home/workspace/smt_judge/hidden_benchmarks --expected /home/workspace/smt_judge/hidden_benchmarks/expected_answers.json --manifest /home/workspace/smt_judge/hidden_benchmarks/selection_manifest.json --timeout 60 --parallel 16 --perturb --perturb-salt hidden-sebench --submission-root /home/workspace/smt_solver --output "$T/smt_hidden_score.json" >"$T/smt_eval.out" 2>"$T/smt_eval.err"; eval_status=$?; evaluator_status=$eval_status; else eval_status=$build_status; evaluator_status=; fi; if [ -f "$T/smt_build.out" ]; then cat "$T/smt_build.out"; fi; if [ -f "$T/smt_build.err" ]; then cat "$T/smt_build.err"; fi; if [ -f "$T/smt_eval.out" ]; then cat "$T/smt_eval.out"; fi; if [ -f "$T/smt_eval.err" ]; then cat "$T/smt_eval.err"; fi; python3 /judge/parse_result.py "$T/smt_hidden_score.json" "$evaluator_status" ) > "$LOG" 2>&1 EXIT_CODE=$? cat "$LOG" diff --git a/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py b/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py index a43158c8..2c6d6667 100755 --- a/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py +++ b/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py @@ -898,7 +898,7 @@ def main(): solver = os.path.abspath(args.solver) if not os.path.isfile(solver) or not os.access(solver, os.X_OK): print(f"Error: solver is not executable: {args.solver}", file=sys.stderr) - sys.exit(1) + sys.exit(2) if not os.path.isdir(args.benchmarks): print(f"Error: benchmark directory does not exist: {args.benchmarks}", file=sys.stderr) sys.exit(1) diff --git a/edgebench/tasks/smt_solver/task.toml b/edgebench/tasks/smt_solver/task.toml index 4b295bfa..f64c86d2 100644 --- a/edgebench/tasks/smt_solver/task.toml +++ b/edgebench/tasks/smt_solver/task.toml @@ -4,7 +4,7 @@ name = "Smt Solver" category = "Combinatorial Optimization" language = "Python" description = "Build an SMT solver from scratch for four quantifier-free theories (uninterpreted functions, linear real and integer arithmetic, and their combination). External SMT solvers are forbidden; model witnesses are independently validated." -version = "1.0.0" +version = "1.1.0" status = "migrated" [environment]