3 months ago
- Proposal to measure how coding LLM perplexity scales with codebase context size, using Lean as a test case for formal languages.
- Aim to estimate scaling laws of 'predictability' by programming language, translating to security and safety improvements in software.
- Lean may have worse baseline performance but better scaling exponents, suggesting long-term benefits for program correctness and cybersecurity.
- Methodology involves empirical measurement via frozen LLMs, corpus construction, loss measurement, and scaling law fitting per language.
- Prediction: 'Weak' languages like Python excel at small scales but have worse scaling exponents, while 'strong' languages like Lean cross over at larger scales.
- Bias controls needed for programmer and domain differences; context learning and failure modes like ecosystem maturity effects are considered.