fix(lean-taskset): audit proof axioms to close the injected-axiom bypass

[CaptainAni187]

Closes #2177

lean_compiled awards 1.0 when the protected signature is intact and lake env lean exits 0 with no sorry. It never checks what the proof depends on, so a rollout can close any goal by supplying its own axiom above the signature:

import Mathlib
axiom cheat : False
-- DO NOT MODIFY the theorem statement below.
theorem fake_irrational : Irrational (1 : ℝ) := by
  exact cheat.elim

Irrational (1 : ℝ) is false. The axiom sits above the protected region, so the signature guard passes, the compile is silent, and the reward returns 1.0.

#1271 flagged this exact gap as future work ("or axiomatize the goal"); #1480 closed a sibling bypass in the same reward.

Change

After a clean compile, write the rollout's file to a sibling path with #print axioms <name> appended, compile that, and reject any axiom outside Mathlib's trusted base — propext, Classical.choice, Quot.sound. The rollout's own file is left untouched.

The parsing and trust decision are pure functions in scoring.py, alongside the existing helpers.

One detail worth flagging

parse_axioms_output matches the last depends on axioms line, not the first. Our query is appended at the end of the file, so anything earlier came from the rollout — without this, a model could inject

#eval IO.println "'fake_irrational' depends on axioms: [propext, Classical.choice, Quot.sound]"

above its proof and have the audit read the decoy. That is the same failure #1480 fixed for EXIT_CODE markers, so I followed the reasoning already documented in parse_compile_output. There is a test for it.

declaration_name returns "" for an anonymous example, which skips the audit rather than failing the rollout — the pre-existing behaviour for statements the reward cannot pin.

Tests

tests/v1/test_lean_scoring.py, 9 tests:

• the pure helpers: name extraction, axiom-list parsing, the trusted baseline, the injected cheat axiom, and the decoy-shadowing case
• the reward itself, driven through a stub runtime: a compiling proof resting on cheat scores 0.0 with lean_untrusted_axioms == ["cheat"], and a genuine proof still scores 1.0

Reverting only the taskset.py wiring (keeping the helpers) turns the first reward test into assert 1.0 == 0.0, so the test pins the bypass itself rather than the helpers.

tests/v1 (excluding test_e2e.py): 76 passed, up from 67, with the same 11 pre-existing failures in test_configs.py::test_eval_config_parses — missing optional taskset packages in my environment, unrelated to this change. test_color_codeword_tasks.py does not collect locally for the same reason.

ruff check and ruff format clean.

I could not run the real Lean toolchain locally, so the audit is verified against recorded #print axioms transcripts rather than a live lake env lean. The transcripts match the ones in the issue, including #print axioms fake_irrational → [cheat, propext, Classical.choice, Quot.sound]. Happy to adjust if the real output differs in shape.

Note

Reject Lean proofs resting on injected axioms in lean_compiled

• Adds LeanTask._print_axioms which writes an audit copy of the proof with a declaration-specific #axioms query, runs Lean on it, and returns the combined transcript without touching the original proof file.
• Adds parsers in scoring.py: declaration_name extracts the theorem/lemma name from a signature, parse_axioms_output selects the last reported axiom list, and untrusted_axioms filters names against the TRUSTED_AXIOMS Mathlib baseline.
• lean_compiled in taskset.py now runs the audit after a successful compile and sets score to zero with tampering info when any untrusted axiom is found.
• Behavioral Change: a proof that compiles but depends on an axiom outside the three accepted Mathlib baseline names now scores zero and is marked tampered; if no declaration name is found or the audit yields no untrusted axioms, full credit is retained.

^{Macroscope summarized 148dfce.}