@inproceedings{shi-etal-2026-prooffrontier,
title = "{P}roof{F}rontier: Turning Verified Proofs into Boundary-hard Tasks for Formal Theorem Proving",
author = "Shi, Zhengyan and
Zhong, Jianyuan and
Zheng, Xiaolin and
Shi, Liangliang and
Xu, Qiang",
editor = "Lee, Hung-Yi and
Dev, Sunipa and
Li, Jessy and
Elliott, Desmond",
booktitle = "Findings of the {A}ssociation for {C}omputational {L}inguistics: {EMNLP} 2026",
month = oct,
year = "2026",
address = "Budapest, Hungary",
publisher = "Association for Computational Linguistics",
url = "https://aclanthology.org/2026.findings-emnlp.1615/",
doi = "10.18653/2026.findings-emnlp.1615",
pages = "34392--34404",
ISBN = "979-8-89176-462-0",
abstract = "Formal theorem proving provides executable verification signals from proof assistants, making it a key domain for improving the reliable reasoning ability of large language models through reinforcement learning (RL). However, RL-based prover training is increasingly bottlenecked by the scarcity of high-quality hard tasks: many existing Lean instances are either already solvable by current provers or too uninformative to drive further improvement. We propose ProofFrontier, a proof-structure-guided method for generating statement-preserving boundary-hard training tasks from verified Lean proofs. Instead of synthesizing open-ended problems that may be ill-posed or unverifiable, ProofFrontier starts from existing theorems with Lean-certified proofs, preserving task completeness and formal verifiability. It selectively withholds proof-structural guidance around important local nodes, encouraging the prover to rediscover nontrivial intermediate reasoning while keeping the original theorem statement unchanged. We further introduce capability-aware filtering to retain tasks that are solvable in principle but not easily solved by the base prover, yielding hard yet rewardable RL data. Training with GRPO on ProofFrontier-generated tasks consistently improves DeepSeek-Prover-V2 and Goedel-Prover-V2 on miniF2F, ProofNet, and PutnamBench. Notably, these gains are achieved using only hundreds of synthesized tasks, showing that complete boundary-hard tasks can be more data-efficient than simply scaling weak or already-solved proof data for theorem-proving RL."
}<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="shi-etal-2026-prooffrontier">
<titleInfo>
<title>ProofFrontier: Turning Verified Proofs into Boundary-hard Tasks for Formal Theorem Proving</title>
</titleInfo>
<name type="personal">
<namePart type="given">Zhengyan</namePart>
<namePart type="family">Shi</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Jianyuan</namePart>
<namePart type="family">Zhong</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Xiaolin</namePart>
<namePart type="family">Zheng</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Liangliang</namePart>
<namePart type="family">Shi</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Qiang</namePart>
<namePart type="family">Xu</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<originInfo>
<dateIssued>2026-10</dateIssued>
</originInfo>
<typeOfResource>text</typeOfResource>
<relatedItem type="host">
<titleInfo>
<title>Findings of the Association for Computational Linguistics: EMNLP 2026</title>
</titleInfo>
<name type="personal">
<namePart type="given">Hung-Yi</namePart>
<namePart type="family">Lee</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Sunipa</namePart>
<namePart type="family">Dev</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Jessy</namePart>
<namePart type="family">Li</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Desmond</namePart>
<namePart type="family">Elliott</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<originInfo>
<publisher>Association for Computational Linguistics</publisher>
<place>
<placeTerm type="text">Budapest, Hungary</placeTerm>
</place>
</originInfo>
<genre authority="marcgt">conference publication</genre>
<identifier type="isbn">979-8-89176-462-0</identifier>
</relatedItem>
<abstract>Formal theorem proving provides executable verification signals from proof assistants, making it a key domain for improving the reliable reasoning ability of large language models through reinforcement learning (RL). However, RL-based prover training is increasingly bottlenecked by the scarcity of high-quality hard tasks: many existing Lean instances are either already solvable by current provers or too uninformative to drive further improvement. We propose ProofFrontier, a proof-structure-guided method for generating statement-preserving boundary-hard training tasks from verified Lean proofs. Instead of synthesizing open-ended problems that may be ill-posed or unverifiable, ProofFrontier starts from existing theorems with Lean-certified proofs, preserving task completeness and formal verifiability. It selectively withholds proof-structural guidance around important local nodes, encouraging the prover to rediscover nontrivial intermediate reasoning while keeping the original theorem statement unchanged. We further introduce capability-aware filtering to retain tasks that are solvable in principle but not easily solved by the base prover, yielding hard yet rewardable RL data. Training with GRPO on ProofFrontier-generated tasks consistently improves DeepSeek-Prover-V2 and Goedel-Prover-V2 on miniF2F, ProofNet, and PutnamBench. Notably, these gains are achieved using only hundreds of synthesized tasks, showing that complete boundary-hard tasks can be more data-efficient than simply scaling weak or already-solved proof data for theorem-proving RL.</abstract>
<identifier type="citekey">shi-etal-2026-prooffrontier</identifier>
<identifier type="doi">10.18653/2026.findings-emnlp.1615</identifier>
<location>
<url>https://aclanthology.org/2026.findings-emnlp.1615/</url>
</location>
<part>
<date>2026-10</date>
<extent unit="page">
<start>34392</start>
<end>34404</end>
</extent>
</part>
</mods>
</modsCollection>
%0 Conference Proceedings
%T ProofFrontier: Turning Verified Proofs into Boundary-hard Tasks for Formal Theorem Proving
%A Shi, Zhengyan
%A Zhong, Jianyuan
%A Zheng, Xiaolin
%A Shi, Liangliang
%A Xu, Qiang
%Y Lee, Hung-Yi
%Y Dev, Sunipa
%Y Li, Jessy
%Y Elliott, Desmond
%S Findings of the Association for Computational Linguistics: EMNLP 2026
%D 2026
%8 October
%I Association for Computational Linguistics
%C Budapest, Hungary
%@ 979-8-89176-462-0
%F shi-etal-2026-prooffrontier
%X Formal theorem proving provides executable verification signals from proof assistants, making it a key domain for improving the reliable reasoning ability of large language models through reinforcement learning (RL). However, RL-based prover training is increasingly bottlenecked by the scarcity of high-quality hard tasks: many existing Lean instances are either already solvable by current provers or too uninformative to drive further improvement. We propose ProofFrontier, a proof-structure-guided method for generating statement-preserving boundary-hard training tasks from verified Lean proofs. Instead of synthesizing open-ended problems that may be ill-posed or unverifiable, ProofFrontier starts from existing theorems with Lean-certified proofs, preserving task completeness and formal verifiability. It selectively withholds proof-structural guidance around important local nodes, encouraging the prover to rediscover nontrivial intermediate reasoning while keeping the original theorem statement unchanged. We further introduce capability-aware filtering to retain tasks that are solvable in principle but not easily solved by the base prover, yielding hard yet rewardable RL data. Training with GRPO on ProofFrontier-generated tasks consistently improves DeepSeek-Prover-V2 and Goedel-Prover-V2 on miniF2F, ProofNet, and PutnamBench. Notably, these gains are achieved using only hundreds of synthesized tasks, showing that complete boundary-hard tasks can be more data-efficient than simply scaling weak or already-solved proof data for theorem-proving RL.
%R 10.18653/2026.findings-emnlp.1615
%U https://aclanthology.org/2026.findings-emnlp.1615/
%U https://doi.org/10.18653/2026.findings-emnlp.1615
%P 34392-34404
Markdown (Informal)
[ProofFrontier: Turning Verified Proofs into Boundary-hard Tasks for Formal Theorem Proving](https://aclanthology.org/2026.findings-emnlp.1615/) (Shi et al., Findings 2026)
ACL