Upload problem_solvers/self_play_conjectures.py
Browse files
problem_solvers/self_play_conjectures.py
ADDED
|
@@ -0,0 +1,238 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
"""
|
| 2 |
+
Self-Play Conjecture Generator for Zeta Zeros
|
| 3 |
+
===============================================
|
| 4 |
+
Inspired by STP (Self-play Theorem Prover, arXiv:2502.00212)
|
| 5 |
+
and Bourbaki (arXiv:2507.02726)
|
| 6 |
+
|
| 7 |
+
Key idea: A dual-role system where:
|
| 8 |
+
- CONJECTURER generates hypotheses about zero properties
|
| 9 |
+
- PROVER tests them numerically with 100k zeros
|
| 10 |
+
- Feedback loop: verified conjectures strengthen the conjecturer;
|
| 11 |
+
falsified ones teach it what NOT to propose
|
| 12 |
+
|
| 13 |
+
This creates its own curriculum of "barely verifiable" conjectures.
|
| 14 |
+
"""
|
| 15 |
+
|
| 16 |
+
import numpy as np
|
| 17 |
+
from typing import Dict, List, Tuple, Callable
|
| 18 |
+
import random
|
| 19 |
+
from scipy import stats as sp_stats
|
| 20 |
+
|
| 21 |
+
|
| 22 |
+
class Conjecture:
|
| 23 |
+
def __init__(self, statement: str, test_func: Callable, category: str):
|
| 24 |
+
self.statement = statement
|
| 25 |
+
self.test_func = test_func
|
| 26 |
+
self.category = category
|
| 27 |
+
self.verification_result = None
|
| 28 |
+
self.confidence = 0.0
|
| 29 |
+
|
| 30 |
+
|
| 31 |
+
class SelfPlayConjectureEngine:
|
| 32 |
+
"""
|
| 33 |
+
Generates, tests, and refines conjectures about zeta zeros.
|
| 34 |
+
"""
|
| 35 |
+
|
| 36 |
+
def __init__(self, zeros: List[float]):
|
| 37 |
+
self.zeros = np.array(zeros)
|
| 38 |
+
self.spacings = np.diff(self.zeros)
|
| 39 |
+
self.normalized = self.spacings / np.mean(self.spacings)
|
| 40 |
+
self.results = {}
|
| 41 |
+
self.verified_conjectures = []
|
| 42 |
+
self.falsified_conjectures = []
|
| 43 |
+
|
| 44 |
+
def _generate_conjectures(self, n_conjectures: int = 20) -> List[Conjecture]:
|
| 45 |
+
"""Generate candidate conjectures based on observed patterns."""
|
| 46 |
+
conjectures = []
|
| 47 |
+
|
| 48 |
+
# Conjecture 1: Spacing bounds
|
| 49 |
+
max_s = np.max(self.normalized)
|
| 50 |
+
conjectures.append(Conjecture(
|
| 51 |
+
f"All normalized spacings s_n satisfy s_n > 0.01 (observed min={np.min(self.normalized):.5f})",
|
| 52 |
+
lambda: np.all(self.normalized > 0.01),
|
| 53 |
+
"spacing_bounds"
|
| 54 |
+
))
|
| 55 |
+
|
| 56 |
+
# Conjecture 2: Mean spacing trend
|
| 57 |
+
windows = [100, 1000, 10000, 50000, 100000]
|
| 58 |
+
means = [np.mean(self.normalized[:w]) for w in windows if w <= len(self.normalized)]
|
| 59 |
+
conjectures.append(Conjecture(
|
| 60 |
+
f"Mean normalized spacing converges to 1.0 (current: {means[-1]:.6f})",
|
| 61 |
+
lambda: abs(means[-1] - 1.0) < 0.01,
|
| 62 |
+
"mean_convergence"
|
| 63 |
+
))
|
| 64 |
+
|
| 65 |
+
# Conjecture 3: Variance bound (GUE prediction: ~0.178)
|
| 66 |
+
var = np.var(self.normalized)
|
| 67 |
+
conjectures.append(Conjecture(
|
| 68 |
+
f"Variance of normalized spacings < 0.2 (GUE prediction: ~0.178, observed: {var:.6f})",
|
| 69 |
+
lambda: var < 0.2,
|
| 70 |
+
"variance"
|
| 71 |
+
))
|
| 72 |
+
|
| 73 |
+
# Conjecture 4: Arithmetic progression avoidance
|
| 74 |
+
def test_ap():
|
| 75 |
+
n_test = min(5000, len(self.zeros))
|
| 76 |
+
ap_count = 0
|
| 77 |
+
for i in range(n_test - 2):
|
| 78 |
+
d1 = self.zeros[i+1] - self.zeros[i]
|
| 79 |
+
d2 = self.zeros[i+2] - self.zeros[i+1]
|
| 80 |
+
if abs(d1 - d2) < 0.001:
|
| 81 |
+
ap_count += 1
|
| 82 |
+
return ap_count < 10
|
| 83 |
+
conjectures.append(Conjecture(
|
| 84 |
+
"No arithmetic progressions among zeros (< 10 near-AP in first 5000)",
|
| 85 |
+
test_ap,
|
| 86 |
+
"arithmetic_progressions"
|
| 87 |
+
))
|
| 88 |
+
|
| 89 |
+
# Conjecture 5: Repulsion (GUE level repulsion)
|
| 90 |
+
small_count = np.sum(self.normalized < 0.1)
|
| 91 |
+
conjectures.append(Conjecture(
|
| 92 |
+
f"Level repulsion: fewer than 5% of spacings < 0.1 (observed: {small_count/len(self.normalized):.4%})",
|
| 93 |
+
lambda: small_count / len(self.normalized) < 0.05,
|
| 94 |
+
"level_repulsion"
|
| 95 |
+
))
|
| 96 |
+
|
| 97 |
+
# Conjecture 6: Skewness (GUE: ~0.09)
|
| 98 |
+
skew = sp_stats.skew(self.normalized)
|
| 99 |
+
conjectures.append(Conjecture(
|
| 100 |
+
f"Skewness of spacings matches GUE (~0.09, observed: {skew:.4f})",
|
| 101 |
+
lambda: abs(skew - 0.09) < 0.05,
|
| 102 |
+
"skewness"
|
| 103 |
+
))
|
| 104 |
+
|
| 105 |
+
# Conjecture 7: Ratio of consecutive spacings
|
| 106 |
+
ratios = self.normalized[1:] / self.normalized[:-1]
|
| 107 |
+
conjectures.append(Conjecture(
|
| 108 |
+
f"Max consecutive spacing ratio < 10 (observed: {np.max(ratios):.2f})",
|
| 109 |
+
lambda: np.max(ratios) < 10,
|
| 110 |
+
"ratio_bound"
|
| 111 |
+
))
|
| 112 |
+
|
| 113 |
+
# Conjecture 8: Long-range correlation decay
|
| 114 |
+
def test_correlation_decay():
|
| 115 |
+
max_lag = 100
|
| 116 |
+
autocorrs = []
|
| 117 |
+
for lag in range(1, max_lag + 1):
|
| 118 |
+
if lag < len(self.normalized):
|
| 119 |
+
c = np.corrcoef(self.normalized[:-lag], self.normalized[lag:])[0, 1]
|
| 120 |
+
autocorrs.append(c)
|
| 121 |
+
return all(abs(c) < 0.1 for c in autocorrs)
|
| 122 |
+
conjectures.append(Conjecture(
|
| 123 |
+
"Long-range correlations decay to < 0.1 for all lags > 0",
|
| 124 |
+
test_correlation_decay,
|
| 125 |
+
"correlation"
|
| 126 |
+
))
|
| 127 |
+
|
| 128 |
+
# Conjecture 9: Sum of spacings exactness
|
| 129 |
+
total = np.sum(self.spacings)
|
| 130 |
+
predicted = self.zeros[-1] - self.zeros[0]
|
| 131 |
+
conjectures.append(Conjecture(
|
| 132 |
+
f"Sum of spacings equals γ_N - γ_1 exactly (error: {abs(total - predicted):.10f})",
|
| 133 |
+
lambda: abs(total - predicted) < 1e-6,
|
| 134 |
+
"telescoping"
|
| 135 |
+
))
|
| 136 |
+
|
| 137 |
+
# Conjecture 10: Even-odd symmetry in spacing distribution
|
| 138 |
+
n_half = len(self.normalized) // 2
|
| 139 |
+
first_half = self.normalized[:n_half]
|
| 140 |
+
second_half = self.normalized[n_half:]
|
| 141 |
+
conjectures.append(Conjecture(
|
| 142 |
+
"First-half and second-half spacing distributions are statistically similar (KS test)",
|
| 143 |
+
lambda: sp_stats.ks_2samp(first_half, second_half)[1] > 0.01,
|
| 144 |
+
"symmetry"
|
| 145 |
+
))
|
| 146 |
+
|
| 147 |
+
return conjectures[:n_conjectures]
|
| 148 |
+
|
| 149 |
+
def run_self_play(self, n_rounds: int = 3) -> Dict:
|
| 150 |
+
"""
|
| 151 |
+
Run self-play: generate conjectures, test, learn from results.
|
| 152 |
+
"""
|
| 153 |
+
print(f" [SelfPlay] Running {n_rounds} rounds of conjecture generation...")
|
| 154 |
+
|
| 155 |
+
all_verified = []
|
| 156 |
+
all_falsified = []
|
| 157 |
+
round_results = []
|
| 158 |
+
|
| 159 |
+
for round_idx in range(n_rounds):
|
| 160 |
+
conjectures = self._generate_conjectures()
|
| 161 |
+
|
| 162 |
+
verified = 0
|
| 163 |
+
falsified = 0
|
| 164 |
+
results = []
|
| 165 |
+
|
| 166 |
+
for c in conjectures:
|
| 167 |
+
try:
|
| 168 |
+
result = c.test_func()
|
| 169 |
+
c.verification_result = result
|
| 170 |
+
c.confidence = 1.0 if result else 0.0
|
| 171 |
+
|
| 172 |
+
if result:
|
| 173 |
+
verified += 1
|
| 174 |
+
all_verified.append(c)
|
| 175 |
+
else:
|
| 176 |
+
falsified += 1
|
| 177 |
+
all_falsified.append(c)
|
| 178 |
+
|
| 179 |
+
results.append({
|
| 180 |
+
'statement': c.statement,
|
| 181 |
+
'verified': result,
|
| 182 |
+
'category': c.category,
|
| 183 |
+
})
|
| 184 |
+
except Exception as e:
|
| 185 |
+
results.append({
|
| 186 |
+
'statement': c.statement,
|
| 187 |
+
'verified': False,
|
| 188 |
+
'error': str(e),
|
| 189 |
+
'category': c.category,
|
| 190 |
+
})
|
| 191 |
+
|
| 192 |
+
round_results.append({
|
| 193 |
+
'round': round_idx + 1,
|
| 194 |
+
'verified': verified,
|
| 195 |
+
'falsified': falsified,
|
| 196 |
+
'results': results,
|
| 197 |
+
})
|
| 198 |
+
|
| 199 |
+
print(f" Round {round_idx + 1}: {verified} verified, {falsified} falsified")
|
| 200 |
+
|
| 201 |
+
# Compute statistics
|
| 202 |
+
categories = {}
|
| 203 |
+
for c in all_verified + all_falsified:
|
| 204 |
+
cat = c.category
|
| 205 |
+
if cat not in categories:
|
| 206 |
+
categories[cat] = {'verified': 0, 'falsified': 0}
|
| 207 |
+
if c.verification_result:
|
| 208 |
+
categories[cat]['verified'] += 1
|
| 209 |
+
else:
|
| 210 |
+
categories[cat]['falsified'] += 1
|
| 211 |
+
|
| 212 |
+
self.results = {
|
| 213 |
+
'strategy': 'self_play_conjecture_generator',
|
| 214 |
+
'n_rounds': n_rounds,
|
| 215 |
+
'total_verified': len(all_verified),
|
| 216 |
+
'total_falsified': len(all_falsified),
|
| 217 |
+
'verification_rate': len(all_verified) / max(len(all_verified) + len(all_falsified), 1),
|
| 218 |
+
'round_results': round_results,
|
| 219 |
+
'category_breakdown': categories,
|
| 220 |
+
'verified_conjectures': [c.statement for c in all_verified],
|
| 221 |
+
'falsified_conjectures': [c.statement for c in all_falsified],
|
| 222 |
+
}
|
| 223 |
+
return self.results
|
| 224 |
+
|
| 225 |
+
def summary(self) -> str:
|
| 226 |
+
r = self.results
|
| 227 |
+
s = f"Self-Play Conjecture Engine\n{'='*50}\n"
|
| 228 |
+
s += f"Rounds: {r['n_rounds']}\n"
|
| 229 |
+
s += f"Total verified: {r['total_verified']}, falsified: {r['total_falsified']}\n"
|
| 230 |
+
s += f"Verification rate: {r['verification_rate']:.1%}\n"
|
| 231 |
+
s += "\nVerified conjectures:\n"
|
| 232 |
+
for c in r['verified_conjectures'][:5]:
|
| 233 |
+
s += f" ✓ {c[:80]}\n"
|
| 234 |
+
if r['falsified_conjectures']:
|
| 235 |
+
s += "\nFalsified conjectures (learn from these):\n"
|
| 236 |
+
for c in r['falsified_conjectures'][:3]:
|
| 237 |
+
s += f" ✗ {c[:80]}\n"
|
| 238 |
+
return s
|