Re:Form -- Reducing Human Priors in Scalable Formal Software
  Verification with RL in LLMs: A Preliminary Study on Dafny
Existing informal language-based (e.g., human language) Large Language Models
(LLMs) trained with Reinforcement Learning (RL) face a significant challenge:
their verification processes, which provide crucial training signals, are
neither reliable nor scalable. In fact, the prevalent large proprietary models
could hardly generate verifiable programs. A promising yet largely uncharted
alternative is formal language-based reasoning. Grounding LLMs in rigorous
formal systems where generative models operate in formal language spaces (e.g.,
Dafny) enables the automatic and mathematically provable verification of their
reasoning processes and outcomes. This capability is pivotal for achieving
large-scale, reliable formal software verification. It is a common practice to
employ human-annotated chain-of-thought and other human priors to induce the
reasoning and coding capabilities of LLMs. Unfortunately, it becomes
unacceptably all-consuming to provide such priors for supervising complex
programming tasks. In this work, we systematically explore ways to reduce human
priors with the formal language, Dafny, as the main environment for our pilot
study. Our pipeline mainly relies on introducing an automatic and scalable data
curation pipeline, and careful RL designs integrated with feedback from the
formal language verifier. We introduce DafnyComp, a benchmark of compositional
formal programs with auto-formalized specifications for specification
reasoning. Our supervised fine-tuning (SFT) stage enables even small models
(e.g., 0.5B) to generate syntactically valid and verifiable Dafny code,
surpassing proprietary models. RL with regularization further improves
performance, achieving stronger generalization to out-of-domain tasks and
outperforming all strong baselines on the challenging DafnyComp benchmark.
6881d9d8df7c5aafaf37f117
Chuanhao Yan
claimed_verified
2025-07-25T08:39:10.525Z
66310f977cd2bfbd3c824d6b
/avatars/6cbc03708dffd66715ba3c613fac2466.svg
Yan Chuanhao
user
SiniShell1
6881d9d8df7c5aafaf37f118
Fengdi Che
claimed_verified
2025-07-25T08:39:06.045Z
6881eea8ca5db489fdfb2b86
/avatars/9d6bac36c484545c8f01781fed281447.svg
Fengdi Che
user
FengdiFlo
6881d9d8df7c5aafaf37f119
Xuhan Huang
claimed_verified
2025-07-25T08:39:08.077Z
658afac6cffe7d2208657bcd
/avatars/0861bd6d394373cd9c03f207a019bc17.svg
Xuhan Huang
user
XuhanH
6881d9d8df7c5aafaf37f11a
Xu Xu
6881d9d8df7c5aafaf37f11b
Xin Li
6881d9d8df7c5aafaf37f11c
Yizhi Li
claimed_verified
2025-07-25T08:39:14.137Z
6382252f54421460665ec501
https://cdn-avatars.huggingface.co/v1/production/uploads/6382252f54421460665ec501/gW9fev3T5QPcNq4f9hqB1.jpeg
Yizhi Li
user
yizhilll
6881d9d8df7c5aafaf37f11d
Xingwei Qu
6881d9d8df7c5aafaf37f11e
Jingzhe Shi
6881d9d8df7c5aafaf37f11f
Zhuangzhuang He
admin_assigned
2025-09-22T19:41:02.927Z
6621e88fa11ce46061d25a16
/avatars/4a9a965a2d0f33e2855d2909a3e162bc.svg
Zhuangzhuang He
user
bruno888
6881d9d8df7c5aafaf37f120
Chenghua Lin
6881d9d8df7c5aafaf37f121
Yaodong Yang
6881d9d8df7c5aafaf37f122
Binhang Yuan
claimed_verified
2025-07-25T08:39:12.364Z
6307c8dda642348dc5e71c20
https://cdn-avatars.huggingface.co/v1/production/uploads/1661454675064-6307c8dda642348dc5e71c20.jpeg
Binhang Yuan
user
biyuan
6881d9d8df7c5aafaf37f123
Hang Zhao
6881d9d8df7c5aafaf37f124
Yu Qiao
6881d9d8df7c5aafaf37f125
Bowen Zhou
6881d9d8df7c5aafaf37f126
Jie Fu
claimed_verified
2025-07-25T08:39:15.917Z
641a6895fb5ffff5ac79d593
https://cdn-avatars.huggingface.co/v1/production/uploads/641a6895fb5ffff5ac79d593/vxvwsto3llOEWGqQKGMYx.jpeg
Jie Fu
user
bigaidream
Re:Form -- Reducing Human Priors in Scalable Formal Software
  Verification with RL in LLMs: A Preliminary Study on Dafny
Existing informal language-based (e.g., human language) Large Language Models
(LLMs) trained with Reinforcement Learning (RL) face a significant challenge:
their verification processes, which provide crucial training signals, are
neither reliable nor scalable. In fact, the prevalent large proprietary models
could hardly generate verifiable programs. A promising yet largely uncharted
alternative is formal language-based reasoning. Grounding LLMs in rigorous
formal systems where generative models operate in formal language spaces (e.g.,
Dafny) enables the automatic and mathematically provable verification of their
reasoning processes and outcomes. This capability is pivotal for achieving
large-scale, reliable formal software verification. It is a common practice to
employ human-annotated chain-of-thought and other human priors to induce the
reasoning and coding capabilities of LLMs. Unfortunately, it becomes
unacceptably all-consuming to provide such priors for supervising complex
programming tasks. In this work, we systematically explore ways to reduce human
priors with the formal language, Dafny, as the main environment for our pilot
study. Our pipeline mainly relies on introducing an automatic and scalable data
curation pipeline, and careful RL designs integrated with feedback from the
formal language verifier. We introduce DafnyComp, a benchmark of compositional
formal programs with auto-formalized specifications for specification
reasoning. Our supervised fine-tuning (SFT) stage enables even small models
(e.g., 0.5B) to generate syntactically valid and verifiable Dafny code,
surpassing proprietary models. RL with regularization further improves
performance, achieving stronger generalization to out-of-domain tasks and
outperforming all strong baselines on the challenging DafnyComp benchmark.
Formal language-based reasoning and automatic verification improve the reliability and scalability of Large Language Models in generating verifiable code.
Large Language Models Reinforcement Learning formal language-based reasoning formal systems generative models formal language spaces Dafny automatic verification human-annotated chain-of-thought human priors data curation pipeline supervised fine-tuning DafnyComp compositional formal programs auto-formalized specifications specification reasoning syntactically valid verifiable code generalization out-of-domain tasks