Searcharxiv⌕ Search

arXiv subjects

Naoto Onda

Publications and source records attributed to Naoto Onda.

5 recordsLinked to original sources
arXiv2026

Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

Large Language Models (LLMs) have demonstrated significant promise in formal theorem proving. In this study, we investigate the ability of LLMs to discover novel theorems and produce verified proofs. We propose a pipeline called Conjecturing-Proving Loop (CPL), which iteratively generates mathematical conjectures and attempts to prove them in Lean 4. A key feature of CPL is that each iteration conditions the LLM on previously generated theorems and their formal proofs, enabling parameter-free improvement of proof strategies via in-context learning. We provide both theoretical and experimental evidence that CPL increases the discovery rate of hard-to-prove theorems compared to frameworks that generate statements and proofs simultaneously. Moreover, our experiments show that reusing the LLM's own formally verified outputs as context consistently improves subsequent proof success, demonstrating the effectiveness of self-generated in-context learning for neural theorem proving. The source code is available at https://github.com/auto-res/ConjecturingProvingLoop.

cs.LG↗
arXiv2026

Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral

Understanding and certifying the generalization performance of machine learning algorithms -- i.e. obtaining theoretical estimates of the test error from the training error -- is a central theme of statistical learning theory. Among the many complexity measures used to derive such guarantees, Rademacher complexity yields sharp, data-dependent bounds that apply well beyond classical VC-dimension theory. In this study, we formalize the generalization error bound by Rademacher complexity in Lean 4, building on measure-theoretic probability theory available in the Mathlib library. Our development provides a mechanically-checked pipeline from the definitions of empirical and expected Rademacher complexity, through a formal symmetrization argument and a bounded-differences analysis, to high-probability uniform deviation bounds via a formally proved McDiarmid inequality. A key technical contribution is a reusable mechanism for lifting results from countable hypothesis classes (where measurability of suprema is straightforward in Mathlib) to separable topological index sets via a reduction to a countable dense subset. As worked applications of the abstract theorem, we mechanize standard empirical Rademacher bounds for linear predictors under $\ell_2$ and $\ell_1$ regularizations, and we also formalize a Dudley-type entropy integral bound based on covering numbers and a chaining construction.

cs.LG↗
arXiv2025

Development and performance evaluation of a water-based liquid scintillator tracking detector with wavelength-shifting fiber readout

We have developed a novel tracking detector utilizing a water-based liquid scintillator (WbLS) for the accurate characterization of neutrino interactions on a water target. In this detector, the WbLS is optically segmented into small cells by reflective separators, and the scintillation light is read out in three directions using wavelength-shifting fibers coupled to silicon photomultipliers. We developed and optimized WbLS samples for this application and measured their light yield using cosmic-ray muons. Subsequently, we constructed a prototype of the WbLS tracking detector and evaluated its performance with a positron beam. The beam test demonstrated good tracking performance, although the light yield was lower than required. The result prompted a review of the surfactant used in the WbLS and the material of the optical separators, leading to a significant improvement in light yield. In this paper, we report on a design of the WbLS tracking detector, the development of the WbLS, the results of the beam test, and subsequent improvements to the WbLS and optical separators.

physics.ins-det↗
arXiv2025

LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving

We introduce LeanConjecturer, a pipeline for automatically generating university-level mathematical conjectures in Lean 4 using Large Language Models (LLMs). Our hybrid approach combines rule-based context extraction with LLM-based theorem statement generation, addressing the data scarcity challenge in formal theorem proving. Through iterative generation and evaluation, LeanConjecturer produced 12,289 conjectures from 40 Mathlib seed files, with 3,776 identified as syntactically valid and non-trivial, that is, cannot be proven by \texttt{aesop} tactic. We demonstrate the utility of these generated conjectures for reinforcement learning through Group Relative Policy Optimization (GRPO), showing that targeted training on domain-specific conjectures can enhance theorem proving capabilities. Our approach generates 103.25 novel conjectures per seed file on average, providing a scalable solution for creating training data for theorem proving systems. Our system successfully verified several non-trivial theorems in topology, including properties of semi-open, alpha-open, and pre-open sets, demonstrating its potential for mathematical discovery beyond simple variations of existing results.

cs.AI↗