संस्कृतम् × Lean 4

RLVR on Sanskrit Fine-tuning Qwen3-8B with a Lean formalization of Sanskrit

by Anish Lakkapragada repo sanskrit-rlvr
Contents
  1. Motivation
  2. Building Sanskrit's Verification Engine
  3. Fine-tuning Qwen3-8B with SFT & GRPO
  4. Results
  5. Conclusions

TLDR: We created a Lean formalization of a portion of Sanskrit to generate verified data and fine-tune Qwen3-8B. Our results demonstrate promise in using formal methods for both data-generation and verified rewards. See the GitHub repo here.

Motivation

Formalization and formal methods has become increasingly popular recently, in no small part due to the recent increase in AI-generated code/math. One domain formalization has largely left untouched, though, is natural human language — which is reasonable, considering how illogical English can be at times. As I learned more about this space, I remembered the following urban legend:

"Sanskrit is the most programmable language"

It only seemed natural to wonder then: Can we formalize all, or a part of, Sanskrit? Moreover, given such a formalization engine, what would happen if we RL'd a model against it (in line with modern RLVR efforts)?

This report is an account of my experiment and process. As a fair disclaimer, I am by no means an expert in Sanskrit linguistics and hence if you find anything, please reach out.

Building Sanskrit's Verification Engine

📚As a bit of history, Sanskrit's 3,983 grammatical rules were written into the foundational Ashtadhyayi during the 4th century BCE.

The key thing we required here was a grader function to take in a given sentence of Sanskrit and spit out a boolean decision of if it was grammatical or not. While existing Sanskrit linguistic tools exist (e.g. Sanskrit Heritage Site, vidyut-prakriya), because we planned to use this checker to not just validate sentences but also generate training tasks (explained momentarily), we decided it would be best to just create our own Lean formal checker.

To start, we first identified two high-quality Sanskrit materials:

Using the DCS, Fable was able to identify the frequencies of these tokens while filtering for those we could actually use in an internally consistent fragment (for example, we focused on verbs that were only in the finite present indicative tense). From there, a subset of 500 of the most frequent nouns were chosen (which accounted for 51.5% of all found noun tokens in DCS), and so Fable looked for the subset of verbs and adjectives which would also meet 51.5% probability mass in their own token category. The idea here is that we want all parts-of-speech in this fragment to be more or less used at around the same frequency in Sanskrit. This yielded 100 verbs and 150 adjectives. To see the work in this step, take a look at data/dcs/README.md.

Having identified this fragment, Fable sorted each word into one of 33 declension/conjugation classes and hand-encoded the grammar tables into Lean. As a sanity check, the words generated by our formalization rules (see functions decline and conjugate) matched 94.2% with the words from DCS, meaning we had largely succeeded in an independent reproduction of Sanskrit.

Finally, this Lean formalization exposes a formal grammatical checker. Specifically, lean/Check.lean creates a Lean executable check that can verify any Sanskrit sentence (encoded in IAST) for grammatical correctness. In addition, check can also return more fine-grained information on if the sentence respects given constraints (i.e. must use certain words), satisfies five grammatical conditions (regarding words/clauses/subject/adjective/objects), and more. The simplest example run of check is shown below:

.lake/build/bin/check "bālaḥ nadīṃ paśyati" # The boy sees the river

Here, all we care about is if we get an exit status of 0, which happens iff the sentence is grammatically correct. For more information on the full capabilities of check (which we utilize across our six fine-tuning tasks), see here.

As a wrap-up, the full formalization directory can be found in lean/. While this fragment is obviously not all of Sanskrit, our hope is that for a proof-of-concept demo this would suffice.

1. Modification of a noun, pronoun, or adjective based on what it is doing in the sentence. We don't have this in English.

Fine-tuning Qwen3-8B with SFT & GRPO

As is convention, we fine-tuned Qwen3-8B first with SFT and then GRPO. Fine-tuning with SFT is straightforward: just plain cross-entropy. GRPO was more complicated: each of the fine-tuning tasks had a reward-specific function, which was a mix of the Lean checker and Python inspection. We detail our fine-tuning tasks and their corresponding rewards in the section below.

Data

Before getting into the precise tasks we used, we categorize Sanskrit sentences into two buckets: in-fragment and out-of-fragment based on whether or not the sentence was modeled inside lean/ (i.e. could check execute against it?). The former is what was used for fine-tuning, and the latter was used as an eval of model generalization.

Training: In-fragment Data

As the name suggests, the in-fragment data was generated entirely from the modeled lexicon in lean/. The in-fragment data consisted of six tasks:

The reward for these tasks used by GRPO can be given by 0.15 * format + 0.85 * task, where format is a 0/1 score on if the answer was correctly wrapped in <ans></ans> tags and task is a task-specific score. You can view examples of the above six tasks and how task is computed for them below:

Interactive The six task families

Prompt — what the model sees
Gold answer
How was task computed

The in-fragment training files are located in data/in_fragment/{grpo, sft}/{train, valid}.jsonl.

Evaluation: Out-of-fragment (OOF) Data

The OOF data is meant to evaluate the model's abilities to reason on Sanskrit outside of the Lean formalization. The OOF data was generated from 22 classical texts (Mahābhārata, Rāmāyaṇa, etc.) and consists of purely cloze tasks with the following catch: each sentence must contain at least one OOF token, but the blanked token for the model to predict is in-fragment. An example question is given below:

Out-of-fragment cloze — real row, from the Rāmāyaṇa

The following is a line of classical Sanskrit, written without sandhi and with compounds hyphenated: "tam ca ____ daśarathaḥ yaṣṭu-kāmaḥ kṛta-añjaliḥ". Replace ____ with the correct form of the noun rājan ('king'). Output only that word.

rājā

The surrounding line uses grammar the fragment does not model (yaṣṭu-kāmaḥ is an infinitive compound) — but the blank itself is the nominative singular of rājan, squarely inside the formalization.

The goal here is to assess the models' ability to generalize Sanskrit's rules to unfamiliar texts, similar to how someone would try to infer the meaning of an unknown word when reading a book. The evaluated metric here was whether the model's output exactly matched the correct answer.

Evaluation Metrics

Having explained data and rewards away, the last custom piece remaining is our evaluation metrics. Note that for the in-fragment evaluation, we evaluate across all six aforementioned tasks (see data/in_fragment/eval.jsonl). We list the relevant metrics below:

In-fragment metrics
compile_rate
% of generated sentences the Lean checker accepts applies to translate · compose · post_edit
exact_rate
% solved perfectly, where the answer is in the gold accept list applies to qa · cloze · error_id
fix_rate
% of corrupted sentences fully repaired applies to post_edit
mean_reward
mean of the actual training reward all tasks
chrF++
character n-gram similarity between the model's answer and the reference answer2 all tasks
TER ↓
translation edit rate against the reference: the number of edits needed to turn the model's answer into the reference, so lower is better all tasks
Out-of-fragment metrics
cloze_exact
% of blanks faithfully restored in the source text the OOF benchmark's single task

2. Note that in Sanskrit the word order enjoys much flexibility, and so chrF++ and TER may not always be the most informative.

Results

We are now ready to get to the results. We evaluate on the following models:

Fig. 1 Final benchmarks across the four models
Data table
Fig. 2 Training evolution: one SFT trunk, two GRPO branches
Data table

Conclusions

The first thing to note is that the performance improvements relative to the base model come by and large by SFT. Furthermore, if we consider cloze_exact (OOF) as a metric of generalization, ironically SFT is much more helpful in this regard than RL. While it's easy to jump to the conclusion that this means our verified rewards system was meaningless, this is hard to conclude because it was the formalization itself which produced all of the SFT data. Additionally, GRPO-Lean outperformed GRPO-chrF++ on compile_rate and chrF++ itself.

If I had to guess the single best next step to this study, I think it would likely be having a human domain expert take a rigorous look at the formalization and suggest a better fragment or clarify any misformalizations. Thank you for reading!

Special thank you to 1517 for providing me with Lambda GPU credits to fund these experiments. If you have any questions or would like to get in touch, please email me.