Searcharxiv⌕ Search

arXiv subjects

Kazuhisa Nakasho

Publications and source records attributed to Kazuhisa Nakasho.

5 recordsLinked to original sources

IntSeqBERT: Learning Arithmetic Structure in OEIS via Modulo-Spectrum Embeddings

Integer sequences in the OEIS span values from single-digit constants to astronomical factorials and exponentials, making prediction challenging for standard tokenised models that cannot handle out-of-vocabulary values or exploit periodic arithmetic structure. We present IntSeqBERT, a dual-stream Transformer encoder for masked integer-sequence modelling on OEIS. Each sequence element is encoded along two complementary axes: a continuous log-scale magnitude embedding and sin/cos modulo embeddings for 100 residues (moduli $2$--$101$), fused via FiLM. Three prediction heads (magnitude regression, sign classification, and modulo prediction for 100 moduli) are trained jointly on 274,705 OEIS sequences. At the Large scale (91.5M parameters), IntSeqBERT achieves 95.85% magnitude accuracy and 50.38% Mean Modulo Accuracy (MMA) on the test set, outperforming a standard tokenised Transformer baseline by $+8.9$ pt and $+4.5$ pt, respectively. An ablation removing the modulo stream confirms it accounts for $+15.2$ pt of the MMA gain and contributes an additional $+6.2$ pt to magnitude accuracy. A probabilistic Chinese Remainder Theorem (CRT)-based Solver converts the model's predictions into concrete integers, yielding a 7.4-fold improvement in next-term prediction over the tokenised-Transformer baseline (Top-1: 19.09% vs. 2.59%). Modulo spectrum analysis reveals a strong negative correlation between Normalised Information Gain (NIG) and Euler's totient ratio $φ(m)/m$ ($r = -0.851$, $p < 10^{-28}$), providing empirical evidence that composite moduli capture OEIS arithmetic structure more efficiently via CRT aggregation.

cs.LG↗

Remote Verification System for Mizar Integrated with Emwiki

In this paper, we present a remote verification environment for Mizar and its integration with a web platform. Although a VSCode extension for Mizar is already available, it requires installing the Mizar verification tools locally. Our newly developed system implements these verification environments on a server, eliminating this requirement. First, we explain the implementation of the remote verification environment for Mizar and the VSCode for the Web extension. Second, we discuss the integration with the web platform emwiki, which allows browsing the existing Mizar Mathematical Library (MML).

cs.SE↗

The Tight Upper Bound for the Size of Single Deletion Error Correcting Codes in Dimension 11

A single deletion error correcting code (SDECC) is a set of fixed-length sequences consisting of two types of symbols, 0 and 1, such that the original sequence can be recovered for at most one deletion error. The upper bound for the size of SDECC is expected to be equal to the size of Varshamov-Tenengolts (VT) code, and this conjecture had been shown to be true when the code length is ten or less. In this paper, we discuss a method for calculating this upper bound by providing an integer linear programming solver with several linear constraints. As a new result, we obtained that the tight upper bound for the size of a single deletion error correcting code in dimension 11 is 172.

cs.IT↗

An Integrated Web Platform for the Mizar Mathematical Library

This paper reports on the development of a Web platform to host the Mizar Mathematical Library (MML). In recent years, the size of formalized mathematical libraries has been drastically increasing, and this has led to a growing demand for tools that support efficient and comprehensive browsing, searching, and annotation of these libraries. This platform implements a Wiki function to add comments to the HTMLized MML, three types of search function (article, symbol, and theorem), and a function to show the dependency graph of the MML. This platform is designed with consistency, scalability, and interoperability as top priorities for long-term use.

cs.PL↗

Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library

The purpose of this project is to collect symbol information in the Mizar Mathematical Library and manipulate it into practical and organized documentation. Inspired by the MathWiki project and API reference systems for computer programs, we developed a documentation generator focusing on symbols for the HTML-ized Mizar library. The system has several helpful features, including a symbol list, incremental search, and a referrer list. It targets those who use proof assistance systems, the volume of whose libraries has been rapidly increasing year by year.

cs.MS↗