REVIEW 4 major objections 4 minor 3 cited by
Automated proof verification can be sharply improved by rejecting a solution whenever any of several parallel verifier reviews finds a flaw, especially when the proof is split into fine-grained chunks.
Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →
T0 review · deepseek-v4-flash
2026-08-03 19:57 UTC pith:S4JN5KZ4
load-bearing objection A simple any-negative verification workflow that mostly holds up on human-labeled benchmarks; the circular QiuZhen-Bench labels and an over-strong annotation-error claim are the real weaknesses, not the core method. the 4 major comments →
Pessimistic Verification for Open Ended Math Questions
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
The paper's central claim is that pessimistic aggregation—declaring a proof incorrect if any of several independent verifier passes flags a flaw—substantially improves the error-detection ability of LLM verifiers on open-ended math proofs. The progressive variant, which starts with a whole-proof review and then iteratively subdivides surviving proofs into smaller chunks with focused chunk-level prompts, is the most efficient and effective: it filters out easily detected errors early and drills into fine-grained steps, using at most 2^n−1 checks per proof. Experiments across contest-level benchmarks and multiple model sizes show that this approach raises true-negative rate and balanced F1 for
What carries the argument
The key machinery is the any-negative rejection rule: multiple parallel verification queries are run on the same proof, and the proof is judged false if any query reports an error, with the verifier required to explain detected flaws. Progressive pessimistic verification adds multi-scale proof decomposition: a whole-proof pass, then iterative halving of the proof into chunks with a focused chunk-review prompt, pruning any proof once an error is flagged. This combination turns verification into a scalable, parallelizable error-search process rather than a single holistic judgment.
Load-bearing premise
The central assumption is that false alarms on correct proofs are rare enough, and the parallel reviews varied enough, that requiring all reviews to pass does not systematically reject many genuinely correct proofs.
What would settle it
Take a set of proofs known to be correct—for example, mechanically verified or hand-checked by experts—run progressive pessimistic verification on them, and count how many are rejected; if a substantial fraction fail, the method's reported gains in error detection are largely driven by false positives rather than real improvements.
If this is right
- Simple pessimistic verification scales steadily with the number of reviews, while majority voting shows almost no improvement on verification tasks.
- Progressive pessimistic verification achieves the best accuracy-efficiency tradeoff, surpassing long chain-of-thought at matched token budgets on contest-level math.
- Gains in balanced F1 and true-negative rate appear across a range of model sizes, with weaker models showing larger improvements at a cost of some true-positive rate.
- If the annotation-error finding holds, current benchmarks systematically underestimate verifiers, and relabeling a sample of proofs could reveal even larger gains for state-of-the-art models.
Where Pith is reading between the lines
- The any-negative rule is a general design principle: it should transfer to code review, formal proof validation, and other settings where false positives are cheap relative to missed errors; a natural extension is to calibrate the number of reviews against the cost of false rejection.
- Whether the gains persist when reviews are not truly independent is testable: conditioning reviews on each other's verdicts or sharing reasoning context may change the aggregation rule, and the paper does not model this correlation.
- If benchmark annotations are as noisy as the case study suggests, the field may benefit more from re-annotating existing datasets than from further verifier design alone.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper proposes pessimistic verification: instead of averaging multiple LLM verifier judgments, a solution is rejected if any parallel review reports an error. Three variants are introduced — simple (repeated whole-proof reviews), vertical (chunkwise review), and progressive (iterative subdivision with pruning). The authors report consistent balanced-F1 gains over single-pass verification across three benchmarks (IMO-GradingBench, Hard2Verify, and a new QiuZhen-Bench), at token costs below extended long-CoT on several models. They further argue via a small case study that many verifier false negatives on strong models are actually correct detections of annotation errors, implying their performance is underestimated. A verification-guided solving workflow is also applied to IMO 2025 and MathArena Apex 2025. The central contribution is a cheap, scalable, model-agnostic method for open-ended math-proof verification.
Significance. If the central claim holds, the paper addresses a real bottleneck in math LLM pipelines: detecting errors in open-ended proofs without formal verification. The proposed progressive pessimistic workflow is simple, parallelizable, and shows consistent directional gains across multiple model families, with code and dataset released. That combination is practically valuable for verifier-guided RL and math agents. The paper also correctly identifies error detection (TNR) as the main source of verifier weakness, consistent with prior work. However, the evaluation has two structural weaknesses: (i) QiuZhen-Bench labels are produced by the same method family under test, and (ii) the only evidence that strong-model TPR loss is 'largely an illusion' is a small, single-annotator manual review. Because the headline claims of underestimation and superiority over long CoT rest on these labels and on this re-annotation, the strength of the empirical contribution is currently conditional on independent human re-annotation and uncertainty quantification.
major comments (4)
- [§3.1 and §3.4 (QiuZhen-Bench labeling and underestimation claim)] The QiuZhen-Bench evaluation labels are generated by 'GPT-5 with progressive@3/6' — i.e., with a progressive pessimistic verification workflow, the exact method family whose performance the paper measures. Reporting F1 gains on these labels and then arguing the method is underestimated is therefore circular to a substantial degree. The only independent evidence against real TPR loss is Table 1's manual review of 48 false-negative cases (20 for GPT-5, 13 for GPT-5-mini, 15 for Qwen3-30B-A3B), with no inter-annotator reliability and an explicitly subjective 'Minor' category. A load-bearing claim such as 'most false negatives are annotation errors' needs a pre-registered coding rubric, multiple expert annotators, agreement statistics, and ideally re-labeling of the full evaluation subset — not just 48 cherry-picked FN cases.
- [§3.3, Figures 1 and 6 (Uncertainty quantification)] All headline comparisons are response-level balanced F1 on 300-sample subsets, with no error bars, confidence intervals, or paired statistical tests. At n=300, a balanced-F1 difference of 3–5 points is well within binomial sampling noise (approximate standard error of ±3–4 points at F1≈0.8). The paper's repeated claim of 'consistently improves' across models should be supported by paired bootstrap intervals or McNemar-type tests over the same responses, especially for the long-CoT comparison, where the token-cost weighting (input/8 + output) is also a proprietary pricing assumption rather than a measured runtime.
- [§2 (Pessimistic aggregation assumption)] The method's validity hinges on the claim that 'pessimistic verification does not significantly affect the verifier's stability on positive examples' (Section 2). This is asserted, not measured. The paper provides no estimate of review-level false-positive correlation on the same proof, or of the number of true-positive proofs that receive at least one spurious negative across n reviews. The authors' own results for Qwen3-30B-A3B and smaller models show substantial TPR degradation, so the stability claim cannot be assumed for stronger models; it must be demonstrated on a sample of human-verified positive proofs. Without this, the F1 gain could simply reflect an aggressive rejection bias.
- [§3.4, Table 1 (Re-labeling as evidence)] The manual FN review conflates mathematical correctness with rigor/style. Table 1 counts cases like Case 4 (a typo with a fixable proof) and Case 6 (a verifier misunderstanding) in ways that depend on subjective interpretation, and the paper's own 'Case 4: our comment' admits the proof is easily fixed. The conclusion that the original IMO-GradingBench labels are wrong is extrapolated from a very small, non-randomly sampled set of FN cases. The claim that stronger models' TPR loss is 'largely an illusion' is therefore not established by the data presented. This is load-bearing because the paper uses it to argue that the measured balanced-F1 gain understates the method's true performance.
minor comments (4)
- [Abstract and §3.3] 'Surpasses ... long CoT' is stated in the abstract, but Figure 1's x-axis is 'equivalent output tokens' using GPT-5-mini pricing (input/8 + output). This equivalence is not a neutral efficiency metric across models and should be reported alongside wall-clock or raw token counts.
- [§3.1] The text says 'we constantly use the same prompt and workflow setting across all these dataset,' yet QiuZhen-Bench labels are produced using a progressive@3/6 workflow, which is not the same single-pass evaluation setting used for the other benchmarks. Clarify the distinction between label generation and evaluation.
- [Throughout] Typos and inconsistent formatting: 'drasticly', 'comparion', 'fron' (Appendix A.1), and 'QiuZhenBench' vs 'QiuZhen-Bench'. Also, several formulas use 'e0' where '≠' is intended (e.g., Case 5 in Appendix A.3). These should be cleaned up.
- [Figure 3] The majority-voting comparison would be more convincing with numeric values and the same token budget axes as Figure 1; currently no error bars or tabulated scores support the 'majority voting has almost no effect' conclusion.
Circularity Check
QiuZhen-Bench labels are produced by the method under test, and the 'underestimated' claim rests on subjective re-labeling of the method's own false negatives; external benchmarks keep the core finding from being fully circular.
specific steps
-
self definitional
[Section 3.1 (Datasets and settings); Section 3.4 (Case study)]
"We randomly selected a subset of 300 problems, had them answered by GPT-5-mini, and used GPT-5 with progressive@3/6 for labeling. This subset can be used to evaluate the performance of weaker models. ... it supports the validity of using GPT-5 to annotate QiuZhen-Bench."
QiuZhen-Bench's ground-truth labels are generated by GPT-5 running progressive@3/6, i.e. by the same pessimistic-verification workflow family whose performance the paper measures. Evaluating progressive pessimistic verification on this benchmark therefore measures agreement with the method's own outputs rather than with an independent standard. The paper then defends the validity of those GPT-5-generated labels by appealing to GPT-5's FN judgments in Section 3.4, forming a self-supporting loop. This does not force the results on IMO-GradingBench and Hard2Verify, which use human annotations.
-
other
[Section 3.4 (Case study), Table 1 and Appendix A.3]
"most of the FN cases produced by GPT-5-mini or stronger models under pessimistic verification did in fact identify real, critical errors in the proofs. ... Minor. If our verifier identified a typo or minor errors that can be easily fixed. In such cases, whether it should be judged as an error depends entirely on subjective criteria."
The paper's load-bearing claim that its TPR loss is 'largely an illusion caused by dataset annotation' is established by manually re-labeling the method's own false-negative cases using categories whose 'Minor' bucket the paper explicitly admits is subjective, and with no independent expert adjudication or inter-annotator reliability. The ground truth is thus revised based on the same verifier judgments that are being evaluated, so the conclusion that the method is underestimated is not derived from an external standard.
full rationale
The paper's central contribution is an empirical verification workflow, not a mathematical derivation; there is no equation-level chain that reduces a prediction to a fitted input. The main independent support comes from IMO-GradingBench and Hard2Verify, both described as human/expert annotated, so the core claim that pessimistic verification improves balanced F1 has real external content. However, two related steps are partially circular. First, QiuZhen-Bench, one of the three evaluation datasets, is labeled by GPT-5 with progressive@3/6, which is the same method family under test; evaluating the method on those labels measures self-consistency rather than independent correctness. Second, the paper's 'our method is underestimated' argument relies on a small, subjective manual re-classification of the method's own false negatives, with the paper itself stating that 'Minor' judgments 'depend entirely on subjective criteria.' The self-citation to the authors' prior pessimistic-verification work (Liu et al., 2025) is not load-bearing: the new variants and evaluations stand on their own experiments. Overall, the central finding is not forced by definition, but the benchmark-label loop and subjective re-annotation introduce a genuine partial circularity that prevents a clean 0-2 score.
Axiom & Free-Parameter Ledger
free parameters (4)
- n (progressive iterations) =
3
- l (minimum chunk split length) =
6
- temperature =
1.0
- reasoning_effort =
medium
axioms (4)
- domain assumption Parallel verifier judgments are sufficiently conditionally independent, and false alarms on correct proofs are rare enough, that any-negative rejection improves balanced F1.
- domain assumption Human annotations on IMO-GradingBench and Hard2Verify are treated as ground truth for the main comparisons.
- ad hoc to paper GPT-5 + progressive@3/6 labels for QiuZhen-Bench are valid ground truth.
- domain assumption The selected 300-sample subsets are representative of the original benchmarks.
invented entities (1)
-
QiuZhen-Bench
no independent evidence
read the original abstract
Automatic verification is a critical component in building math-solving agents and reinforcement learning, yet it often falls short in generalizability, performance, and cost-efficiency. Identifying that the primary bottleneck of verification lies in error detection capability, we propose pessimistic verification, a paradigm of agentic workflows that rejects a solution if any of multiple parallel verifiers identifies a flaw. We further introduce progressive pessimistic verification, which employs fine-grained proof decomposition to significantly enhance verification accuracy and efficiency. Our approach surpasses the performance and token efficiency of extended long chain-of-thought (long CoT) and mainstream verification workflows, crucially, our analysis reveals that existing benchmarks underestimate its effectiveness on stronger models due to inherent annotation errors. To further validate the effectiveness of our method, we applied a verification-based solving workflow on the IMO 2025 and MathArena Apex 2025 datasets, where the workflow with progressive pessimistic verification exhibits remarkable improvements in both efficiency and accuracy on highly challenging contest-level math problems with state-of-the-art models. Code is available at https://github.com/THUNLP-MT/pverify.
Figures
Forward citations
Cited by 3 Pith papers
-
Pseudo-Formalization for Automatic Proof Verification
Pseudo-Formalization decomposes proofs into self-contained natural language modules for independent LLM-based Block Verification, outperforming LLM-as-judge baselines on olympiad and research math benchmarks while rel...
-
AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification
A 245-problem advanced proof benchmark plus 888 expert-labeled trajectories shows frontier LLMs remain far from reliable advanced proof generation and verification.
-
Pseudo-Formalization for Automatic Proof Verification
Pseudo-Formalization decomposes natural language proofs into modular blocks for independent LLM verification via Block Verification, outperforming LLM-as-judge baselines on error detection in olympiad and research mat...
Reference graph
Works this paper leans on
-
[1]
The provided content is indeed a math problem and its corresponding solution, rather than unrelated material supplied by mistake
-
[2]
URLhttp://arxiv.org/abs/2507.15855. arXiv:2507.15855 [cs]. Thomas Kwa, Ben West, Joel Becker, Amy Deng, Katharyn Garcia, Max Hasin, Sami Jawhar, Megan Kinniment, Nate Rush, Sydney Von Arx, Ryan Bloom, Thomas Broadley, Haoxing Du, Brian Goodrich, Nikola Jurkovic, Luke Harold Miles, Seraphina Nix, Tao Lin, Neev Parikh, David Rein, Lucas Jun Koba Sato, Hjalm...
arXiv 2025
-
[3]
URLhttp://arxiv.org/abs/2505.09388. arXiv:2505.09388 [cs]. Tianyu Yu, Bo Ji, Shouli Wang, Shu Yao, Zefan Wang, Ganqu Cui, Lifan Yuan, Ning Ding, Yuan Yao, Zhiyuan Liu, Maosong Sun, and Tat-Seng Chua. RLPR: Extrapolating RLVR to General Domains without Verifiers, June 2025. URL http://arxiv.org/abs/2506.18254. arXiv:2506.18254 [cs]. Lianmin Zheng, Wei-Lin ...
Pith/arXiv arXiv 2025
-
[4]
The hypotheses (conditions) and conclusions of any theorems used are correctly matched and applied
-
[5]
The solution relies only on the conditions given in the problem and does not introduce any additional assumptions to obtain the conclusion. Consistency and error-severity policy (important): - If only minor, easily fixable issues exist (e.g., small algebraic slips later corrected, notational typos, superficial formatting), treat the solution as correct ov...
-
[6]
The solution actually derives the conclusion required by the original problem
-
[7]
Every step of calculation and formula derivation in the solution is correct
-
[9]
Thus, D=D ∗ is the required point inside the angle, different from A
**Conclusion**: Since the problem stipulates that α̸= 60◦, we must have D∗ ̸=A . Thus, D=D ∗ is the required point inside the angle, different from A. The constant angle is calculated to beθ=π−2α. **2. Detailed Solution** Step 1: Setup and Coordinate System. Let α= ̸ XYZ. We are given 0 <α<π/ 2 and α̸=π/ 3. We set up a coordinate system in the complex pla...
-
[10]
The chunk's reasoning and calculations adhere to mathematical correctness
-
[11]
Any theorems used in the chunk match their hypotheses and conclusions
-
[12]
The chunk does not rely on assumptions not justified by the problem or earlier proven steps. Consistency and error-severity policy (important): 15 - If only minor, easily fixable issues exist (e.g., small algebraic slips later corrected, notational typos, superficial formatting), treat the chunk as correct overall but briefly note such issues. - If there ...
-
[13]
Let α= ̸ XYZ
**Setup**: We establish a coordinate system with Y at the origin. Let α= ̸ XYZ. The rays − →YX and − →YZ correspond to the positive real axis and the ray at angle α, respectively. A=a is inside the angle. B=b and C=ce iα (b> 0, c> 0). 2. **Analysis of Configurations ( SA)**: We analyze the condition ̸ BAC=α . This geometric condition implies the directed ...
-
[15]
rsin(ϕ 1 −α) =k(−bsin(− 2α) + rsin(ϕ 1 −2α)).rsin(ϕ 1 −α) =k(bsin 2α−rsin(ϕ 1 −2α))
rsin(ϕ 1 −α) +k(bsin(− 2α)−rsin(ϕ 1 − 2α)) =0. rsin(ϕ 1 −α) =k(−bsin(− 2α) + rsin(ϕ 1 −2α)).rsin(ϕ 1 −α) =k(bsin 2α−rsin(ϕ 1 −2α)). We rewrite this using sin(x) =−sin(−x) . −rsin(α−ϕ 1) =k(bsin 2α+rsin( 2α− ϕ1)). Let C1 =rsin(α−ϕ 1). Since 0 <α−ϕ 1 <π/ 2, C1 > 0. Let C2 =sin 2α. Since 0 < 2α<π , C2 > 0. Let C3 =rsin( 2α−ϕ 1). Since 0 <ϕ 1 <α and α<π/ 2, w...
-
[16]
This yields two possibilities for D: D=A (i.e., d=a) orC 3 −C 2d−C 1e−iα =0
(a−d)[(C 3 −C 2d)−C 1e−iα ] =0. This yields two possibilities for D: D=A (i.e., d=a) orC 3 −C 2d−C 1e−iα =0. We are looking for D̸=A . Let D∗ be the second solution, with coordinate d∗. C2d∗ = C3 −C 1e−iα.d ∗ = C3−C1e−iα C2 . If D=D ∗, then (b−d ∗) is a common factor of P(b) and Q(b). P(b) =p 1(b−d ∗). Q(b) =−C 2(b−d ∗)(b−b 0). X(b) = p1 −C2(b−b0) . For b...
-
[17]
Then α=π/ 2 −π/ 6 =π/ 3 (60 degrees)
ϕ1 =π/ 6 (30 degrees). Then α=π/ 2 −π/ 6 =π/ 3 (60 degrees). So D∗ =A if and only if α= 60◦ andAis on the angle bisector (ϕ 1 =α/2). Step 7: Conclusion. The problem states that ̸ XYZ̸= 60◦ (i.e., α̸=π/ 3). Therefore, the condition for D∗ =A is not met, so D∗ ̸=A . We have shown that D∗ is strictly inside the angle ̸ XYZ. We have shown that forD=D ∗, the a...
-
[18]
Legendre symbol
f(x) = 1 for all x∈Z . 3. f(x) =x for all x∈Z . 4. f(x) = 0 ifxis even 1 ifxis odd . 5. f(x) = 0 ifx≡0(mod 3) 1 ifx≡1(mod 3) −1 ifx≡2(mod 3) . Case 2: review from gpt-5 The chunk makes critical, unjustified assumptions when classifying the non-constant solutions. In particular: • In Step 4.3 (k= 2), it assumes Z= 2Z (all even numbers are zeros) and ...
2024
-
[19]
N((m−1) 2,m 2)< ⌊2 log2 m⌋ ∑ j=3 2 j (m−1) 2 j −1 ≤ ⌊2 log2 m⌋ ∑ j=3 2 3 (m−1) −1/3 The number of terms in the summation is⌊2 log 2 m⌋ −2<2 log2 m
Assuming m−1≥1, we have(m−1) 2 j −1 ≤(m−1) −1/3. N((m−1) 2,m 2)< ⌊2 log2 m⌋ ∑ j=3 2 j (m−1) 2 j −1 ≤ ⌊2 log2 m⌋ ∑ j=3 2 3 (m−1) −1/3 The number of terms in the summation is⌊2 log 2 m⌋ −2<2 log2 m. N((m−1) 2,m 2)<(2 log 2 m)· 2 3 (m−1) −1/3 = 4 log2 m 3(m−1) 1/3 Asm→∞, this upper bound tends to 0. To see this formally: limm→∞ 4 log2 m 3(m−1) 1/3 =limm→∞ 4 ...
-
[20]
From Claim 1, the interval ((m− 1)2, m2) contains no perfect powers. This means that for any integer n in the interval Im = [(m− 1)2, m2 − 1], the set of perfect powers less than or equal to n is the same as the set of perfect powers less than or equal to (m− 1)2. Thus, An has a constant value for all n∈I m. Let this value be km =A (m−1)2
-
[21]
this sum → 0 ⇒N= 0 for large m
From Claim 2, the inequality 2 m− 1 >A (m−1)2 =k m holds. The length of the interval Im is (m2 − 1)−(m− 1)2 + 1 = 2m− 1. So, for m≥M , the length of the intervalI m is strictly greater thank m. We are looking for an integer n such that An |(n+ 2024). For any m≥M , we seek an n∈I m satisfying km |(n+ 2024). This is equivalent to finding an n in the range (...
2024
-
[22]
We define R(x) =L −1(Sk(L(x))) =S k(x+ 4)− 4
The degree of ˜R(y) =S k(y) is 2k. We define R(x) =L −1(Sk(L(x))) =S k(x+ 4)− 4. The degree ofR(x)is 2 k. Step 3: Assembling the final solution We are now ready to define P(x) and Q(x). - Let Q(x) =Q 0(x) = 1 4 x2 + 2x+ 3. - Let R(x) be constructed with k= 10, so ˜R(y) =S 10(y) =S ◦10(y), and R(x) = S10(x+4)−4. - LetP(x) =R(P 0(x)) =R( 1 4 x2 +x). 27 Let’...
-
[23]
This satisfies deg(Q)≥2
**Degree of Q(x)**: deg(Q) =deg(Q 0) =2. This satisfies deg(Q)≥2
-
[24]
deg(P0) =2
**Degree of P(x)**: The degree of P(x) is the product of the degrees of R(x) and P0(x). deg(P0) =2. deg(R) =deg(S 10) =210 = 1024. deg(P) =deg(R)·deg(P 0) = 1024 · 2 = 2048. We need deg(P)≥ 2024. Our value 2048 satisfies this condition. (If we needed an even higher degree, we could just choose a larger k. For instance, k= 11 would give deg(P) =4096.)
2048
-
[25]
Our construction of R(x) ensures it commutes with Q0(x), so this identity holds for all inputs, and thus for all real numbersx
**The functional equation**: As shown in Step 2, the choice P(x) =R(P 0(x)) and Q(x) =Q 0(x) reduces the equation (∗) to R(Q0(P0(x))) =Q 0(R(P0(x))) . Our construction of R(x) ensures it commutes with Q0(x), so this identity holds for all inputs, and thus for all real numbersx. We have successfully constructed polynomials P(x) and Q(x) that satisfy all th...
2024
-
[103]
The maximum value of h(k) for k∈[ 0, 120] is many orders of magnitude smaller than 270
270 = (210)7 ≈( 103)7 = 1021. The maximum value of h(k) for k∈[ 0, 120] is many orders of magnitude smaller than 270. Therefore, we have shown that for any graph G, M(f)≤max 0≤k≤120 (120−k+g(k))≪2 70. This shows thatM(f)≤2 70. Case 6: review from qwen3-30b-a3b <verification>false</verification> The solution incorrectly claims that the function f correspon...
-
[2023]
URLhttp://arxiv.org/abs/2306.05685. arXiv:2306.05685 [cs]. Yuxin Zuo, Kaiyan Zhang, Shang Qu, Li Sheng, Xuekai Zhu, Biqing Qi, Youbang Sun, Ganqu Cui, Ning Ding, and Bowen Zhou. TTRL: Test-Time Reinforcement Learning, April 2025. URLhttp://arxiv.org/abs/2504.16084. arXiv:2504.16084 [cs]. 12 A Appendix A.1 Details in QiuZhen-Bench QiuZhen-Bench is a datase...
Pith/arXiv arXiv 2025
-
[2025]
Rajarshi Haldar and Julia Hockenmaier
Multimodal large language model. Rajarshi Haldar and Julia Hockenmaier. Rating Roulette: Self-Inconsistency in LLM- As-A-Judge Frameworks, October 2025. URL http://arxiv.org/abs/2510.27106. arXiv:2510.27106 [cs]. Yichen Huang and Lin F. Yang. Gemini 2.5 Pro Capable of Winning Gold at IMO 2025, July
Pith/arXiv arXiv 2025
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.