Proof assistants such as Lean 4 offer machine-checkable verification of mathematical reasoning, but their adoption is limited because formal languages have a steep learning curve and can be challenging to use. Large language models offer a way to lower this barrier to entry through natural-language co-reasoning systems: proof assistants that users interact with entirely in natural language, and which use formal verification to provide feedback to users who submit incomplete and incorrect proofs. This paper explores such a co-reasoning system in an educational setting.

We explore metrics for three properties that are important for natural language co-reasoning systems—faithfulness, accuracy and appropriate granularity. We introduce an evaluation framework for these properties in the context of educational proofs. Second, we present a case study on an educational natural-language co-reasoning system for math proofs, evaluating its autoformalization harness on student-written proofs from an undergraduate linear algebra class using these three properties.

Developers can build LLM agents by adapting third-party models through benign post-training. We study a supply-chain threat in which an attacker supplies a model with a backdoor: hidden behavior that produces malicious outputs when a particular input pattern appears. Focusing on software-engineering agents, we ask whether such backdoors survive the developer’s supervised fine-tuning (SFT) and subsequent task-level reinforcement learning (RL). We observe that benign SFT substantially reduces attack success, but subsequent RL often preserves the residual behavior and sometimes even increases attack success. Our analysis of backdoor erosion during SFT identifies two factors that may favor survival: initial backdoor strength and gradient compatibility with benign training. These factors motivate PersistBD, which refines an already-backdoored model before release to improve its persistency through the benign post-training process. On Qwen2.5-Coder-7B, PersistBD raises attack success from 20% to 74% after SFT and from 20% to 76% after SFT-RL, while maintaining comparable benign task performance. Together, our results show that backdoors can remain active through benign post-training and that adversaries can deliberately increase their persistence. This highlights a supply-chain risk for AI developers and motivates stronger techniques for detecting and mitigating inherited backdoors when adapting third-party models into agents. Our code is available at https://github.com/uiuc-kang-lab/PersistBD.