Projects

This is an ultra-low-resource research codebase that translates short Tangut titles into modern Chinese using only 491 parallel pairs, achieving its strongest results via a hybrid workflow of frontier prompt‑only models and locally trained DPO‑repaired candidates rather than any single approach.

Lean Portfolio Attribution is a research codebase that attributes inference-time gains in Lean theorem proving via fixed-budget attempt portfolios, retrieval-free controls, matched-compute baselines, and cross-system portability checks against external provers like ReProver.

CORAL is a research codebase that enhances trustworthy travel planning by directly parsing natural-language queries and applying localized repair, boosting pass rates on TravelPlanner and ChinaTravel while addressing benchmark infeasibility and constraint consistency.

This project studies whether logical-reasoning LLMs should be trained to emit three different evidence regimes: PROVE for entailed queries, REFUTE for contradicted queries, ABSTAIN for unsupported queries with a missing-support witness.

This repository studies LLM autoformalization on Rzk/sHoTT body-completion tasks, with an emphasis on shape-heavy held-out definitions, lightweight structural priors, repair, routing, and Lean portability checks.

A banking customer-emotion recognition system based on Qwen2-Audio 7B, using a dual-path audio pipeline to adapt to different call-recording qualities and service scenarios.

A deterministic translator toolkit for RC-1, a standardized R'lyehian/Cthuvian conlang layer. Turns English into Lovecraftian grammar with gloss support, sealed fallbacks, and an optional LLM-assisted registry.

An English TeX reconstruction of Informal Notes on Mathematics, with corrected and expanded notes compiled into a book-length PDF.

A long-running QQ bot codebase evolving from CQP to Mirai and AstrBot, preserving multiple generations of plugin architecture and bot operations.

A Tangut-Chinese translation prototype that combines dictionary scraping, sparse-script processing, and LLM-assisted interpretation for a low-resource historical writing system.

A deep-learning experiment for Google Emoji Kitchen-style emoji fusion, exploring image generation, spatial priors, and small-sample visual synthesis.

A Python pipeline for converting PDFs into structured text and generating AI-assisted summaries, keywords, and reusable reading notes.

A question-bank generator that extracts math problems from images, web pages, and PDFs through multimodal models, local OCR, and uniform TeX output.

The personal academic portal and archive behind this site, integrating mathematical notes, projects, fragments, classical writing, and research records.