arXiv subjects

Taeil Hur

Publications and source records attributed to Taeil Hur.

8 recordsLinked to original sources

arXiv2025

Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques

The challenge of formal proof generation has a rich history, but with modern techniques, we may finally be at the stage of making actual progress in real-life mathematical problems. This paper explores the integration of ChatGPT and basic searching techniques to simplify generating formal proofs, with a particular focus on the miniF2F dataset. We demonstrate how combining a large language model like ChatGPT with a formal language such as Lean, which has the added advantage of being verifiable, enhances the efficiency and accessibility of formal proof generation. Despite its simplicity, our best-performing Lean-based model surpasses all known benchmarks with a 31.15% pass rate. We extend our experiments to include other datasets and employ alternative language models, showcasing our models' comparable performance in diverse settings and allowing for a more nuanced analysis of our results. Our findings offer insights into AI-assisted formal proof generation, suggesting a promising direction for future research in formal mathematical proof.

cs.LO↗

arXiv2022

Laplacian Pyramid-like Autoencoder

In this paper, we develop the Laplacian pyramid-like autoencoder (LPAE) by adding the Laplacian pyramid (LP) concept widely used to analyze images in Signal Processing. LPAE decomposes an image into the approximation image and the detail image in the encoder part and then tries to reconstruct the original image in the decoder part using the two components. We use LPAE for experiments on classifications and super-resolution areas. Using the detail image and the smaller-sized approximation image as inputs of a classification network, our LPAE makes the model lighter. Moreover, we show that the performance of the connected classification networks has remained substantially high. In a super-resolution area, we show that the decoder part gets a high-quality reconstruction image by setting to resemble the structure of LP. Consequently, LPAE improves the original results by combining the decoder part of the autoencoder and the super-resolution network.

cs.CV↗

arXiv2018

Deep learning for determining a near-optimal topological design without any iteration

In this study, we propose a novel deep learning-based method to predict an optimized structure for a given boundary condition and optimization setting without using any iterative scheme. For this purpose, first, using open-source topology optimization code, datasets of the optimized structures paired with the corresponding information on boundary conditions and optimization settings are generated at low (32 x 32) and high (128 x 128) resolutions. To construct the artificial neural network for the proposed method, a convolutional neural network (CNN)-based encoder and decoder network is trained using the training dataset generated at low resolution. Then, as a two-stage refinement, the conditional generative adversarial network (cGAN) is trained with the optimized structures paired at both low and high resolutions, and is connected to the trained CNN-based encoder and decoder network. The performance evaluation results of the integrated network demonstrate that the proposed method can determine a near-optimal structure in terms of pixel values and compliance with negligible computational time.

cs.LG↗

arXiv2011

Scale invariant extension of the standard model with strongly interacting hidden sector

We present a scale invariant extension of the standard model with new QCD-like strong interaction in the hidden sector. A scale $Λ_H$ is dynamically generated in the hidden sector by dimensional transmutation, and chiral symmetry breaking occurs in the hidden sector. This scale is transmitted to the SM sector by a real singlet scalar messenger S, and can trigger electroweak symmetry breaking (EWSB). Thus all the mass scales in this model arises from the hidden sector scale $Λ_H$ which has quantum mechanical origin. Furthermore the lightest hadrons in the hidden sector is stable by the flavor conservation of the hidden sector strong interaction, could be the cold dark matter (CDM). We study collider phenomenology, and relic density and direct detection rates of the CDM of this model.

hep-ph↗

arXiv2011

Electroweak symmetry breaking and cold dark matter from strongly interacting hidden sector

We consider a hidden sector with a vectorlike confining gauge theory like QCD with $N_{h,c}$ colors and $N_{h,f}$ light quarks ${\cal Q}_h$ in the hidden sector. Then a scale $Λ_H$ would be generated by dimensional transmutation, and chiral symmetry breaking occurs in the hidden sector. This scale $Λ_H$ can play a role of the SM Higgs mass parameter, triggering electroweak symmetry breaking (EWSB). Furthermore the lightest mesons in the hidden sector is stable by flavor conservation of the hidden sector strong interaction, and could be a good cold dark matter (CDM). We study collider phenomenology, and relic density and direct detection rates of the CDM of this model.

hep-ph↗

arXiv2009

Common gauge origin of discrete symmetries in observable sector and hidden sector

An extra Abelian gauge symmetry is motivated in many new physics models in both supersymmetric and nonsupersymmetric cases. Such a new gauge symmetry may interact with both the observable sector and the hidden sector. We systematically investigate the most general residual discrete symmetries in both sectors from a common Abelian gauge symmetry. Those discrete symmetries can ensure the stability of the proton and the dark matter candidate. A hidden sector dark matter candidate (lightest U-parity particle or LUP) interacts with the standard model fields through the gauge boson Z', which may selectively couple to quarks or leptons only. We make a comment on the implications of the discrete symmetry and the leptonically coupling dark matter candidate, which has been highlighted recently due to the possibility of the simultaneous explanation of the DAMA and the PAMELA results. We also show how to construct the most general U(1) charges for a given discrete symmetry, and discuss the relation between the U(1) gauge symmetry and R-parity.

hep-ph↗

arXiv2008

Neutral scalar Higgs bosons in the USSM at the LHC

We study the possibility of discovering neutral scalar Higgs bosons in the $U(1)'$-extended supersymmetric standard model (USSM) at the CERN Large Hadron Collider (LHC), by examining their productions via the exotic quark loop in the gluon fusion process at leading order. It is possible in some parameter region that the neutral scalar Higgs bosons may have stronger couplings with the exotic quarks than with top quark. In this case, the exotic quarks may contribute more significantly than top quark in productions of the neutral scalar Higgs bosons in the gluon fusion process. We find that there is indeed some parameter region in the USSM that supports our speculations.

hep-ph↗

arXiv2007

A Supersymmetric U(1)' Model with Multiple Dark Matters

We consider a scenario where a supersymmetric model has multiple dark matter particles. Adding a U(1)' gauge symmetry is a well-motivated extension of the Minimal Supersymmetric Standard Model (MSSM). It can cure the problems of the MSSM such as the mu-problem or the proton decay problem with high-dimensional lepton number and baryon number violating operators which R-parity allows. An extra parity (U-parity) may arise as a residual discrete symmetry after U(1)' gauge symmetry is spontaneously broken. The Lightest U-parity Particle (LUP) is stable under the new parity becoming a new dark matter candidate. Up to three massive particles can be stable in the presence of the R-parity and the U-parity. We numerically illustrate that multiple stable particles in our model can satisfy both constraints from the relic density and the direct detection, thus providing a specific scenario where a supersymmetric model has well-motivated multiple dark matters consistent with experimental constraints. The scenario provides new possibilities in the present and upcoming dark matter searches in the direct detection and collider experiments.

hep-ph↗