arXiv subjects

Jiakun Zhang

Publications and source records attributed to Jiakun Zhang.

3 recordsLinked to original sources

arXiv2026

Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving

Automated theorem proving with large language models in Lean 4 is commonly approached through either step-level tactic prediction with tree search or whole-proof generation. These two paradigms represent opposite granularities for constructing supervised training data: the former provides dense local signals but may fragment coherent proof processes, while the latter preserves global structure but requires complex end-to-end generation. In this paper, we revisit supervision granularity as a training set construction problem over proof trajectories and propose segment-level supervision, a training data construction strategy that extracts locally coherent proof segments for training policy models. We further reuse the same strategy at inference time to trigger short rollouts for existing step-level models. When trained with segment-level supervision on STP, LeanWorkbook, and NuminaMath-LEAN, the resulting policy models achieve proof success rates of 64.84%, 60.90%, and 66.31% on miniF2F, respectively, consistently outperforming both step-level and whole-proof baselines. Goal-aware rollout further improves existing step-level provers while reducing inference costs. It increases the proof success rate of BFS-Prover-V2-7B from 68.77% to 70.74% and that of InternLM2.5-StepProver from 59.59% to 60.33%, showing that appropriate supervision granularity better aligns model learning with proof structure and search. Code and models are available at https://github.com/NJUDeepEngine/SEG-ATP.

cs.AI↗

arXiv2025

LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation

Recent advancements in large language models (LLMs) have sparked considerable interest in automated theorem proving and a prominent line of research integrates stepwise LLM-based provers into tree search. In this paper, we introduce a novel proof-state exploration approach for training data synthesis, designed to produce diverse tactics across a wide range of intermediate proof states, thereby facilitating effective one-shot fine-tuning of LLM as the policy model. We also propose an adaptive beam size strategy, which effectively takes advantage of our data synthesis method and achieves a trade-off between exploration and exploitation during tree search. Evaluations on the MiniF2F and ProofNet benchmarks demonstrate that our method outperforms strong baselines under the stringent Pass@1 metric, attaining an average pass rate of $60.74\%$ on MiniF2F and $21.18\%$ on ProofNet. These results underscore the impact of large-scale synthetic data in advancing automated theorem proving.

cs.AI↗

arXiv2022

Research on the spectral reconstruction of a low-dimensional filter array micro-spectrometer based on a truncated singular value decomposition-convex optimization algorithm

Currently, the engineering of miniature spectrometers mainly faces three problems: the mismatch between the number of filters at the front end of the detector and the spectral reconstruction accuracy; the lack of a stable spectral reconstruction algorithm; and the lack of a spectral reconstruction evaluation method suitable for engineering. Therefore, based on 20 sets of filters, this paper classifies and optimizes the filter array by the K-means algorithm and particle swarm algorithm, and obtains the optimal filter combination under different matrix dimensions. Then, the truncated singular value decomposition-convex optimization algorithm is used for high-precision spectral reconstruction, and the detailed spectral reconstruction process of two typical target spectra is described. In terms of spectral evaluation, due to the strong randomness of the target detected during the working process of the spectrometer, the standard value of the target spectrum cannot be obtained. Therefore, for the first time, we adopt the method of joint cross-validation of multiple sets of data for spectral evaluation. The results show that when the random error of positive or negative 2 code values is applied multiple times for reconstruction, the spectral angle cosine value between the reconstructed curves becomes more than 0.995, which proves that the spectral reconstruction under this algorithm has high stability. At the same time, the spectral angle cosine value of the spectral reconstruction curve and the standard curve can reach above 0.99, meaning that it realizes a high-precision spectral reconstruction effect. A high-precision spectral reconstruction algorithm based on truncated singular value-convex optimization, which is suitable for engineering applications, is established in this paper, providing important scientific research value for the engineering application of micro-spectrometers.

physics.data-an↗