Cover Image

Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Yan, Chuanhao, Che, Fengdi, Huang, Xuhan, Xu, Xu, Li, Xin, Li, Yizhi, Qu, Xingwei, Shi, Jingzhe, Lin, Chenghua, Yang, Yaodong, Yuan, Binhang, Zhao, Hang, Qiao, Yu, Zhou, Bowen, Fu, Jie
Format:	Preprint
Published:	2025
Subjects:	Computation and Language
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
by: Zeng, Lingfei, et al.
Published: (2025)

Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification
by: Xu, Xu, et al.
Published: (2025)

DafnyBench: A Benchmark for Formal Software Verification
by: Loughridge, Chloe, et al.
Published: (2024)

ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization
by: Chen, Guoxin, et al.
Published: (2025)

A Tutorial: An Intuitive Explanation of Offline Reinforcement Learning Theory
by: Che, Fengdi
Published: (2025)

ReFormer: Generating Radio Fakes for Data Augmentation
by: Kaasaragadda, Yagna, et al.
Published: (2024)

DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
by: Banerjee, Debangshu, et al.
Published: (2026)

Overview of the NLPCC 2024 Shared Task on Chinese Metaphor Generation
by: Qu, Xingwei, et al.
Published: (2024)

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
by: Ukhanov, Evgeny
Published: (2025)

Dafny as Verification-Aware Intermediate Language for Code Generation
by: Li, Yue Chen, et al.
Published: (2025)

Verification of E-Voting Algorithms in Dafny
by: Büttner, Robert, et al.
Published: (2025)

dafny-annotator: AI-Assisted Verification of Dafny Programs
by: Poesia, Gabriel, et al.
Published: (2024)

From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification
by: Erfan, Md, et al.
Published: (2026)

Derivation and Verification of Array Sorting by Merging, and its Certification in Dafny
by: Carbonell, Juan Pablo, et al.
Published: (2025)

TinyV: Reducing False Negatives in Verification Improves RL for LLM Reasoning
by: Xu, Zhangchen, et al.
Published: (2025)

The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification
by: Tihanyi, Norbert, et al.
Published: (2023)

Baking for Dafny: A CakeML Backend for Dafny
by: Nezamabadi, Daniel, et al.
Published: (2025)

ReVeal: Self-Evolving Code Agents via Reliable Self-Verification
by: Jin, Yiyang, et al.
Published: (2025)

MutDafny: A Mutation-Based Approach to Assess Dafny Specifications
by: Amaral, Isabel, et al.
Published: (2025)

Specification-Driven Generation and Evaluation of Discrete-Event World Models via the DEVS Formalism
by: Chen, Zheyu, et al.
Published: (2026)

DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
by: Fedchin, Aleksandr, et al.
Published: (2025)

Average-DICE: Stationary Distribution Correction by Regression
by: Che, Fengdi, et al.
Published: (2025)

Towards a Formal Verification of Secure Vehicle Software Updates
by: Hagen, Martin Slind, et al.
Published: (2025)

Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems
by: Wojtak, Connor, et al.
Published: (2025)

Automated Formal Verification of a Software Fault Isolation System
by: Sotoudeh, Matthew, et al.
Published: (2025)

PatchPilot: A Cost-Efficient Software Engineering Agent with Early Attempts on Formal Verification
by: Li, Hongwei, et al.
Published: (2025)

Overview of the NLPCC 2025 Shared Task: Gender Bias Mitigation Challenge
by: Li, Yizhi, et al.
Published: (2025)

LongEval: A Comprehensive Analysis of Long-Text Generation Through a Plan-based Paradigm
by: Wu, Siwei, et al.
Published: (2025)

Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny
by: Carreira, Carolina, et al.
Published: (2025)

Distributed Consensus Optimization with Consensus ALADIN
by: Du, Xu, et al.
Published: (2025)

CASCADE: A Cascading Architecture for Social Coordination with Controllable Emergence at Low Cost
by: Xu, Yizhi
Published: (2026)

Supporting Software Formal Verification with Large Language Models: An Experimental Study
by: Wang, Weiqi, et al.
Published: (2025)

The Design of an Interactive Proof Mode for Dafny
by: Ciobâcă, Ştefan, et al.
Published: (2025)

Verified VCG and Verified Compiler for Dafny
by: Nezamabadi, Daniel, et al.
Published: (2025)

Can Digital Transformation Reduce the Zombification of Enterprises?
by: Xiujuan Lan, et al.
Published: (2025)

DocMMIR: A Framework for Document Multi-modal Information Retrieval
by: Li, Zirui, et al.
Published: (2025)

Formal Verification of Parameterized Systems based on Induction
by: Xiu, Jiaqi, et al.
Published: (2025)

ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers
by: Chen, Chen, et al.
Published: (2025)

Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds
by: Reinhard, Tobias
Published: (2024)

Towards Automated Formal Verification of Backend Systems with LLMs
by: Xu, Kangping, et al.
Published: (2025)