LeanGraphSearch/tests/test_reasoning_budget.py at main · PlusLabNLP/LeanGraphSearch · GitHub

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
from __future__ import annotations

import asyncio
import unittest
from unittest.mock import patch

from leansearchv2.reasoning.decompose import ProofPlan
from leansearchv2.reasoning.run import (
    Problem,
    ReasoningResult,
    _batch_search,
    run_reasoning_budgeted,
)
from leansearchv2.standard_client import ResultData, SearchResult


def _doc(name: str) -> SearchResult:
    return SearchResult(
        result=ResultData(
            module_name=["Mathlib", "Test"],
            kind="theorem",
            name=[name],
            signature="",
            type="True",
        ),
        distance=0.0,
    )


def _result(
    status: str,
    filtered: dict[str, list[SearchResult]] | None = None,
) -> ReasoningResult:
    return ReasoningResult(
        problem_id="p",
        status=status,
        big_loop_count=0,
        plan=ProofPlan(),
        filtered=filtered or {},
        filter_reasoning=f"filter-{status}",
        quality_reasoning=f"judge-{status}",
        entries=[],
    )


class ReasoningBranchBudgetTests(unittest.IsolatedAsyncioTestCase):
    async def test_graph_search_kwargs_are_forwarded_and_internal_pool_is_sliced(self) -> None:
        class Retriever:
            calls: list[dict] = []

            async def search(self, _query, **kwargs):
                self.calls.append(kwargs)
                return [_doc("A"), _doc("B"), _doc("C")]

        retriever = Retriever()
        result = await _batch_search(
            retriever,  # type: ignore[arg-type]
            ["query"],
            top_k=2,
            rerank=True,
            concurrency=1,
            search_kwargs={
                "graph_augment": True,
                "graph_final_top_k": 100,
                "rank_fusion": "qwen_ppr_zscore",
            },
        )

        self.assertEqual([doc.result.name[-1] for doc in result["query"]], ["A", "B"])
        self.assertEqual(retriever.calls[0]["top_k"], 2)
        self.assertEqual(retriever.calls[0]["graph_final_top_k"], 100)
        self.assertEqual(retriever.calls[0]["rank_fusion"], "qwen_ppr_zscore")

    async def test_first_good_cancels_unfinished_sibling(self) -> None:
        sibling_cancelled = asyncio.Event()

        async def fake_run(_problem, _retriever, llm, **_kwargs):
            if llm == "winner":
                return _result("good")
            try:
                await asyncio.Event().wait()
            except asyncio.CancelledError:
                sibling_cancelled.set()
                raise

        with patch("leansearchv2.reasoning.run.run_reasoning", side_effect=fake_run):
            result = await run_reasoning_budgeted(
                Problem("p", "theorem p : True"),
                object(),  # type: ignore[arg-type]
                ["winner", "sibling"],  # type: ignore[list-item]
            )

        self.assertEqual(result.winning_branch, 0)
        self.assertEqual(result.branch_statuses, ["good", "early_stop"])
        self.assertTrue(sibling_cancelled.is_set())
        self.assertEqual(result.to_dict()["branch_budget"], 2)

    async def test_two_failed_branches_pool_rank_votes(self) -> None:
        common = _doc("Common")
        left = _doc("Left")
        right = _doc("Right")
        branch_outputs = {
            "left": _result("fail", {"q": [common, left]}),
            "right": _result("fail", {"q": [common, right]}),
        }

        async def fake_run(_problem, _retriever, llm, **_kwargs):
            return branch_outputs[llm]

        with patch("leansearchv2.reasoning.run.run_reasoning", side_effect=fake_run):
            result = await run_reasoning_budgeted(
                Problem("p", "theorem p : True"),
                object(),  # type: ignore[arg-type]
                ["left", "right"],  # type: ignore[list-item]
                output_top_k=3,
            )

        self.assertIsNone(result.winning_branch)
        self.assertEqual(result.status, "fail")
        self.assertEqual(result.branch_statuses, ["fail", "fail"])
        self.assertEqual(len(result.result.filtered), 2)
        self.assertEqual(
            [doc_id for doc_id, _score, _doc in result.entries],
            [
                "Mathlib.Test::Common",
                "Mathlib.Test::Left",
                "Mathlib.Test::Right",
            ],
        )

    async def test_completed_sibling_keeps_real_status(self) -> None:
        async def fake_run(_problem, _retriever, _llm, **_kwargs):
            return _result("good")

        with patch("leansearchv2.reasoning.run.run_reasoning", side_effect=fake_run):
            result = await run_reasoning_budgeted(
                Problem("p", "theorem p : True"),
                object(),  # type: ignore[arg-type]
                ["first", "second"],  # type: ignore[list-item]
            )

        self.assertEqual(result.winning_branch, 0)
        self.assertEqual(result.branch_statuses, ["good", "good"])

    async def test_all_branch_errors_are_not_reported_as_success(self) -> None:
        async def fake_run(_problem, _retriever, llm, **_kwargs):
            raise ValueError(f"broken-{llm}")

        with patch("leansearchv2.reasoning.run.run_reasoning", side_effect=fake_run):
            with self.assertRaisesRegex(RuntimeError, "all reasoning branches errored"):
                await run_reasoning_budgeted(
                    Problem("p", "theorem p : True"),
                    object(),  # type: ignore[arg-type]
                    ["left", "right"],  # type: ignore[list-item]
                )


if __name__ == "__main__":
    unittest.main()