arXiv subjects

Jineon Baek

Publications and source records attributed to Jineon Baek.

17 recordsLinked to original sources

arXiv2026

A Computational Obstruction to Swapping Area and Dinv: An Automata-Theoretic View of the $q,t$-Catalan Symmetry

Algebraic combinatorics often seeks bijections that explain identities between distributions object by object. Encoding combinatorial objects as words lets automata theory study such a bijection as a word-to-word computation and measure its memory, input access, and control of output order. This refines existence questions by asking which computational mechanisms a bijection requires. We develop this viewpoint for Dyck paths. Our motivating example is the $q,t$-Catalan polynomial. Let $D_n$ be the set of Dyck paths of semilength $n$, let $D=\bigcup_{n\ge 0}D_n$, and let $area, dinv, bounce \colon D\to\mathbb{N}$ be the standard statistics. Then, \[ C_n(q,t)=\sum_{P\in D_n}q^{area(P)}t^{bounce(P)} =\sum_{P\in D_n}q^{dinv(P)}t^{area(P)}. \] Haglund's zeta map $\zeta\colon D\to D$ gives a bijective proof: it preserves semilength and sends $(dinv,area)$ to $(area,bounce)$. By contrast, the full symmetry $C_n(q,t)=C_n(t,q)$ still lacks a direct explanation: no explicit, uniform, semilength-preserving bijection is known that swaps area and dinv on every Dyck path. Polyregular maps from automata theory provide a natural computational starting point, but we prove that neither $\zeta$ nor the classical height-sweep bijection witnessing Narayana symmetry is polyregular. The missing mechanism is global ordering by numerical levels whose range grows with the input. We call this a \emph{rank sort} and introduce \emph{weighted-rank polyregular maps} (WRP), extending polyregular maps by one such sort and containing both bijections. Nevertheless, WRP is a proper subclass of deterministic logspace. We prove that $\zeta^{-1}$ lies outside WRP and that no WRP map can realise a semilength-preserving area-dinv swap. Thus the rank-sorting strategy behind $\zeta$ cannot be extended within WRP to exchange the two statistics.

math.CO↗

arXiv2026

Sum-of-Squares Certificates for Copositive Matrices via Recursive Identities: The de Klerk-Pasechnik Conjecture and Hoffman--Pereira Matrices

We establish the conjecture by de Klerk and Pasechnik (2002), claiming that the semidefinite bounds $\vartheta^{(r)}(G)(r\geq 0)$ for the stability number $\alpha(G)$ are exact at $r=\alpha(G)-1$, by exhibiting an explicit sum-of-squares certificate. This certificate allows us to recover a known characterization of the minimizers of the Motzkin-Straus formulation for $1/\alpha(G)$. Additionally, we give sum-of-squares copositivity certificates for the matrices satisfying the Hoffman--Pereira sign condition, a crucial condition for characterizing copositive matrices with $\{-1,0,1\}$ entries.

math.OC↗

arXiv2026

Lean-GAP: A Dataset of Formalized Graduate Algebra Problems

We present Lean-GAP (Lean-Graduate Agebra Problems), 430 formalized graduate-level algebra problems from the textbook Abstract Algebra by Dummit and Foote. We develop a scalable pipeline consisting of PDF-to-LaTeX preprocessing, autoformalization into Lean 4, and verification of informal-formal correspondence. While the preprocessing and autoformalization stages can be largely automated, we find that verification remains the most subtle and labor-intensive component, requiring careful human oversight. Our contributions include (i) the construction of a structured dataset of formalized exercises, (ii) a systematic methodology for formalizing textbook mathematics, and (iii) an analysis of recurring challenges in the formalization process. We also compare the performance of different autoformalization models and highlight key bottlenecks in translating informal statements into formal language.

cs.LO↗

arXiv2024

Optimality of Gerver's Sofa

We resolve the moving sofa problem by showing that Gerver's construction with 18 curve sections attains the maximum area $2.2195\cdots$.

math.MG↗

arXiv2024

A note on the Erd\H{o}s conjecture about square packing

Let $f(n)$ denote the maximum total length of the sides of $n$ squares packed inside a unit square. Erd\H{o}s conjectured that $f(k^2+1)=k$. We show that the conjecture is true if we assume that the sides of the squares are parallel to the sides of the unit square.

math.CO↗

arXiv2024

Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4

The ABC conjecture implies many conjectures and theorems in number theory, including the celebrated Fermat's Last Theorem. Mason-Stothers Theorem is a function field analogue of the ABC conjecture that admits a much more elementary proof with many interesting consequences, including a polynomial version of Fermat's Last Theorem. While years of dedicated effort are expected for a full formalization of Fermat's Last Theorem, the simple proof of Mason-Stothers Theorem and its corollaries calls for an immediate formalization. We formalize an elementary proof by Snyder in Lean 4, and also formalize many consequences of Mason-Stothers, including nonsolvability of Fermat-Cartan equations in polynomials, nonparametrizability of a certain elliptic curve, and Davenport's Theorem. We compare our work to existing formalizations of the Mason-Stothers by Eberl in Isabelle and Wagemaker in Lean 3 respectively. Our formalization has been integrated into the mathlib library of Lean 4.

cs.LO↗

arXiv2024

A Conditional Upper Bound for the Moving Sofa Problem

The moving sofa problem asks for the connected shape with the largest area $\mu_{\text{max}}$ that can move around the right-angled corner of a hallway $L$ with unit width. The best bounds currently known on $\mu_{\max}$ are summarized as $2.2195\ldots \leq \mu_{\max} \leq 2.37$. The lower bound $2.2195\ldots \leq \mu_{\max}$ comes from Gerver's sofa $S_G$ of area $\mu_G := 2.2195\ldots$. The upper bound $\mu_{\max} \leq 2.37$ was proved by Kallus and Romik using extensive computer assistance. It is conjectured that the equality $\mu_{\max} = \mu_G$ holds at the lower bound. We develop a new approach to the moving sofa problem by approximating it as an infinite-dimensional convex quadratic optimization problem. The problem is then explicitly solved using a calculus of variation based on the Brunn-Minkowski theory. Consequently, we prove that any moving sofa satisfying a property named the injectivity condition has an area of at most $1 + \pi^2/8 = 2.2337\dots$. The new conditional bound does not rely on any computer assistance, yet it is much closer to the lower bound $2.2195\ldots$ of Gerver than the computer-assisted upper bound $2.37$ of Kallus and Romik. Gerver's sofa $S_G$, the conjectured optimum, satisfies the injectivity condition in particular.

math.MG↗

arXiv2023

$n^2 + 1$ unit equilateral triangles cannot cover an equilateral triangle of side $> n$ if all triangles have parallel sides

Conway and Soifer showed that an equilateral triangle $T$ of side $n + \varepsilon$ with sufficiently small $\varepsilon > 0$ can be covered by $n^2 + 2$ unit equilateral triangles. They conjectured that it is impossible to cover $T$ with $n^2 + 1$ unit equilateral triangles no matter how small $\varepsilon$ is. We show that if we require all sides of the unit equilateral triangles to be parallel to the sides of $T$ (e.g. $\bigtriangleup$ and $\bigtriangledown$), then it is impossible to cover $T$ of side $n + \varepsilon$ with $n^2 + 1$ unit equilateral triangles for any $\varepsilon > 0$. As the coverings of $T$ by Conway and Soifer only involve triangles with sides parallel to $T$, our result determines the exact minimum number $n^2+2$ of unit equilateral triangles with all sides parallel to $T$ that cover $T$. We also determine the largest value $\varepsilon = 1/(n + 1)$ (resp. $\varepsilon = 1 / n$) of $\varepsilon$ such that the equilateral triangle $T$ of side $n + \varepsilon$ can be covered by $n^2+2$ (resp. $n^2 + 3$) unit equilateral triangles with sides parallel to $T$, where the first case is achieved by the construction of Conway and Soifer.

math.CO↗

arXiv2022

On the Erd\H{o}s-Tuza-Valtr Conjecture

The Erd\H{o}s-Szekeres conjecture states that any set of more than $2^{n-2}$ points in the plane with no three on a line contains the vertices of a convex $n$-gon. Erd\H{o}s, Tuza, and Valtr strengthened the conjecture by stating that any set of more than $\sum_{i = n - b}^{a - 2} \binom{n - 2}{i}$ points in a plane either contains the vertices of a convex $n$-gon, $a$ points lying on a concave downward curve, or $b$ points lying on a concave upward curve. They also showed that the generalization is actually equivalent to the Erd\H{o}s-Szekeres conjecture. We prove the first new case of the Erd\H{o}s-Tuza-Valtr conjecture since the original 1935 paper of Erd\H{o}s and Szekeres. Namely, we show that any set of $\binom{n-1}{2} + 2$ points in the plane with no three points on a line and no two points sharing the same $x$-coordinate either contains 4 points lying on a concave downward curve or the vertices of a convex $n$-gon.

math.CO↗

arXiv2020

Prescribing Deep Attentive Score Prediction Attracts Improved Student Engagement

Intelligent Tutoring Systems (ITSs) have been developed to provide students with personalized learning experiences by adaptively generating learning paths optimized for each individual. Within the vast scope of ITS, score prediction stands out as an area of study that enables students to construct individually realistic goals based on their current position. Via the expected score provided by the ITS, a student can instantaneously compare one's expected score to one's actual score, which directly corresponds to the reliability that the ITS can instill. In other words, refining the precision of predicted scores strictly correlates to the level of confidence that a student may have with an ITS, which will evidently ensue improved student engagement. However, previous studies have solely concentrated on improving the performance of a prediction model, largely lacking focus on the benefits generated by its practical application. In this paper, we demonstrate that the accuracy of the score prediction model deployed in a real-world setting significantly impacts user engagement by providing empirical evidence. To that end, we apply a state-of-the-art deep attentive neural network-based score prediction model to Santa, a multi-platform English ITS with approximately 780K users in South Korea that exclusively focuses on the TOEIC (Test of English for International Communications) standardized examinations. We run a controlled A/B test on the ITS with two models, respectively based on collaborative filtering and deep attentive neural networks, to verify whether the more accurate model engenders any student engagement. The results conclude that the attentive model not only induces high student morale (e.g. higher diagnostic test completion ratio, number of questions answered, etc.) but also encourages active engagement (e.g. higher purchase rate, improved total profit, etc.) on Santa.

cs.HC↗

arXiv2020

Deep Attentive Study Session Dropout Prediction in Mobile Learning Environment

Student dropout prediction provides an opportunity to improve student engagement, which maximizes the overall effectiveness of learning experiences. However, researches on student dropout were mainly conducted on school dropout or course dropout, and study session dropout in a mobile learning environment has not been considered thoroughly. In this paper, we investigate the study session dropout prediction problem in a mobile learning environment. First, we define the concept of the study session, study session dropout and study session dropout prediction task in a mobile learning environment. Based on the definitions, we propose a novel Transformer based model for predicting study session dropout, DAS: Deep Attentive Study Session Dropout Prediction in Mobile Learning Environment. DAS has an encoder-decoder structure which is composed of stacked multi-head attention and point-wise feed-forward networks. The deep attentive computations in DAS are capable of capturing complex relations among dynamic student interactions. To the best of our knowledge, this is the first attempt to investigate study session dropout in a mobile learning environment. Empirical evaluations on a large-scale dataset show that DAS achieves the best performance with a significant improvement in area under the receiver operating characteristic curve compared to baseline models.

cs.LG↗

arXiv2020

Towards an Appropriate Query, Key, and Value Computation for Knowledge Tracing

Knowledge tracing, the act of modeling a student's knowledge through learning activities, is an extensively studied problem in the field of computer-aided education. Although models with attention mechanism have outperformed traditional approaches such as Bayesian knowledge tracing and collaborative filtering, they share two limitations. Firstly, the models rely on shallow attention layers and fail to capture complex relations among exercises and responses over time. Secondly, different combinations of queries, keys and values for the self-attention layer for knowledge tracing were not extensively explored. Usual practice of using exercises and interactions (exercise-response pairs) as queries and keys/values respectively lacks empirical support. In this paper, we propose a novel Transformer based model for knowledge tracing, SAINT: Separated Self-AttentIve Neural Knowledge Tracing. SAINT has an encoder-decoder structure where exercise and response embedding sequence separately enter the encoder and the decoder respectively, which allows to stack attention layers multiple times. To the best of our knowledge, this is the first work to suggest an encoder-decoder model for knowledge tracing that applies deep self-attentive layers to exercises and responses separately. The empirical evaluations on a large-scale knowledge tracing dataset show that SAINT achieves the state-of-the-art performance in knowledge tracing with the improvement of AUC by 1.8% compared to the current state-of-the-art models.

cs.LG↗

arXiv2020

Assessment Modeling: Fundamental Pre-training Tasks for Interactive Educational Systems

Like many other domains in Artificial Intelligence (AI), there are specific tasks in the field of AI in Education (AIEd) for which labels are scarce and expensive, such as predicting exam score or review correctness. A common way of circumventing label-scarce problems is pre-training a model to learn representations of the contents of learning items. However, such methods fail to utilize the full range of student interaction data available and do not model student learning behavior. To this end, we propose Assessment Modeling, a class of fundamental pre-training tasks for general interactive educational systems. An assessment is a feature of student-system interactions which can serve as a pedagogical evaluation. Examples include the correctness and timeliness of a student's answer. Assessment Modeling is the prediction of assessments conditioned on the surrounding context of interactions. Although it is natural to pre-train on interactive features available in large amounts, limiting the prediction targets to assessments focuses the tasks' relevance to the label-scarce educational problems and reduces less-relevant noise. While the effectiveness of different combinations of assessments is open for exploration, we suggest Assessment Modeling as a first-order guiding principle for selecting proper pre-training tasks for label-scarce educational problems.

cs.LG↗

arXiv2019

EdNet: A Large-Scale Hierarchical Dataset in Education

With advances in Artificial Intelligence in Education (AIEd) and the ever-growing scale of Interactive Educational Systems (IESs), data-driven approach has become a common recipe for various tasks such as knowledge tracing and learning path recommendation. Unfortunately, collecting real students' interaction data is often challenging, which results in the lack of public large-scale benchmark dataset reflecting a wide variety of student behaviors in modern IESs. Although several datasets, such as ASSISTments, Junyi Academy, Synthetic and STATICS, are publicly available and widely used, they are not large enough to leverage the full potential of state-of-the-art data-driven models and limits the recorded behaviors to question-solving activities. To this end, we introduce EdNet, a large-scale hierarchical dataset of diverse student activities collected by Santa, a multi-platform self-study solution equipped with artificial intelligence tutoring system. EdNet contains 131,441,538 interactions from 784,309 students collected over more than 2 years, which is the largest among the ITS datasets released to the public so far. Unlike existing datasets, EdNet provides a wide variety of student actions ranging from question-solving to lecture consumption and item purchasing. Also, EdNet has a hierarchical structure where the student actions are divided into 4 different levels of abstractions. The features of EdNet are domain-agnostic, allowing EdNet to be extended to different domains easily. The dataset is publicly released under Creative Commons Attribution-NonCommercial 4.0 International license for research purposes. We plan to host challenges in multiple AIEd tasks with EdNet to provide a common ground for the fair comparison between different state of the art models and encourage the development of practical and effective methods.

cs.CY↗

arXiv2019

Unpaired image denoising using a generative adversarial network in X-ray CT

This paper proposes a deep learning-based denoising method for noisy low-dose computerized tomography (CT) images in the absence of paired training data. The proposed method uses a fidelity-embedded generative adversarial network (GAN) to learn a denoising function from unpaired training data of low-dose CT (LDCT) and standard-dose CT (SDCT) images, where the denoising function is the optimal generator in the GAN framework. This paper analyzes the f-GAN objective to derive a suitable generator that is optimized by minimizing a weighted sum of two losses: the Kullback-Leibler divergence between an SDCT data distribution and a generated distribution, and the $\ell_2$ loss between the LDCT image and the corresponding generated images (or denoised image). The computed generator reflects the prior belief about SDCT data distribution through training. We observed that the proposed method allows the preservation of fine anomalous features while eliminating noise. The experimental results show that the proposed deep-learning method with unpaired datasets performs comparably to a method using paired datasets. A clinical experiment was also performed to show the validity of the proposed method for noise arising in the low-dose X-ray CT.

cs.CV↗

arXiv2017

Johnson's bijections and their application to counting simultaneous core partitions

Johnson recently proved Armstrong's conjecture which states that the average size of an $(a,b)$-core partition is $(a+b+1)(a-1)(b-1)/24$. He used various coordinate changes and one-to-one correspondences that are useful for counting problems about simultaneous core partitions. We give an expression for the number of $(b_1,b_2,\cdots, b_n)$-core partitions where $\{b_1,b_2,\cdots,b_n\}$ contains at least one pair of relatively prime numbers. We also evaluate the largest size of a self-conjugate $(s,s+1,s+2)$-core partition.

math.CO↗

arXiv2017

A bijective proof of Amdeberhan's conjecture on the number of $(s, s+2)$-core partitions with distinct parts

Amdeberhan conjectured that the number of $(s,s+2)$-core partitions with distinct parts for an odd integer $s$ is $2^{s-1}$. This conjecture was first proved by Yan, Qin, Jin and Zhou, then subsequently by Zaleski and Zeilberger. Since the formula for the number of such core partitions is so simple one can hope for a bijective proof. We give the first direct bijective proof of this fact by establishing a bijection between the set of $(s, s+2)$-core partitions with distinct parts and a set of lattice paths.

math.CO↗