Dennis Koshta
I’m a software engineer at Bronco AI in San Francisco. My independent work covers language-model training, evaluation, and formal verification.
I’m interested in how models respond to training signals, where automated checks fail, and what we can learn by studying model internals.
Selected work
Upbringing
Post-training experiments with OLMo-2 and Qwen2.5: supervised fine-tuning, preference optimization, and reinforcement learning on arithmetic tasks. Includes checkpoints, evaluation results, and a grader audit.
BusyCoq contributions
Five merged contributions to BusyCoq: twelve nonhalting proofs and one halting proof. I directed the AI-assisted proof-search work and submitted the contributions; Claude Code produced the formalizations.
Curiosity & satisfaction in LLMs
Activation-steering experiments on Qwen3-32B. The completed screen found no change in stopping behavior across the tested interventions. The write-up covers the measurements, failed diagnostic, and limits of the result.
Cognanimus
An adaptive learning platform with learning paths, practice, generated feedback, and checked answers. My work covers the learning flow, grading, content contracts, and progress tracking.
Writing
What the checker actually checks
What a post-training grader audit, an adaptive-learning rubric, and a formal proof reveal about the limits of automated checks.
When steering changes nothing
Activation steering on Qwen3-32B changed the model’s activations without changing its stopping behavior in the tested conditions.
Interactive projects
Games, music tools, and small simulations developed with GPT and Claude. I set the direction, test the software, and refine the results.
Signal Garden
A music composition tool in which a landscape is also an editable score.
Try Signal Garden here
Press Play to hear the piece, then change notes in the sequencer. Closing this panel stops playback.
Also: Lanternfish LF-16, a fantasy computer with a compiler and debugger; Foldsmith+, a papercraft design tool.
Other software
rag-eval-kit evaluates retrieval-augmented generation. TransferBatch prepares print-production sheets. SheetMason labels and splits drawing sets. The project index includes these, my agent harness, and earlier systems work.