arXiv subjects

Junyu Guo

Publications and source records attributed to Junyu Guo.

13 recordsLinked to original sources

arXiv2026

A Solution to Iima--Yoshino Problem 2.3

Iima and Yoshino asked for an ideal $I$ in $S=k[x_1,x_2,\ldots]$, with $\operatorname{deg} x_i=i$, and a monomial order such that $S/I\cong k[x_i:i\equiv\pm1\pmod5], \operatorname{in}(I)=(x_i^2,x_ix_{i+1}:i\geq1).$ We construct such an ideal and monomial order over every field $k$ of characteristic different from $5$ containing an element $c$ with $c^2+c=1$. The ideal has an explicit infinite homogeneous reduced Gr\"obner basis. A five-periodic syzygy derived from a pentagon identity proves that all basis relations belong to $I$ and supplies standard representations for the non-coprime critical pairs. Triangular elimination establishes the graded quotient isomorphism. Together, the quotient and initial ideal descriptions yield the partition form of the first Rogers-Ramanujan identity. In each weighted degree, a perfect matching in the support of the normal-form matrix gives a bijection between the two partition classes. We formalize the complex specialization in Lean 4 using Mathlib and our set-based theory of infinite Gr\"obner bases, including the reduced basis, the graded quotient isomorphism, and the partition-matching theorem.

math.AC↗

arXiv2026

MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4

We present MechGeo, a Mathlib native agentic framework that jointly addresses faithful autoformalization and certified proof construction for Euclidean geometry. In this framework, GeoFormalizer represents informal problems in GeoIR, deterministically translates them into Lean 4, and iteratively repairs candidate statements using structural diagnostics and semantic evaluation. GeoProver constructs geometric proof plans, derives intermediate lemmas, and selectively algebraizes suitable subgoals through a library verified in Lean. Singular or SymPy may generate algebraic certificates, but all resulting proofs and counterexamples are checked by Lean's kernel. Experiments across seven LLM backbones show substantial improvements in autoformalization, particularly for models with weaker direct translation performance. On 43 historical IMO geometry problems, GeoFormalizer generates formal statements that GeoProver proves in 29 cases; for the remaining 14, it constructs counterexamples verified in Lean and proves all repaired statements after expert correction. Together with IMO 2026 Problem 2, this yields, to the best of our knowledge, the largest reported collection of automated, kernel-checked Lean proofs for IMO geometry problems. On the 14 geometry statements in LEAP's Lean-IMO-Bench, MechGeo proves 12 for the first time, formally refutes the remaining two, and proves both repaired statements. These results establish counterexample guided diagnosis, geometric reasoning, and certified symbolic computation as a practical foundation for trustworthy formal geometry.

cs.AI↗

arXiv2026

Formalizing Wu-Ritt Method in Lean 4

We formalize the Wu-Ritt characteristic set method for the triangular decomposition of polynomial systems in the Lean 4 theorem prover. Our development includes the core algebraic notions of the method, such as polynomial initials, orders, pseudo-division, pseudo-remainders with respect to a polynomial or a triangular set, and standard and weak ascending sets. On this basis, we formalize algorithms for computing basic sets, characteristic sets, and zero decompositions, and prove their termination and correctness. In particular, we formalize the well-ordering principle relating a polynomial system to its characteristic set and verify that zero decomposition expresses the zero set of the original system as a union of zero sets of triangular sets away from the zeros of the corresponding initials. This work provides a machine-checked verification of Wu-Ritt's method in Lean 4 and establishes a foundation for certified polynomial system solving and geometric theorem proving.

math.AC↗

arXiv2026

Automated Tactics for Polynomial Reasoning in Lean 4

Applying Gr\"obner basis theory to concrete problems in Lean 4 remains difficult since the current formalization of multivariate polynomials is based on a non-computable representation and is therefore not suitable for efficient symbolic computation. As a result, computing Gr\"obner bases directly inside Lean is impractical for realistic examples. To address this issue, we propose a certificate-based approach that combines external computer algebra systems, such as SageMath or SymPy, with formal verification in Lean 4. Our approach uses a computable representation of multivariate polynomials in Lean to import and verify externally generated Gr\"obner basis computations. The external solver carries out the main algebraic computations, while the returned results are verified inside Lean. Based on this method, we develop automated tactics that transfer polynomial data between Lean and the external system and certify the returned results. These tactics support tasks such as remainder verification, Gr\"obner basis checking, ideal equality, and ideal or radical membership. This work provides a practical way to integrate external symbolic computation into Lean 4 while preserving the reliability of formal proof.

cs.LO↗

arXiv2026

LLMs Should Express Uncertainty Explicitly

Large language models (LLMs) often produce confident yet incorrect answers, which can lead to risky failures in real-world applications. We study whether post-training can make a model's self-assessment explicit: when the model is uncertain, can it be trained to signal so within its own response? A central design question is where in the response this signal should be exposed -- during reasoning, while the answer is still being formed, or at the end, once the answer has been produced. We study both. For end-of-reasoning self-assessment, we train the model to verbalize a confidence score for its response, with the aim of high confidence on correct answers and low confidence on incorrect ones. For during-reasoning self-assessment, we train the model to emit the marker whenever its current reasoning state appears unreliable. Across factual reasoning tasks, both forms sharply reduce overconfident errors while improving answer quality, and both can be used as triggers for retrieval augmented generation (RAG) to improve the final response. We further analyze their internal mechanisms: end-of-reasoning verbalized confidence sharpens a confidence-related structure already present in the pretrained model, whereas during-reasoning emission teaches the model to mark high-risk reasoning steps, with parameter changes concentrated in the model's late layers.

cs.LG↗

arXiv2026

Differential Mental Disorder Detection with Psychology-Inspired Multimodal Stimuli

Differential diagnosis of mental disorders remains a fundamental challenge in real-world clinical practice, where multiple conditions often exhibit overlapping symptoms. However, most existing public datasets are developed under single-disorder settings and rely on limited data elicitation paradigms, restricting their ability to capture disorder-specific patterns. In this work, we investigate differential mental disorder detection through psychology-inspired multimodal stimuli, designed to elicit diverse emotional, cognitive, and behavioral responses grounded in findings from experimental psychology. Based on this paradigm, we collect a large-scale multimodal mental health dataset (MMH) covering depression, anxiety, and schizophrenia, with all diagnostic labels clinically verified by licensed psychiatrists. To effectively model the heterogeneous signals induced by diverse elicitation tasks, we further propose a paradigm-aware multimodal framework that leverages inter-disorder differences prior knowledge as prompt-guided semantic descriptions to capture task-specific affective and interaction contexts for multimodal representation learning in the new differential mental disorder detection task. Extensive experiments show that our framework consistently outperforms existing baselines, underscoring the value of psychology-inspired stimulus design for differential mental disorder detection.

cs.MM↗

arXiv2026

Formalizing Gr\"obner Basis Theory in Lean

We present a formalization of Gr\"obner basis theory in Lean 4, built on top of Mathlib's infrastructure for multivariate polynomials and monomial orders. Our development covers the core foundations of Gr\"obner basis theory, including polynomial division with remainder, Buchberger's criterion, and the existence and uniqueness of reduced Gr\"obner bases. We develop the theory uniformly for polynomial rings indexed by arbitrary types, enabling the treatment of Gr\"obner bases in rings with infinitely many variables. Furthermore, we connect the finite and infinite settings by showing that infinite-variable reduced Gr\"obner bases can be characterized via reduced Gr\"obner bases on finite-variable subrings through monomial-order embeddings and filter-based limit constructions.

math.AC↗

arXiv2025

StyleBench: Evaluating thinking styles in Large Language Models

Structured reasoning can improve the inference performance of large language models (LLMs), but it also introduces computational cost and control constraints. When additional reasoning structure helps, and when it instead reduces efficiency or robustness, remains poorly understood. We propose StyleBench, where we study reasoning structure as a capacity-constrained design choice rather than a fixed inference recipe. We evaluate five representative reasoning styles: Chain-of-Thought, Tree-of-Thought, Algorithm-of-Thought, Sketch-of-Thought, and Chain-of-Draft across five reasoning tasks and 15 open-source LLMs ranging from 270M to 120B parameters. We find that greater structural complexity improves accuracy only in limited regimes defined by task demands and model capacity. Search-based styles help on open-ended combinatorial problems but fail on smaller models, while concise styles achieve large efficiency gains on structured tasks without sacrificing performance. We also identify systematic failure modes in smaller models, including premature guessing and weak adherence to reasoning-control instructions. To study adaptive reasoning control, we further compare supervised and reinforcement-based strategy selection on Qwen-7B-Instruct. Supervised fine-tuning collapses to shallow style preferences, whereas GRPO learns stronger adaptive control and improves downstream performance. Together, these results clarify when structured reasoning is useful, when it is wasteful, and why learning to choose a reasoning strategy is itself a challenging inference problem, we open source the benchmark in https://github.com/JamesJunyuGuo/Style_Bench.

cs.LG↗

arXiv2025

Don't Trade Off Safety: Diffusion Regularization for Constrained Offline RL

Constrained reinforcement learning (RL) seeks high-performance policies under safety constraints. We focus on an offline setting where the agent has only a fixed dataset -- common in realistic tasks to prevent unsafe exploration. To address this, we propose Diffusion-Regularized Constrained Offline Reinforcement Learning (DRCORL), which first uses a diffusion model to capture the behavioral policy from offline data and then extracts a simplified policy to enable efficient inference. We further apply gradient manipulation for safety adaptation, balancing the reward objective and constraint satisfaction. This approach leverages high-quality offline data while incorporating safety requirements. Empirical results show that DRCORL achieves reliable safety performance, fast inference, and strong reward outcomes across robot learning tasks. Compared to existing safe offline RL methods, it consistently meets cost limits and performs well with the same hyperparameters, indicating practical applicability in real-world scenarios.

cs.LG↗

arXiv2024

HS-FPN: High Frequency and Spatial Perception FPN for Tiny Object Detection

The introduction of Feature Pyramid Network (FPN) has significantly improved object detection performance. However, substantial challenges remain in detecting tiny objects, as their features occupy only a very small proportion of the feature maps. Although FPN integrates multi-scale features, it does not directly enhance or enrich the features of tiny objects. Furthermore, FPN lacks spatial perception ability. To address these issues, we propose a novel High Frequency and Spatial Perception Feature Pyramid Network (HS-FPN) with two innovative modules. First, we designed a high frequency perception module (HFP) that generates high frequency responses through high pass filters. These high frequency responses are used as mask weights from both spatial and channel perspectives to enrich and highlight the features of tiny objects in the original feature maps. Second, we developed a spatial dependency perception module (SDP) to capture the spatial dependencies that FPN lacks. Our experiments demonstrate that detectors based on HS-FPN exhibit competitive advantages over state-of-the-art models on the AI-TOD dataset for tiny object detection.

cs.CV↗

arXiv2023

Reinforcement Learning for SBM Graphon Games with Re-Sampling

The Mean-Field approximation is a tractable approach for studying large population dynamics. However, its assumption on homogeneity and universal connections among all agents limits its applicability in many real-world scenarios. Multi-Population Mean-Field Game (MP-MFG) models have been introduced in the literature to address these limitations. When the underlying Stochastic Block Model is known, we show that a Policy Mirror Ascent algorithm finds the MP-MFG Nash Equilibrium. In more realistic scenarios where the block model is unknown, we propose a re-sampling scheme from a graphon integrated with the finite N-player MP-MFG model. We develop a novel learning framework based on a Graphon Game with Re-Sampling (GGR-S) model, which captures the complex network structures of agents' connections. We analyze GGR-S dynamics and establish the convergence to dynamics of MP-MFG. Leveraging this result, we propose an efficient sample-based N-player Reinforcement Learning algorithm for GGR-S without population manipulation, and provide a rigorous convergence analysis with finite sample guarantee.

cs.GT↗

arXiv2021

Automated Kidney Segmentation by Mask R-CNN in T2-weighted Magnetic Resonance Imaging

Despite the recent advances of deep learning algorithms in medical imaging, the automatic segmentation algorithms for kidneys in MRI exams are still scarce. Automated segmentation of kidneys in Magnetic Resonance Imaging (MRI) exams are important for enabling radiomics and machine learning analysis of renal disease. In this work, we propose to use the popular Mask R-CNN for the automatic segmentation of kidneys in coronal T2-weighted Fast Spin Eco slices of 100 MRI exams. We propose the morphological operations as post-processing to further improve the performance of Mask R-CNN for this task. With 5-fold cross-validation data, the proposed Mask R-CNN is trained and validated on 70 and 10 MRI exams and then evaluated on the remaining 20 exams in each fold. Our proposed method achieved a dice score of 0.904 and IoU of 0.822.

eess.IV↗

arXiv2020

RLCard: A Toolkit for Reinforcement Learning in Card Games

RLCard is an open-source toolkit for reinforcement learning research in card games. It supports various card environments with easy-to-use interfaces, including Blackjack, Leduc Hold'em, Texas Hold'em, UNO, Dou Dizhu and Mahjong. The goal of RLCard is to bridge reinforcement learning and imperfect information games, and push forward the research of reinforcement learning in domains with multiple agents, large state and action space, and sparse reward. In this paper, we provide an overview of the key components in RLCard, a discussion of the design principles, a brief introduction of the interfaces, and comprehensive evaluations of the environments. The codes and documents are available at https://github.com/datamllab/rlcard

cs.AI↗