Merge pull request 'extract: 2026-02-28-demoura-when-ai-writes-software' (#1409) from extract/2026-02-28-demoura-when-ai-writes-software into main
This commit is contained in:
commit
4fed9af9d9
2 changed files with 51 additions and 1 deletions
|
|
@ -0,0 +1,35 @@
|
||||||
|
{
|
||||||
|
"rejected_claims": [
|
||||||
|
{
|
||||||
|
"filename": "ai-generated-code-overfits-test-suites-creating-adversarial-brittleness-that-testing-cannot-detect.md",
|
||||||
|
"issues": [
|
||||||
|
"missing_attribution_extractor"
|
||||||
|
]
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"filename": "supply-chain-poisoning-via-ai-training-data-enables-systematic-vulnerability-injection-at-ecosystem-scale.md",
|
||||||
|
"issues": [
|
||||||
|
"missing_attribution_extractor"
|
||||||
|
]
|
||||||
|
}
|
||||||
|
],
|
||||||
|
"validation_stats": {
|
||||||
|
"total": 2,
|
||||||
|
"kept": 0,
|
||||||
|
"fixed": 5,
|
||||||
|
"rejected": 2,
|
||||||
|
"fixes_applied": [
|
||||||
|
"ai-generated-code-overfits-test-suites-creating-adversarial-brittleness-that-testing-cannot-detect.md:set_created:2026-03-19",
|
||||||
|
"ai-generated-code-overfits-test-suites-creating-adversarial-brittleness-that-testing-cannot-detect.md:stripped_wiki_link:formal-verification-becomes-economically-necessary-as-AI-gen",
|
||||||
|
"ai-generated-code-overfits-test-suites-creating-adversarial-brittleness-that-testing-cannot-detect.md:stripped_wiki_link:AI-models-distinguish-testing-from-deployment-environments-p",
|
||||||
|
"supply-chain-poisoning-via-ai-training-data-enables-systematic-vulnerability-injection-at-ecosystem-scale.md:set_created:2026-03-19",
|
||||||
|
"supply-chain-poisoning-via-ai-training-data-enables-systematic-vulnerability-injection-at-ecosystem-scale.md:stripped_wiki_link:formal-verification-becomes-economically-necessary-as-AI-gen"
|
||||||
|
],
|
||||||
|
"rejections": [
|
||||||
|
"ai-generated-code-overfits-test-suites-creating-adversarial-brittleness-that-testing-cannot-detect.md:missing_attribution_extractor",
|
||||||
|
"supply-chain-poisoning-via-ai-training-data-enables-systematic-vulnerability-injection-at-ecosystem-scale.md:missing_attribution_extractor"
|
||||||
|
]
|
||||||
|
},
|
||||||
|
"model": "anthropic/claude-sonnet-4.5",
|
||||||
|
"date": "2026-03-19"
|
||||||
|
}
|
||||||
|
|
@ -7,11 +7,14 @@ date_published: 2026-02-28
|
||||||
date_archived: 2026-03-16
|
date_archived: 2026-03-16
|
||||||
domain: ai-alignment
|
domain: ai-alignment
|
||||||
secondary_domains: [teleological-economics]
|
secondary_domains: [teleological-economics]
|
||||||
status: unprocessed
|
status: enrichment
|
||||||
processed_by: theseus
|
processed_by: theseus
|
||||||
tags: [formal-verification, lean, ai-generated-code, proof-verification, trust-infrastructure]
|
tags: [formal-verification, lean, ai-generated-code, proof-verification, trust-infrastructure]
|
||||||
sourced_via: "Alex Obadia (@ObadiaAlex) tweet, ARIA Research Scaling Trust programme"
|
sourced_via: "Alex Obadia (@ObadiaAlex) tweet, ARIA Research Scaling Trust programme"
|
||||||
twitter_id: "712705562191011841"
|
twitter_id: "712705562191011841"
|
||||||
|
processed_by: theseus
|
||||||
|
processed_date: 2026-03-19
|
||||||
|
extraction_model: "anthropic/claude-sonnet-4.5"
|
||||||
---
|
---
|
||||||
|
|
||||||
# When AI Writes the World's Software, Who Verifies It?
|
# When AI Writes the World's Software, Who Verifies It?
|
||||||
|
|
@ -33,3 +36,15 @@ Key arguments:
|
||||||
- "The barrier to verified software is no longer AI capability. It is platform readiness."
|
- "The barrier to verified software is no longer AI capability. It is platform readiness."
|
||||||
|
|
||||||
Directly relevant to [[formal verification of AI-generated proofs provides scalable oversight that human review cannot match because machine-checked correctness scales with AI capability while human verification degrades]].
|
Directly relevant to [[formal verification of AI-generated proofs provides scalable oversight that human review cannot match because machine-checked correctness scales with AI capability while human verification degrades]].
|
||||||
|
|
||||||
|
|
||||||
|
## Key Facts
|
||||||
|
- Google: >25% of new code is AI-generated as of 2026
|
||||||
|
- Microsoft: ~30% of code is AI-generated as of 2026
|
||||||
|
- Microsoft CTO predicts 95% AI-generated code by 2030
|
||||||
|
- Anthropic built 100,000-line C compiler using AI agents in 2 weeks for <$20,000
|
||||||
|
- Nearly half of AI-generated code fails basic security tests
|
||||||
|
- Poor software quality costs US economy $2.41T/year (CSIQ 2022)
|
||||||
|
- Lean has 200K+ formalized theorems
|
||||||
|
- 5 Fields medalists have adopted Lean
|
||||||
|
- AlphaProof uses Lean as verification platform
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue