1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
|
from __future__ import annotations
import asyncio
import json
from gap_pipeline.clients import ScriptedClient
from gap_pipeline.paper_pipeline import PaperKernelPipeline, PaperPipelineConfig
from gap_pipeline.prompts import JUDGE_SYSTEM_PROMPT
from gap_pipeline.store import RunStore
def _dag() -> dict:
return {
"nodes": [
{
"node_id": "n1",
"claim": "(a-1)^2 >= 0",
"dependencies": [],
},
{
"node_id": "n2",
"claim": "a+1/a >= 2",
"dependencies": ["n1"],
},
],
"terminal_node_id": "n2",
}
def _methods() -> dict:
return {
"nodes": [
{
"node_id": "n1",
"method_label": "use nonnegativity of a square",
},
{
"node_id": "n2",
"method_label": "expand and divide by a positive quantity",
},
]
}
def _replacement() -> dict:
return {
"changes": [
{
"slot_id": "slot1",
"source_node_id": "n1",
"description": "positive equality value",
"original_value": "1",
"replacement_value": "2",
"guard_condition": "replacement is positive",
"guard_justification": "2 is positive",
}
],
"closure_statement": "No undeclared changes.",
}
def _diffused() -> dict:
return {
"nodes": [
{
"node_id": "n1",
"dependencies": [],
"method_label": "use nonnegativity of a square",
"instantiated_claim": "(x-2)^2 >= 0",
"justification": "squares are nonnegative",
},
{
"node_id": "n2",
"dependencies": ["n1"],
"method_label": "expand and divide by a positive quantity",
"instantiated_claim": "x+4/x >= 4",
"justification": "expand and divide by x>0",
},
],
"terminal_node_id": "n2",
"terminal_answer": "4",
}
def _variant(suffix: str = "") -> dict:
return {
"question": f"Let x>0. Prove that x+4/x >= 4.{suffix}",
"solution": (
"[n1] Since (x-2)^2 >= 0. "
"[n2] Expand and divide by x>0 to obtain x+4/x >= 4."
),
"node_order": ["n1", "n2"],
"terminal_answer": "4",
}
def _accept() -> dict:
return {
"verdict": "accept",
"step_by_step_check": "n1 is valid; n2 is valid",
"blocking_issues": "",
"patch_suggestion": "",
}
def _reject() -> dict:
return {
"verdict": "reject",
"step_by_step_check": "n1 is valid; n2 needs a wording correction",
"blocking_issues": "the terminal wording is ambiguous",
"patch_suggestion": "clarify the terminal wording",
}
def test_five_stage_repair_uses_prior_bundle_and_appendix_judge(
tmp_path,
item,
) -> None:
proposer = ScriptedClient(
{
f"{item.item_id}.stage1.dag": _dag(),
f"{item.item_id}.stage2.methods": _methods(),
f"{item.item_id}.stage3.replacement": [
_replacement(),
_replacement(),
],
f"{item.item_id}.stage4.diffusion": [
_diffused(),
_diffused(),
],
f"{item.item_id}.stage5.render": [
_variant(),
_variant(" The requested bound is explicit."),
],
}
)
judges = []
for judge_id in range(1, 6):
first = _reject() if judge_id == 1 else _accept()
judges.append(
ScriptedClient(
{f"{item.item_id}.verify": [first, _accept(), _accept()]}
)
)
run_root = tmp_path / "run"
result = asyncio.run(
PaperKernelPipeline(
proposer=proposer,
judges=judges,
store=RunStore(run_root, item.item_id),
config=PaperPipelineConfig(
proposer_model="scripted",
judge_model="scripted",
),
).run(item)
)
assert result.status == "accepted"
assert [row.pass_streak_after for row in result.iterations] == [0, 1, 2]
assert result.iterations[0].bundle_sha256 != result.iterations[1].bundle_sha256
assert result.iterations[1].bundle_sha256 == result.iterations[2].bundle_sha256
calls_dir = run_root / "items" / item.item_id / "calls"
repair_stage_calls = [
json.loads(
(
calls_dir
/ f"{item.item_id}.stage{stage}.{name}.v02.json"
).read_text()
)
for stage, name in [
(3, "replacement"),
(4, "diffusion"),
(5, "render"),
]
]
assert "PREVIOUS REPLACEMENT PLAN" in repair_stage_calls[0]["user_prompt"]
assert "PREVIOUS DIFFUSED PROOF" in repair_stage_calls[1]["user_prompt"]
assert "PREVIOUS RENDERED VARIANT" in repair_stage_calls[2]["user_prompt"]
assert all(
"the terminal wording is ambiguous" in call["user_prompt"]
for call in repair_stage_calls
)
judge_calls = sorted(calls_dir.glob(f"{item.item_id}.verify.*.json"))
assert len(judge_calls) == 15
assert not any(".a1." in path.name for path in judge_calls)
first_judge_call = json.loads(judge_calls[0].read_text())
assert first_judge_call["system_prompt"] == JUDGE_SYSTEM_PROMPT
assert "METHOD-LABEL SEQUENCE (abstract plan):" in first_judge_call["user_prompt"]
assert "SOURCE PROOF DAG:" not in first_judge_call["user_prompt"]
|
