# FVRuleLearner: Operator-Level Reasoning Tree (Op-Tree)-Based Rules Learning for Formal Verification

arXiv: https://arxiv.org/abs/2604.03245 · HTML: https://mlsanity.com/paper/2604.03245/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 33 of its 62 references that are in the map.
- First posted on arXiv 6 Mar 2026.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 30 of 33)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [DeepSeek-Coder-V2: Breaking the Barrier of Closed-Source Models in Code Intelligence](https://mlsanity.com/paper/2406.11931/) (2024)
- [TextGrad: Automatic "Differentiation" via Text](https://mlsanity.com/paper/2406.07496/) (2024)
- [When Can LLMs Actually Correct Their Own Mistakes? A Critical Survey of Self-Correction of LLMs](https://mlsanity.com/paper/2406.01297/) (2024)
- [Automatically Correcting Large Language Models: Surveying the landscape of diverse self-correction strategies](https://mlsanity.com/paper/2308.03188/) (2023)
- [ChipNeMo: Domain-Adapted LLMs for Chip Design](https://mlsanity.com/paper/2311.00176/) (2023)
- [Recursive Introspection: Teaching Language Model Agents How to Self-Improve](https://mlsanity.com/paper/2407.18219/) (2024)
- [SWT-Bench: Testing and Validating Real-World Bug-Fixes with Code Agents](https://mlsanity.com/paper/2406.12952/) (2024)
- [Symbolic Learning Enables Self-Evolving Agents](https://mlsanity.com/paper/2406.18532/) (2024)
- [RTLFixer: Automatically Fixing RTL Syntax Errors with Large Language Models](https://mlsanity.com/paper/2311.16543/) (2023)
- [Can LLMs Learn from Previous Mistakes? Investigating LLMs' Errors to Boost for Reasoning](https://mlsanity.com/paper/2403.20046/) (2024)
- [Internal Consistency and Self-Feedback in Large Language Models: A Survey](https://mlsanity.com/paper/2407.14507/) (2024)
- [In-Context Principle Learning from Mistakes](https://mlsanity.com/paper/2402.05403/) (2024)
- [LeDex: Training LLMs to Better Self-Debug and Explain Code](https://mlsanity.com/paper/2405.18649/) (2024)
- [Towards LLM-Powered Verilog RTL Assistant: Self-Verification and Self-Correction](https://mlsanity.com/paper/2406.00115/) (2024)
- [SOEN-101: Code Generation by Emulating Software Process Models Using Large Language Model Agents](https://mlsanity.com/paper/2403.15852/) (2024)
- [(Security) Assertions by Large Language Models](https://mlsanity.com/paper/2306.14027/) (2023)
- [AssertLLM: Generating and Evaluating Hardware Verification Assertions from Design Specifications via Multi-LLMs](https://mlsanity.com/paper/2402.00386/) (2024)
- [Towards Understanding the Characteristics of Code Generation Errors Made by Large Language Models](https://mlsanity.com/paper/2406.08731/) (2024)
- [ThinkRepair: Self-Directed Automated Program Repair](https://mlsanity.com/paper/2407.20898/) (2024)
- [ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation](https://mlsanity.com/paper/2402.00093/) (2024)
- [AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation](https://mlsanity.com/paper/2406.18627/) (2024)
- [Empowering Large Language Models to Set up a Knowledge Retrieval Indexer via Self-Learning](https://mlsanity.com/paper/2405.16933/) (2024)
- [SQLFixAgent: Towards Semantic-Accurate Text-to-SQL Parsing via Consistency-Enhanced Multi-Agent Collaboration](https://mlsanity.com/paper/2406.13408/) (2024)
- [Large Language Model (LLM) for Standard Cell Layout Design Optimization](https://mlsanity.com/paper/2406.06549/) (2024)
- [Collaborative Evolving Strategy for Automatic Data-Centric Development](https://mlsanity.com/paper/2407.18690/) (2024)
- [Hybrid-NL2SVA: Integrating RAG and Finetuning for LLM-based NL2SVA](https://mlsanity.com/paper/2506.21569/) (2025)
- [Retrieved In-Context Principles from Previous Mistakes](https://mlsanity.com/paper/2407.05682/) (2024)
- [Beyond Code Generation: Assessing Code LLM Maturity with Postconditions](https://mlsanity.com/paper/2407.14118/) (2024)

## Built on by (most cited first, 1 of 1)

- [Formal-Verification-Guided Bayesian Optimization for Non-Intrusive Last-Mile Coverage Closure](https://mlsanity.com/paper/2610.17449/) (2026)

## Abstract (arXiv)

The remarkable reasoning and code generation capabilities of large language models (LLMs) have recently motivated increasing interest in automating formal verification (FV), a process that ensures hardware correctness through mathematically precise assertions but remains highly labor-intensive, particularly through the translation of natural language into SystemVerilog Assertions (NL-to-SVA). However, LLMs still struggle with SVA generation due to limited training data and the intrinsic complexity of FV operators. Consequently, a more efficient and robust methodology for ensuring correct SVA operator selection is essential for producing functionally correct assertions. To address these challenges, we introduce FVRuleLearner, an Operator-Level Rule (Op-Rule) learning framework built on a novel Operator Reasoning Tree (Op-Tree), which models SVA generation as structured, interpretable reasoning. FVRuleLearner operates in two complementary phases: (1) Training: it constructs Op-Tree that decomposes NL-to-SVA alignment into fine-grained, operator-aware questions, combining reasoning paths that lead to correct assertions; and (2) Testing: it performs operator-aligned retrieval to fetch relevant reasoning traces from the learned Op-Tree and generate new rules for unseen specifications. In the comprehensive studies, the proposed FVRuleLearner outperforms the state-of-the-art baseline by 3.95% in syntax correctness and by 31.17% in functional correctness on average. Moreover, FVRuleLearner successfully reduces an average of 70.33% of SVA functional failures across diverse operator categories through a functional taxonomy analysis, showing the effectiveness of applying learned Op-Tree to the Op-Rule generations for unseen NL-to-SVA tasks. These results establish FVRuleLearner as a new paradigm for domain-specific reasoning and rule learning in formal verification.