Repository navigation
feat: add ProofNet benchmark - #1114
Merged
Merged
Conversation
Binds the ProofNet Lean4 formal-proof test split (186 theorems) to the existing
`math_formal_lean` resources server and `simple_agent` (single-turn, matching
NeMo-Skills' evaluation protocol). No new server code.
## Includes
- `benchmarks/proofnet/` — benchmark config, `prepare.py`, `prompts/default.yaml`,
README.
- Data source: deepseek-ai/DeepSeek-Prover-V1.5 `proofnet.jsonl` (186 test
theorems; 185 `valid` rows dropped), pinned to commit
`2c4ba9119eef74d0d611f494261b2c5bae98c69a`.
- Prompt: zero-shot port of `lean4/formal-proof`. Upstream template has a
`{examples}` placeholder that renders to an empty string when
`examples_type=None` (the NeMo-Skills default), so dropping it here is
equivalent for zero-shot evaluation.
- Per-row schema `{name, split, header, informal_prefix, formal_statement, goal}`
— byte-identical to Skills' `nemo_skills/dataset/proofnet/test.jsonl` (verified
via sorted-diff across all 186 rows).
- `prepare.py` asserts `len(test_rows) == 186` to catch upstream drift.
## Test plan
- `ng_prepare_benchmark` writes 186-row JSONL byte-identical to Skills' upstream.
- `ng_list_benchmarks` shows `proofnet` bound to
`proofnet_math_formal_lean_simple_agent` with `num_repeats=32`.
- Existing `resources_servers/math_formal_lean` tests unaffected (mocked sandbox).
- `pre-commit run --files benchmarks/proofnet/**/*` clean.
End-to-end pass@k baseline deferred to a follow-up run with a Lean sandbox;
same pipeline as the miniF2F port (#1111) which was validated against Skills.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Signed-off-by: Stephen Ge <stephen.ge@gmail.com>
Two changes on top of the original port: 1. Prompt switch: drop the zero-shot port of `lean4/formal-proof` in favor of the shared `lean4_formal_proof_deepseek_prover_v2` prompt used by miniF2F (#1111) and MOBench (#1113). Intentionally differs from NeMo-Skills' upstream choice for ProofNet; per user request, all four ported Lean benchmarks should use the same prompt for consistency. 2. Move to shared location: reference `benchmarks/prompts/lean4_formal_proof_deepseek_prover_v2.yaml` (merged in via main) and delete the benchmark-local `prompts/default.yaml`. Data output and server binding unchanged; only prompt rendering differs at rollout time. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> Signed-off-by: Stephen Ge <stephen.ge@gmail.com>
gwarmstrong
approved these changes
Apr 23, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Binds the ProofNet Lean4 formal-proof test split (186 theorems) to the existing
math_formal_leanresources server andsimple_agent(single-turn, matching NeMo-Skills' evaluation protocol). No new server code.Includes
benchmarks/proofnet/— benchmark config,prepare.py,prompts/default.yaml, README.proofnet.jsonlpinned to commit2c4ba9119eef74d0d611f494261b2c5bae98c69a. 186 test theorems; 185validrows dropped.lean4/formal-proof.yaml. The upstream template has a{examples}few-shot placeholder that renders to an empty string whenexamples_type=None(NeMo-Skills default), so dropping it here is equivalent for zero-shot evaluation.{name, split, header, informal_prefix, formal_statement, goal}— byte-identical to Skills'nemo_skills/dataset/proofnet/test.jsonl(verified via sorted-diff across all 186 rows).prepare.pyassertslen(test_rows) == 186to catch upstream drift.Test plan
ng_prepare_benchmarkwrites 186-row JSONL byte-identical to NeMo-Skills' upstream.ng_list_benchmarksshowsproofnetbound toproofnet_math_formal_lean_simple_agentwithnum_repeats=32.resources_servers/math_formal_leantests unaffected (mocked sandbox).pre-commit run --files benchmarks/proofnet/**/*clean.End-to-end pass@k baseline deferred to a follow-up run with a Lean sandbox; this PR is a pure binding — same pipeline as the miniF2F port (#1111) which was validated against NeMo-Skills.
🤖 Generated with Claude Code