Searcharxiv⌕ Search

arXiv subjects

Donghoon Hyeon

Publications and source records attributed to Donghoon Hyeon.

13 recordsLinked to original sources
arXiv2026

SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization

Autoformalization translates informal mathematical theorems into code for proof assistants such as Lean. A central challenge is that current evaluation metrics can accept type-correct but misaligned statements or reject correct statements written in a different formulation. Inspired by Pass@$k$, we propose SA-Pass (*Semantic Alignment Pass*), which tests formal statements using auxiliary statements called *shadows* that characterize the intended statement. A generated statement receives full credit only when it compiles, implies each shadow (forward check), and is implied by their conjunction (backward check). We instantiate SA-Pass in ShadowBench, a Lean 4 full autoformalization benchmark of 178 postgraduate- to research-level problems spanning eight mathematical areas. Claude Code (Opus 4.8) with Numina-Lean-Agent reaches $61.8\%$ compile rate and $11.2\%$ SA-Pass. Across outputs generated by six agentic configurations, SA-Pass achieves $98.8\%$ binary agreement with expert judgments. An early version of ShadowBench served as the benchmark for Track 4 of the ICML 2026 AI4Math Challenge.

cs.CL↗
arXiv2017

Generic states and stability

We define the notion of the generic state polytope, analogous to the generic initial ideal and prove its existence: This greatly generalizes the work of Römer and Schmitz who proved the existence of generic Gröber fans. We also show that a generic state polytope always contains the trivial character: Equivalently, in any GIT quotient problem of semisimple group representations, every point is semistable with respect to a {\it general} maximal torus. Also, we revisit Kempf's proof of the existence of the worst one parameter subgroup (1-ps) and describe the equations for determining the worst 1-ps.

math.AG↗
arXiv2017

Note on the decomposition of states

We derive a sharp decomposition formula for the state polytope of the Hilbert point and the Hilbert-Mumford index of reducible varieties by using the decomposition of characters and basic convex geometry. This proof captures the essence of the decomposition of the state polytopes in general, and considerably simplifies an earlier proof by the author and Jaekwang Kim which uses a careful analysis of initial ideals of reducible varieties.

math.AG↗
arXiv2017

Grothendieck-Plücker images of Hilbert schemes are degenerate

We study the decompositions of Hilbert schemes induced by the Schubert cell decomposition of the Grassmannian variety and show that Hilbert schemes admit a stratification into locally closed subschemes along which the generic initial ideals remain the same. We give two applications: First, we give a completely geometric proofs of the existence of the generic initial ideals and of their Borel fixed properties. Secondly, we prove that when a Hilbert scheme of nonconstant Hilbert polynomial is embedded by the Grothendieck-Plücker embedding of a high enough degree, it must be degenerate.

math.AG↗
arXiv2016

Conjugacy classes of commuting nilpotents

We consider the space $\mathcal M_{q,n}$ of regular $q$-tuples of commuting nilpotent endomorphisms of $k^n$ modulo simultaneous conjugation. We show that $\mathcal M_{q,n}$ admits a natural homogeneous space structure, and that it is an affine space bundle over $\mathbb P^{q-1}$. A closer look at the homogeneous structure reveals that, over $\mathbb C$ and with respect to the complex topology, $\mathcal M_{q,n}$ is a smooth vector bundle over $\mathbb P^{q-1}$. We prove that, in this case, $\mathcal M_{q,n}$ is diffeomorphic to a direct sum of twisted tangent bundles. We also prove that $\mathcal M_{q,n}$ possesses a universal property and represents a functor of ideals, and use it to identify $\mathcal M_{q,n}$ with an open subscheme of a punctual Hilbert scheme. By using a result of A. Iarrobino, we show that $\mathcal M_{q,n} \to \mathbb P^{q-1}$ is not a vector bundle, hence giving a family of affine space bundles that are not vector bundles.

math.AG↗
arXiv2013

Birational contraction of genus two tails in the moduli space of genus four curves I

We show that for $α\in (2/3, 7/10)$, the log canonical model $\bar M_4(α)$ of the pair $(\bar M_4, αδ)$ is isomorphic to the moduli space $\bar M_4^{hs}$ of h-semistable curves, and that there is a birational morphism $Ξ: \bar M_4^{hs} \to \bar M_4(2/3)$ that contracts the locus of curves $C_1\cup_p C_2$ consisting of genus two curves meeting in a node $p$ such that $p$ is a Weierstrass point of $C_1$ or $C_2$. To obtain this morphism, we construct a compact moduli space $\bar M_{2,1}^{hs}$ of pointed genus two curves that have nodes, ordinary cusps and tacnodes as singularity, and prove that it is isomorphic to Rulla's flip constructed in his thesis.

math.AG↗
arXiv2011

GIT Constructions of Log Canonical Models of M_g

The purpose of this article is to give an overview of the construction of moduli spaces of curves from the viewpoint of the log minimal model program for M_g by providing an update of recent developments and discussing future problems. This survey is distinguished from the recent articles of Fedorchuk-Smyth and Morrison in its focus on low degree Hilbert stability of curves.

math.AG↗
arXiv2011

An outline of the log minimal model program for the moduli space of curves

Hassett and Keel predicted that there is a descending sequence of critical $α$ values where the log canonical model for the moduli space of stable curves with respect to $αδ$ changes. We derive a conjectural formula for the critical values in two different ways, by working out the intersection theory of the moduli space of hyperelliptic curves and by computing the GIT stability of certain curves with tails and bridges. The results give a rough outline of how the log minimal model program would proceed, telling us when the log canonical model changes and which curves are to be discarded and acquired at the critical steps.

math.AG↗
arXiv2009

Stability of Tails and 4-Canonical Models

We show that the GIT quotients of suitable loci in the Hilbert and Chow schemes of 4-canonically embedded curves of genus $g\ge 3$ are the moduli space $\bar{M}_g^{\text{ps}}$ of pseudo-stable curves constructed by Schubert in \cite{Schubert} using Chow varieties and 3-canonical models. The only new ingredient needed in the Hilbert scheme variant is a more careful analysis of the stability with respect to a certain 1-ps $λ$ of the $m^{\text{th}}$ Hilbert points of curves $X$ with elliptic tails. We compute the exact weight with which $λ$ acts, and not just the leading term in $m$ of this weight. A similar analysis of stability of curves with rational cuspidal tails allows us to determine the stable and semistable 4-canonical Chow loci. Although here the geometry of the quotient is more complicated because there are strictly semi-stable orbits, we are able to again identify it as $\bar{M}_g^{\text{ps}}$. Our computations yield, as byproducts, examples of both $m$-Hilbert unstable and $m$-Hilbert stable $X$ that are Chow strictly semi-stable.

math.AG↗
arXiv2008

Log minimal model program for the moduli space of stable curves: The first flip

We give a geometric invariant theory (GIT) construction of the log canonical model $\bar M_g(α)$ of the pairs $(\bar M_g, αδ)$ for $α\in (7/10 - ε, 7/10]$ for small $ε\in \mathbb Q_+$. We show that $\bar M_g(7/10)$ is isomorphic to the GIT quotient of the Chow variety bicanonical curves; $\bar M_g(7/10-ε)$ is isomorphic to the GIT quotient of the asymptotically-linearized Hilbert scheme of bicanonical curves. In each case, we completely classify the (semi)stable curves and their orbit closures. Chow semistable curves have ordinary cusps and tacnodes as singularities but do not admit elliptic tails. Hilbert semistable curves satisfy further conditions, e.g., they do not contain elliptic bridges. We show that there is a small contraction $Ψ: \bar M_g(7/10+ε) \to \bar M_g(7/10)$ that contracts the locus of elliptic bridges. Moreover, by using the GIT interpretation of the log canonical models, we construct a small contraction $Ψ^+ : \bar M_g(7/10-ε) \to \bar M_g(7/10)$ that is the Mori flip of $Ψ$.

math.AG↗
arXiv2007

Log minimal model program for the moduli space of stable curves of genus three

In this paper, we completely work out the log minimal model program for the moduli space of stable curves of genus three. We employ a rational multiple $αδ$ of the divisor $δ$ of singular curves as the boundary divisor, construct the log canonical model for the pair $(\bar{\mathcal M}_3, αδ)$ using geometric invariant theory as we vary $α$ from one to zero, and give a modular interpretation of each log canonical model and the birational maps between them. By using the modular description, we are able to identify all but one log canonical models with existing compactifications of $M_3$, some new and others classical, while the exception gives a new modular compactification of $M_3$.

math.AG↗
arXiv2006

Log canonical models for the moduli space of curves: First divisorial contraction

In this paper, we initiate our investigation of log canonical models for the moduli space of curves with the boundary divisor $\a \d$ as we decrease $\a$ from 1 to 0. We prove that for the first critical value $\a = 9/11$, the log canonical model is isomorphic to the moduli space of pseudostable curves, which have nodes and cusps as singularities. We also show that $\a = 7/10$ is the next critical value, i.e., the log canonical model stays the same in the interval $(7/10, 9/11]$. In the appendix, we develop a theory of log canonical models of stacks that explains how these can be expressed in terms of the coarse moduli space.

math.AG↗