We describe HSE’s submission to the Sorbian track of WMT26 Multitask LLMs with Lim- ited Resources, where a single 2B-parameter model must translate between German, Up- per Sorbian, and Lower Sorbian and also an- swer multiple-choice questions, check spelling and grammar, and solve maths problems in both Sorbian languages. Our system is one LoRA adapter on Qwen3.5-2B, trained on the official parallel data, synthetic spelling and grammar examples, a question-answering proxy, and English GSM8K in about nine GPU- hours on two consumer RTX 3090 GPUs. Ex- tended translation-only fine-tuning cost about ten points of question-answering accuracy, re- producing a WMT25 finding, and nearly erased the output conventions of the other tasks; the multitask mixture recovered them at almost no translation cost. The system ranked fourth of four teams. It far exceeded the baseline on translation (21.7 → 61.5 chrF++) and spell checking (6.7 → 63.6), but on grammar check- ing and maths reasoning it learned the answer format without the skill: the grammar score is almost exactly the share of error-free sentences, and maths accuracy did not exceed the baseline. Two negative results may transfer to other low- resource settings. Synthetic holdouts did not predict performance on the official tasks in ei- ther direction, and self-translated training prob- lems passed every automatic check yet changed meaning in at least 6 of 20 inspected cases. The model is publicly available.

Modern mathematical reasoning benchmarks primarily focus on answer finding rather than proof verification, creating a gap in evaluating the proving capabilities of large language models (LLMs). We present a methodology for generating diverse mathematical proof tasks using formal tools. Our approach combines Lean-based synthetic problem generation with a Tool-Integrated Reasoning (TiR) framework for partial (sampling-based) proof validation, and it uses contrastive preference optimization to align the model’s proof outputs. Experiments on the Qwen-2.5 family of models demonstrate meaningful improvements in mathematical reasoning, particularly for smaller models. Our aligned models achieve up to a 57% higher success rate than baselines on the MiniF2F benchmark (across 0.5B, 1.5B, and 7B parameter models). These results highlight the potential of synthetic data and integrated validation for advancing LLM-based mathematical reasoning.