SearcharxivSearch

arXiv subjects

Hanbin Yang

Publications and source records attributed to Hanbin Yang.

5 recordsLinked to original sources

Clarifying Before Reasoning: A Coq Prover with Structural Context

In this work, we investigate whether improving task clarity can enhance reasoning ability of large language models, focusing on theorem proving in Coq. We introduce a concept-level metric to evaluate task clarity and show that adding structured semantic context to the standard input used by modern LLMs, leads to a 1.85$\times$ improvement in clarity score (44.5\%~$\rightarrow$~82.3\%). Using the general-purpose model \texttt{DeepSeek-V3}, our approach leads to a 2.1$\times$ improvement in proof success (21.8\%~$\rightarrow$~45.8\%) and outperforms the previous state-of-the-art \texttt{Graph2Tac} (33.2\%). We evaluate this on 1,386 theorems randomly sampled from 15 standard Coq packages, following the same evaluation protocol as \texttt{Graph2Tac}. Furthermore, fine-tuning smaller models on our structured data can achieve even higher performance (48.6\%). Our method uses selective concept unfolding to enrich task descriptions, and employs a Planner--Executor architecture. These findings highlight the value of structured task representations in bridging the gap between understanding and reasoning.

cs.AI

FICA: Faster Inner Convex Approximation of Chance Constrained Grid Dispatch with Decision-Coupled Uncertainty

This paper proposes a Faster Inner Convex Approximation (FICA) method for solving power system dispatch problems with Wasserstein distributionally robust joint chance constraints (WJCC) and incorporating the modelling of the automatic generation control factors. The problem studied belongs to the computationally challenging class of WJCC with left-hand-side uncertainty (LHS-WJCC). By exploiting the special one-dimensional structure (even if only partially present) of the problem, the proposed FICA incorporates a set of strong valid inequalities to accelerate the solution process. We prove that FICA achieves the same optimality as the well-known conditional value-at-risk (CVaR) inner convex approximation method. Our numerical experiments demonstrate that the proposed FICA can yield 40x computational speedup compared to CVaR, and can even reach up to 500x speedup when the optimisation horizon exceeds 16 time steps. This speedup is achieved when only 50% of constraints in a WJCC have the one-dimensional structure. The approximation quality is numerically verified to be the same as CVaR, and the quality gap is below 1% when compared to the computationally demanding exact reformulation of the LHS-WJCC in most cases. We also discuss the applications of FICA in optimisation problems from other domains that (partially) exhibit the one-dimensional structure.

math.OC

Strengthened and Faster Linear Approximation to Joint Chance Constraints with Wasserstein Ambiguity

Many real-world decision-making problems have uncertain parameters in constraints. Wasserstein distributionally robust joint chance constraints (WDRJCC) offer a promising solution by explicitly guaranteeing the probability of the simultaneous constraint satisfaction. However, WDRJCC are computationally demanding, and practical applications often require more tractable approaches, especially for large-scale problems such as power system unit commitment problems and multilevel problems with chance constraints in lower levels. To address this, this paper proposes a convex inner-approximation for WDRJCC with right-hand-side uncertainties (RHS-WDRJCC). We propose a Strengthened and Faster Linear Approximation (SFLA) by strengthening an existing convex inner-approximation. This strengthening process reduces the number of constraints and tightens the feasible region for ancillary variables, leading to significant computational speedup. We prove that the proposed SFLA does not introduce extra conservativeness and can be less conservative compared to common approximations such as W-CVaR. We then extend the proposed SFLA to a more interpretable decision-making paradigm: robustness maximization, where the risk level and the Wasserstein radius are determined by maximizing solution robustness subject to a utility degradation limit. We discuss the connection between risk minimization and radius maximization as two formulations of robustness maximization, and show the advantage of radius maximization. In power system unit commitment, the proposed SFLA achieves up to 10x computational speedup compared to the strengthened and exact reformulation. In a bilevel strategic bidding problem where the exact reformulation is not applicable due to non-convexity, the proposed SFLA leads to 90x speedup than W-CVaR. In robustness maximization, the proposed SFLA demonstrated over 100x speedup.

math.OC

Multistage Stochastic Program for Mitigating Power System Risks under Wildfire Disruptions

The frequency of wildfire disasters has surged five-fold in the past 50 years due to climate change. Preemptive de-energization is a potent strategy to mitigate wildfire risks but substantially impacts customers. We propose a multistage stochastic programming model for proactive de-energization planning, aiming to minimize economic loss while accomplishing a fair load delivery. We model wildfire disruptions as stochastic disruptions with varying timing and intensity, introduce a cutting-plane decomposition algorithm, and test our approach on the RTS-GLMC test case. Our model consistently offers a robust and fair de-energization plan that mitigates wildfire damage costs and minimizes load-shedding losses, particularly when pre-disruption restoration is considered.

math.OC

Multi-period Power System Risk Minimization under Wildfire Disruptions

Natural wildfire becomes increasingly frequent as climate change evolves, posing a growing threat to power systems, while grid failures simultaneously fuel the most destructive wildfires. Preemptive de-energization of grid equipment is effective in mitigating grid-induced wildfires but may cause significant power outages during natural wildfires. This paper proposes a novel two-stage stochastic program for planning preemptive de-energization and solves it via an enhanced Lagrangian cut decomposition algorithm. We model wildfire events as stochastic disruptions with random magnitude and timing. The stochastic program maximizes the electricity delivered while proactively de-energizing components over multiple time periods to reduce wildfire risks. We use a cellular automaton process to sample grid failure and wildfire scenarios driven by realistic risk and environmental factors. We test our method on an augmented version of the RTS-GLMC test case in Southern California and compare it with four benchmark cases, including deterministic, wait-and-see, and robust optimization formulations as well as a comparison with prior wildfire risk optimization. Our method reduces wildfire damage costs and load-shedding losses, and our nominal plan is robust against uncertainty perturbation.

math.OC